Relation homomorphisms, embeddings, isomorphisms #
This file defines relation homomorphisms, embeddings, isomorphisms and order embeddings and isomorphisms.
Main declarations #
RelHom
: Relation homomorphism. ARelHom r s
is a functionf : α → β→ β
such thatr a b → s (f a) (f b)→ s (f a) (f b)
.RelEmbedding
: Relation embedding. ARelEmbedding r s
is an embeddingf : α ↪ β↪ β
such thatr a b ↔ s (f a) (f b)↔ s (f a) (f b)
.RelIso
: Relation isomorphism. ARelIso r s
is an equivalencef : α ≃ β≃ β
such thatr a b ↔ s (f a) (f b)↔ s (f a) (f b)
.sumLexCongr
,prodLexCongr
: Creates a relation homomorphism between twoSum.Lex
or twoProd.Lex
from relation homomorphisms between their arguments.
Notation #
→r→r
:RelHom
↪r↪r
:RelEmbedding
≃r≃r
:RelIso
The underlying function of a
RelHom
toFun : α → βA
RelHom
sends related elements to related elementsmap_rel' : {a b : α} → r a b → s (toFun a) (toFun b)
A relation homomorphism with respect to a given pair of relations r
and s
is a function f : α → β→ β
such that r a b → s (f a) (f b)→ s (f a) (f b)
.
Instances For
A relation homomorphism with respect to a given pair of relations r
and s
is a function f : α → β→ β
such that r a b → s (f a) (f b)→ s (f a) (f b)
.
Equations
- «term_→r_» = Lean.ParserDescr.trailingNode `term_→r_ 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →r ") (Lean.ParserDescr.cat `term 26))
A
RelHomClass
sends related elements to related elementsmap_rel : (f : F) → {a b : α} → r a b → s (↑f a) (↑f b)
RelHomClass F r s
asserts that F
is a type of functions such that all f : F
satisfy r a b → s (f a) (f b)→ s (f a) (f b)
.
The relations r
and s
are outParam
s since figuring them out from a goal is a higher-order
matching problem that Lean usually can't do unaided.
Instances
Equations
- RelHom.instRelHomClassRelHom = RelHomClass.mk RelHom.map_rel'
The map coe_fn : (r →r s) → (α → β)→r s) → (α → β)→ (α → β)→ β)
is injective.
Composition of two relation homomorphisms is a relation homomorphism.
Equations
- RelHom.comp g f = { toFun := fun x => ↑g (↑f x), map_rel' := @RelHom.comp.proof_1 α β γ r s t g f }
A relation homomorphism is also a relation homomorphism between dual relations.
Equations
- RelHom.swap f = { toFun := ↑f, map_rel' := @RelHom.swap.proof_1 α β r s f }
An increasing function is injective
An increasing function is injective
Elements are related iff they are related after apply a
RelEmbedding
map_rel_iff' : ∀ {a b : α}, s (↑toEmbedding a) (↑toEmbedding b) ↔ r a b
A relation embedding with respect to a given pair of relations r
and s
is an embedding f : α ↪ β↪ β
such that r a b ↔ s (f a) (f b)↔ s (f a) (f b)
.
Instances For
A relation embedding with respect to a given pair of relations r
and s
is an embedding f : α ↪ β↪ β
such that r a b ↔ s (f a) (f b)↔ s (f a) (f b)
.
Equations
- «term_↪r_» = Lean.ParserDescr.trailingNode `term_↪r_ 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ↪r ") (Lean.ParserDescr.cat `term 26))
A relation embedding is also a relation homomorphism
Equations
- RelEmbedding.toRelHom f = { toFun := f.toEmbedding.toFun, map_rel' := @RelEmbedding.toRelHom.proof_1 α β r s f }
Equations
- RelEmbedding.instRelHomClassRelEmbedding = RelHomClass.mk RelEmbedding.instRelHomClassRelEmbedding.proof_2
See Note [custom simps projection]. We specify this explicitly because we have a coercion not
given by the FunLike
instance. Todo: remove that instance?
Equations
- RelEmbedding.Simps.apply h = ↑h.toEmbedding
The map coe_fn : (r ↪r s) → (α → β)↪r s) → (α → β)→ (α → β)→ β)
is injective.
Equations
- RelEmbedding.instInhabitedRelEmbedding r = { default := RelEmbedding.refl r }
A relation embedding is also a relation embedding between dual relations.
Equations
- RelEmbedding.swap f = { toEmbedding := f.toEmbedding, map_rel_iff' := (_ : ∀ {a b : α}, s (↑f.toEmbedding b) (↑f.toEmbedding a) ↔ r b a) }
If f
is injective, then it is a relation embedding from the
preimage relation of s
to s
.
Equations
- RelEmbedding.preimage f s = { toEmbedding := f, map_rel_iff' := (_ : ∀ {a b : α}, s (↑f a) (↑f b) ↔ s (↑f a) (↑f b)) }
Quotient.out
as a relation embedding between the lift of a relation and the relation.
Equations
- One or more equations did not get rendered due to their size.
A relation is well founded iff its lift to a quotient is.
Alias of the reverse direction of wellFounded_lift₂_iff
.
Alias of the forward direction of wellFounded_lift₂_iff
.
To define an relation embedding from an antisymmetric relation r
to a reflexive relation s
it suffices to give a function together with a proof that it satisfies s (f a) (f b) ↔ r a b↔ r a b
.
Equations
- RelEmbedding.ofMapRelIff f hf = { toEmbedding := { toFun := f, inj' := (_ : ∀ (x x_1 : α), f x = f x_1 → x = x_1) }, map_rel_iff' := (_ : ∀ {a b : α}, s (f a) (f b) ↔ r a b) }
It suffices to prove f
is monotone between strict relations
to show it is a relation embedding.
Equations
- One or more equations did not get rendered due to their size.
Sum.inl
as a relation embedding into Sum.LiftRel r s
.
Equations
- One or more equations did not get rendered due to their size.
Sum.inr
as a relation embedding into Sum.LiftRel r s
.
Equations
- One or more equations did not get rendered due to their size.
Sum.map
as a relation embedding between Sum.LiftRel
relations.
Equations
- One or more equations did not get rendered due to their size.
Sum.inl
as a relation embedding into Sum.Lex r s
.
Equations
- RelEmbedding.sumLexInl r s = { toEmbedding := { toFun := Sum.inl, inj' := (_ : Function.Injective Sum.inl) }, map_rel_iff' := (_ : ∀ {a b : α}, Sum.Lex r s (Sum.inl a) (Sum.inl b) ↔ r a b) }
Sum.inr
as a relation embedding into Sum.Lex r s
.
Equations
- RelEmbedding.sumLexInr r s = { toEmbedding := { toFun := Sum.inr, inj' := (_ : Function.Injective Sum.inr) }, map_rel_iff' := (_ : ∀ {a b : β}, Sum.Lex r s (Sum.inr a) (Sum.inr b) ↔ s a b) }
Sum.map
as a relation embedding between Sum.Lex
relations.
Equations
- One or more equations did not get rendered due to their size.
Elements are related iff they are related after apply a
RelIso
map_rel_iff' : ∀ {a b : α}, s (↑toEquiv a) (↑toEquiv b) ↔ r a b
A relation isomorphism is an equivalence that is also a relation embedding.
Instances For
A relation isomorphism is an equivalence that is also a relation embedding.
Equations
- «term_≃r_» = Lean.ParserDescr.trailingNode `term_≃r_ 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≃r ") (Lean.ParserDescr.cat `term 26))
Convert an RelIso
to a RelEmbedding
. This function is also available as a coercion
but often it is easier to write f.toRelEmbedding
than to write explicitly r
and s
in the target type.
Equations
- RelIso.toRelEmbedding f = { toEmbedding := Equiv.toEmbedding f.toEquiv, map_rel_iff' := (_ : ∀ {a b : α}, s (↑f.toEquiv a) (↑f.toEquiv b) ↔ r a b) }
Equations
- RelIso.instRelHomClassRelIso = RelHomClass.mk RelIso.instRelHomClassRelIso.proof_2
The map coe_fn : (r ≃r s) → (α → β)≃r s) → (α → β)→ (α → β)→ β)
is injective. Lean fails to parse
function.injective (λ e : r ≃r s, (e : α → β))≃r s, (e : α → β))→ β))
, so we use a trick to say the same.
Inverse map of a relation isomorphism is a relation isomorphism.
Equations
- RelIso.symm f = { toEquiv := Equiv.symm f.toEquiv, map_rel_iff' := (_ : ∀ (a b : β), r (↑(Equiv.symm f.toEquiv) a) (↑(Equiv.symm f.toEquiv) b) ↔ s a b) }
See Note [custom simps projection]. We need to specify this projection explicitly in this case,
because RelIso
defines custom coercions other than the ones given by FunLike
.
Equations
- RelIso.Simps.apply h = ↑(RelIso.toRelEmbedding h).toEmbedding
See Note [custom simps projection].
Equations
- RelIso.Simps.symm_apply h = ↑(RelIso.toRelEmbedding (RelIso.symm h)).toEmbedding
Identity map is a relation isomorphism.
Equations
- RelIso.refl r = { toEquiv := Equiv.refl α, map_rel_iff' := (_ : ∀ {a b : α}, r (↑(Equiv.refl α) a) (↑(Equiv.refl α) b) ↔ r (↑(Equiv.refl α) a) (↑(Equiv.refl α) b)) }
Equations
- RelIso.instInhabitedRelIso r = { default := RelIso.refl r }
A relation isomorphism between equal relations on equal types.
Equations
- RelIso.cast h₁ h₂ = { toEquiv := Equiv.cast h₁, map_rel_iff' := (_ : ∀ (a b : α), s (↑(Equiv.cast h₁) a) (↑(Equiv.cast h₁) b) ↔ r a b) }
a relation isomorphism is also a relation isomorphism between dual relations.
Equations
- RelIso.swap f = { toEquiv := f.toEquiv, map_rel_iff' := (_ : ∀ {a b : α}, s (↑(RelIso.toRelEmbedding f).toEmbedding b) (↑(RelIso.toRelEmbedding f).toEmbedding a) ↔ r b a) }
A surjective relation embedding is a relation isomorphism.
Equations
- One or more equations did not get rendered due to their size.
Given relation isomorphisms r₁ ≃r s₁≃r s₁
and r₂ ≃r s₂≃r s₂
, construct a relation isomorphism for the
lexicographic orders on the sum.
Equations
- One or more equations did not get rendered due to their size.
Given relation isomorphisms r₁ ≃r s₁≃r s₁
and r₂ ≃r s₂≃r s₂
, construct a relation isomorphism for the
lexicographic orders on the product.
Equations
- One or more equations did not get rendered due to their size.
Two relations on empty types are isomorphic.
Equations
- RelIso.relIsoOfIsEmpty r s = { toEquiv := Equiv.equivOfIsEmpty α β, map_rel_iff' := (_ : ∀ (a : α) {b : α}, s (↑(Equiv.equivOfIsEmpty α β) a) (↑(Equiv.equivOfIsEmpty α β) b) ↔ r a b) }
Two irreflexive relations on a unique type are isomorphic.
Equations
- RelIso.relIsoOfUniqueOfIrrefl r s = { toEquiv := Equiv.equivOfUnique α β, map_rel_iff' := (_ : ∀ {a b : α}, s (↑(Equiv.equivOfUnique α β) a) (↑(Equiv.equivOfUnique α β) b) ↔ r a b) }
Two reflexive relations on a unique type are isomorphic.
Equations
- RelIso.relIsoOfUniqueOfRefl r s = { toEquiv := Equiv.equivOfUnique α β, map_rel_iff' := (_ : ∀ {a b : α}, s (↑(Equiv.equivOfUnique α β) a) (↑(Equiv.equivOfUnique α β) b) ↔ r a b) }