Initial and principal segments #
This file defines initial and principal segments.
Main definitions #
InitialSeg r s
: type of order embeddings ofr
intos
for which the range is an initial segment (i.e., ifb
belongs to the range, then anyb' < b
also belongs to the range). It is denoted byr ≼i s
.PrincipalSeg r s
: Type of order embeddings ofr
intos
for which the range is a principal segment, i.e., an interval of the form(-∞, top)
for some elementtop
. It is denoted byr ≺i s
.
The lemmas Ordinal.type_le_iff
and Ordinal.type_lt_iff
tell us that ≼i
corresponds to the ≤
relation on ordinals, while ≺i
corresponds to the <
relation. This prompts us to think of
PrincipalSeg
as a "strict" version of InitialSeg
.
Notations #
These notations belong to the InitialSeg
locale.
r ≼i s
: the type of initial segment embeddings ofr
intos
.r ≺i s
: the type of principal segment embeddings ofr
intos
.α ≤i β
is an abbreviation for(· < ·) ≼i (· < ·)
.α <i β
is an abbreviation for(· < ·) ≺i (· < ·)
.
Initial segments #
Order embeddings whose range is an initial segment of s
(i.e., if b
belongs to the range, then
any b' < b
also belongs to the range). The type of these embeddings from r
to s
is called
InitialSeg r s
, and denoted by r ≼i s
.
If r
is a relation on α
and s
in a relation on β
, then f : r ≼i s
is an order
embedding whose range is an initial segment. That is, whenever b < f a
in β
then b
is in the
range of f
.
- toFun : α → β
- inj' : Function.Injective self.toFun
- map_rel_iff' : ∀ {a b : α}, s (self.toEmbedding a) (self.toEmbedding b) ↔ r a b
- mem_range_of_rel' : ∀ (a : α) (b : β), s b (self.toRelEmbedding a) → b ∈ Set.range ⇑self.toRelEmbedding
The order embedding is an initial segment
If r
is a relation on α
and s
in a relation on β
, then f : r ≼i s
is an order
embedding whose range is an initial segment. That is, whenever b < f a
in β
then b
is in the
range of f
.
Equations
- «term_≼i_» = Lean.ParserDescr.trailingNode `term_≼i_ 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≼i ") (Lean.ParserDescr.cat `term 26))
An InitialSeg
between the <
relations of two types.
Equations
- «term_≤i_» = Lean.ParserDescr.trailingNode `term_≤i_ 25 24 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≤i ") (Lean.ParserDescr.cat `term 25))
Equations
- ⋯ = ⋯
An initial segment embedding between the <
relations of two partial orders is an order
embedding.
Equations
- f.toOrderEmbedding = f.orderEmbeddingOfLTEmbedding
Equations
- ⋯ = ⋯
Alias of InitialSeg.mem_range_of_rel
.
An order isomorphism is an initial segment
Equations
- InitialSeg.ofIso f = { toRelEmbedding := f.toRelEmbedding, mem_range_of_rel' := ⋯ }
The identity function shows that ≼i
is reflexive
Equations
- InitialSeg.refl r = { toRelEmbedding := RelEmbedding.refl r, mem_range_of_rel' := ⋯ }
Equations
- InitialSeg.instInhabited r = { default := InitialSeg.refl r }
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
If we have order embeddings between α
and β
whose images are initial segments, and β
is a well-order then α
and β
are order-isomorphic.
Equations
- f.antisymm g = { toFun := ⇑f, invFun := ⇑g, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }
Restrict the codomain of an initial segment
Equations
- InitialSeg.codRestrict p f H = { toRelEmbedding := RelEmbedding.codRestrict p f.toRelEmbedding H, mem_range_of_rel' := ⋯ }
Initial segment from an empty type.
Equations
- InitialSeg.ofIsEmpty r s = { toRelEmbedding := RelEmbedding.ofIsEmpty r s, mem_range_of_rel' := ⋯ }
Initial segment embedding of an order r
into the disjoint union of r
and s
.
Equations
- InitialSeg.leAdd r s = { toFun := Sum.inl, inj' := ⋯, map_rel_iff' := ⋯, mem_range_of_rel' := ⋯ }
Principal segments #
Order embeddings whose range is a principal segment of s
(i.e., an interval of the form
(-∞, top)
for some element top
of β
). The type of these embeddings from r
to s
is called
PrincipalSeg r s
, and denoted by r ≺i s
. Principal segments are in particular initial
segments.
If r
is a relation on α
and s
in a relation on β
, then f : r ≺i s
is an order
embedding whose range is an open interval (-∞, top)
for some element top
of β
. Such order
embeddings are called principal segments
- toFun : α → β
- inj' : Function.Injective self.toFun
- map_rel_iff' : ∀ {a b : α}, s (self.toEmbedding a) (self.toEmbedding b) ↔ r a b
- top : β
The supremum of the principal segment
The range of the order embedding is the set of elements
b
such thats b top
If r
is a relation on α
and s
in a relation on β
, then f : r ≺i s
is an order
embedding whose range is an open interval (-∞, top)
for some element top
of β
. Such order
embeddings are called principal segments
Equations
- «term_≺i_» = Lean.ParserDescr.trailingNode `term_≺i_ 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≺i ") (Lean.ParserDescr.cat `term 26))
A PrincipalSeg
between the <
relations of two types.
Equations
- «term_<i_» = Lean.ParserDescr.trailingNode `term_<i_ 25 24 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <i ") (Lean.ParserDescr.cat `term 25))
Alias of PrincipalSeg.exists_eq_iff_rel
.
A principal segment is the same as a non-surjective initial segment.
Equations
- f.toPrincipalSeg hf = { toRelEmbedding := f.toRelEmbedding, top := Classical.choose ⋯, mem_range_iff_rel' := ⋯ }
Equations
- ⋯ = ⋯
Composition of a principal segment with an initial segment, as a principal segment
Equations
- f.ltLe g = { toRelEmbedding := f.trans g.toRelEmbedding, top := g f.top, mem_range_iff_rel' := ⋯ }
Composition of two principal segments as a principal segment
Equations
- f.trans g = f.ltLe { toRelEmbedding := g.toRelEmbedding, mem_range_of_rel' := ⋯ }
Composition of an order isomorphism with a principal segment, as a principal segment
Equations
- PrincipalSeg.equivLT f g = { toRelEmbedding := f.toRelEmbedding.trans g.toRelEmbedding, top := g.top, mem_range_iff_rel' := ⋯ }
Composition of a principal segment with an order isomorphism, as a principal segment
Equations
- f.ltEquiv g = { toRelEmbedding := f.trans g.toRelEmbedding, top := g f.top, mem_range_iff_rel' := ⋯ }
Given a well order s
, there is a most one principal segment embedding of r
into s
.
Equations
- ⋯ = ⋯
Alias of PrincipalSeg.top_rel_top
.
Any element of a well order yields a principal segment
Equations
- PrincipalSeg.ofElement r a = { toRelEmbedding := Subrel.relEmbedding r {b : α | r b a}, top := a, mem_range_iff_rel' := ⋯ }
For any principal segment r ≺i s
, there is a Subrel
of s
order isomorphic to r
.
Equations
- f.subrelIso = { toEquiv := (Equiv.ofInjective ⇑f.toRelEmbedding ⋯).trans (Equiv.setCongr ⋯), map_rel_iff' := ⋯ }.symm
Restrict the codomain of a principal segment
Equations
- PrincipalSeg.codRestrict p f H H₂ = { toRelEmbedding := RelEmbedding.codRestrict p f.toRelEmbedding H, top := ⟨f.top, H₂⟩, mem_range_iff_rel' := ⋯ }
Principal segment from an empty type into a type with a minimal element.
Equations
- PrincipalSeg.ofIsEmpty r H = { toRelEmbedding := RelEmbedding.ofIsEmpty r s, top := b, mem_range_iff_rel' := ⋯ }
Principal segment from the empty relation on PEmpty
to the empty relation on PUnit
.
Equations
- PrincipalSeg.pemptyToPunit = PrincipalSeg.ofIsEmpty EmptyRelation ⋯
Properties of initial and principal segments #
To an initial segment taking values in a well order, one can associate either a principal segment (if the range is not everything, hence one can take as top the minimum of the complement of the range) or an order isomorphism (if the range is everything).
Equations
- f.ltOrEq = if h : Function.Surjective ⇑f then Sum.inr (RelIso.ofSurjective f.toRelEmbedding h) else Sum.inl (f.toPrincipalSeg h)
Composition of an initial segment taking values in a well order and a principal segment.
Equations
- f.leLT g = match f.ltOrEq with | Sum.inl f' => f'.trans g | Sum.inr f' => PrincipalSeg.equivLT f' g
Given an order embedding into a well order, collapse the order embedding by filling the
gaps, to obtain an initial segment. Here, we construct the collapsed order embedding pointwise,
but the proof of the fact that it is an initial segment will be given in collapse
.
Construct an initial segment from an order embedding into a well order, by collapsing it to fill the gaps.
Equations
- f.collapse = { toRelEmbedding := RelEmbedding.ofMonotone (fun (a : α) => ↑(f.collapseF a)) ⋯, mem_range_of_rel' := ⋯ }
For any two well orders, one is an initial segment of the other.
Equations
- One or more equations did not get rendered due to their size.