Series of a relation #
If r
is a relation on α
then a relation series of length n
is a series
a_0, a_1, ..., a_n
such that r a_i a_{i+1}
for all i < n
Let r
be a relation on α
, a relation series of r
of length n
is a series
a_0, a_1, ..., a_n
such that r a_i a_{i+1}
for all i < n
For any type α
, each term of α
gives a relation series with the right most index to be 0.
Equations
- RelSeries.singleton r a = { length := 0, toFun := fun (x : Fin (0 + 1)) => a, step := ⋯ }
Equations
- RelSeries.instInhabited r = { default := RelSeries.singleton r default }
Every nonempty list satisfying the chain condition gives a relation series
Relation series of r
and nonempty list of α
satisfying r
-chain condition bijectively
corresponds to each other.
Equations
- One or more equations did not get rendered due to their size.
A relation r
is said to be finite dimensional iff there is a relation series of r
with the
maximum length.
A relation
r
is said to be finite dimensional iff there is a relation series ofr
with the maximum length.
Instances
A relation r
is said to be infinite dimensional iff there exists relation series of arbitrary
length.
A relation
r
is said to be infinite dimensional iff there exists relation series of arbitrary length.
Instances
The longest relational series when a relation is finite dimensional
Equations
- RelSeries.longestOf r = ⋯.choose
A relation series with length n
if the relation is infinite dimensional
Equations
- RelSeries.withLength r n = ⋯.choose
If a relation on α
is infinite dimensional, then α
is nonempty.
Equations
- RelSeries.membership = { mem := Function.swap fun (x1 : α) (x2 : RelSeries r) => x1 ∈ Set.range x2.toFun }
If a₀ -r→ a₁ -r→ ... -r→ aₙ
and b₀ -r→ b₁ -r→ ... -r→ bₘ
are two strict series
such that r aₙ b₀
, then there is a chain of length n + m + 1
given by
a₀ -r→ a₁ -r→ ... -r→ aₙ -r→ b₀ -r→ b₁ -r→ ... -r→ bₘ
.
If a₀ -r→ a₁ -r→ ... -r→ aₙ
is an r
-series and a
is such that
aᵢ -r→ a -r→ a_ᵢ₊₁
, then
a₀ -r→ a₁ -r→ ... -r→ aᵢ -r→ a -r→ aᵢ₊₁ -r→ ... -r→ aₙ
is another r
-series
A relation series a₀ -r→ a₁ -r→ ... -r→ aₙ
of r
gives a relation series of the reverse of r
by reversing the series aₙ ←r- aₙ₋₁ ←r- ... ←r- a₁ ←r- a₀
.
Given a series a₀ -r→ a₁ -r→ ... -r→ aₙ
and an a
such that a₀ -r→ a
holds, there is
a series of length n+1
: a -r→ a₀ -r→ a₁ -r→ ... -r→ aₙ
.
Equations
- p.cons newHead rel = (RelSeries.singleton r newHead).append p rel
Given a series a₀ -r→ a₁ -r→ ... -r→ aₙ
and an a
such that aₙ -r→ a
holds, there is
a series of length n+1
: a₀ -r→ a₁ -r→ ... -r→ aₙ -r→ a
.
Equations
- p.snoc newLast rel = p.append (RelSeries.singleton r newLast) rel
Given two series of the form a₀ -r→ ... -r→ X
and X -r→ b ---> ...
,
then a₀ -r→ ... -r→ X -r→ b ...
is another series obtained by combining the given two.
Equations
- One or more equations did not get rendered due to their size.
A type is finite dimensional if its LTSeries
has bounded length.
Equations
- FiniteDimensionalOrder γ = Rel.FiniteDimensional fun (x1 x2 : γ) => x1 < x2
Equations
- ⋯ = ⋯
A type is infinite dimensional if it has LTSeries
of at least arbitrary length
Equations
- InfiniteDimensionalOrder γ = Rel.InfiniteDimensional fun (x1 x2 : γ) => x1 < x2
The longest <
-series when a type is finite dimensional
Equations
- LTSeries.longestOf α = RelSeries.longestOf fun (x1 x2 : α) => x1 < x2
A <
-series with length n
if the relation is infinite dimensional
Equations
- LTSeries.withLength α n = RelSeries.withLength (fun (x1 x2 : α) => x1 < x2) n
if α
is infinite dimensional, then α
is nonempty.
An alternative constructor of LTSeries
from a strictly monotone function.
Equations
- LTSeries.mk length toFun strictMono = { length := length, toFun := toFun, step := ⋯ }
An injection from the type of strictly monotone functions with limited length to LTSeries
.
Equations
- LTSeries.injStrictMono n = { toFun := fun (f : { f : (l : Fin n) × (Fin (↑l + 1) → α) // StrictMono f.snd }) => LTSeries.mk (↑(↑f).fst) (↑f).snd ⋯, inj' := ⋯ }
For two preorders α, β
, if f : α → β
is strictly monotonic, then a strict chain of α
can be pushed out to a strict chain of β
by
a₀ < a₁ < ... < aₙ ↦ f a₀ < f a₁ < ... < f aₙ
Equations
- p.map f hf = LTSeries.mk p.length (f ∘ p.toFun) ⋯
For two preorders α, β
, if f : α → β
is surjective and strictly comonotonic, then a
strict series of β
can be pulled back to a strict chain of α
by
b₀ < b₁ < ... < bₙ ↦ f⁻¹ b₀ < f⁻¹ b₁ < ... < f⁻¹ bₙ
where f⁻¹ bᵢ
is an arbitrary element in the
preimage of f⁻¹ {bᵢ}
.
Equations
- p.comap f comap surjective = LTSeries.mk p.length (fun (i : Fin (p.length + 1)) => ⋯.choose) ⋯
The strict series 0 < … < n
in ℕ
.
Equations
- LTSeries.range n = { length := n, toFun := fun (i : Fin (n + 1)) => ↑i, step := ⋯ }
In ℕ, the head and tail of an LTSeries
differ at least by the length of the series
In ℤ, the head and tail of an LTSeries
differ at least by the length of the series
Equations
- LTSeries.instFintypeOfDecidableRelLt = { elems := Finset.map (LTSeries.injStrictMono (Fintype.card α)) Finset.univ, complete := ⋯ }
If f : α → β
is a strictly monotonic function and α
is an infinite dimensional type then so
is β
.