Complete lattice homomorphisms #
This file defines frame homomorphisms and complete lattice homomorphisms.
We use the DFunLike design, so each type of morphisms has a companion typeclass which is meant to
be satisfied by itself and all stricter types.
Types of morphisms #
sSupHom: Maps which preserve⨆.sInfHom: Maps which preserve⨅.FrameHom: Frame homomorphisms. Maps which preserve⨆,⊓and⊤.CompleteLatticeHom: Complete lattice homomorphisms. Maps which preserve⨆and⨅.
Typeclasses #
Concrete homs #
CompleteLatticeHom.setPreimage:Set.preimageas a complete lattice homomorphism.
TODO #
Frame homs are Heyting homs.
The type of ⨆-preserving functions from α to β.
- toFun : α → β
The underlying function of a sSupHom.
The proposition that a
sSupHomcommutes with arbitrary suprema/joins.
The type of ⨅-preserving functions from α to β.
structure
FrameHom
(α : Type u_8)
(β : Type u_9)
[CompleteLattice α]
[CompleteLattice β]
extends
InfTopHom
:
Type (max u_8 u_9)
The type of frame homomorphisms from α to β. They preserve finite meets and arbitrary joins.
- toFun : α → β
The proposition that frame homomorphisms commute with arbitrary suprema/joins.
structure
CompleteLatticeHom
(α : Type u_8)
(β : Type u_9)
[CompleteLattice α]
[CompleteLattice β]
extends
sInfHom
:
Type (max u_8 u_9)
The type of complete lattice homomorphisms from α to β.
- toFun : α → β
The proposition that complete lattice homomorphism commutes with arbitrary suprema/joins.
class
sSupHomClass
(F : Type u_8)
(α : Type u_9)
(β : Type u_10)
[SupSet α]
[SupSet β]
[FunLike F α β]
:
sSupHomClass F α β states that F is a type of ⨆-preserving morphisms.
You should extend this class when you extend sSupHom.
The proposition that members of
sSupHomClasss commute with arbitrary suprema/joins.
class
sInfHomClass
(F : Type u_8)
(α : Type u_9)
(β : Type u_10)
[InfSet α]
[InfSet β]
[FunLike F α β]
:
sInfHomClass F α β states that F is a type of ⨅-preserving morphisms.
You should extend this class when you extend sInfHom.
The proposition that members of
sInfHomClasss commute with arbitrary infima/meets.
class
FrameHomClass
(F : Type u_8)
(α : Type u_9)
(β : Type u_10)
[CompleteLattice α]
[CompleteLattice β]
[FunLike F α β]
extends
InfTopHomClass
:
FrameHomClass F α β states that F is a type of frame morphisms. They preserve ⊓ and ⨆.
You should extend this class when you extend FrameHom.
The proposition that members of
FrameHomClasscommute with arbitrary suprema/joins.
class
CompleteLatticeHomClass
(F : Type u_8)
(α : Type u_9)
(β : Type u_10)
[CompleteLattice α]
[CompleteLattice β]
[FunLike F α β]
extends
sInfHomClass
:
CompleteLatticeHomClass F α β states that F is a type of complete lattice morphisms.
You should extend this class when you extend CompleteLatticeHom.
The proposition that members of
CompleteLatticeHomClasscommute with arbitrary suprema/joins.
instance
sSupHomClass.toSupBotHomClass
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[FunLike F α β]
[CompleteLattice α]
[CompleteLattice β]
[sSupHomClass F α β]
:
SupBotHomClass F α β
Equations
- ⋯ = ⋯
instance
sInfHomClass.toInfTopHomClass
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[FunLike F α β]
[CompleteLattice α]
[CompleteLattice β]
[sInfHomClass F α β]
:
InfTopHomClass F α β
Equations
- ⋯ = ⋯
instance
FrameHomClass.tosSupHomClass
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[FunLike F α β]
[CompleteLattice α]
[CompleteLattice β]
[FrameHomClass F α β]
:
sSupHomClass F α β
Equations
- ⋯ = ⋯
instance
FrameHomClass.toBoundedLatticeHomClass
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[FunLike F α β]
[CompleteLattice α]
[CompleteLattice β]
[FrameHomClass F α β]
:
BoundedLatticeHomClass F α β
Equations
- ⋯ = ⋯
instance
CompleteLatticeHomClass.toFrameHomClass
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[FunLike F α β]
[CompleteLattice α]
[CompleteLattice β]
[CompleteLatticeHomClass F α β]
:
FrameHomClass F α β
Equations
- ⋯ = ⋯
instance
CompleteLatticeHomClass.toBoundedLatticeHomClass
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[FunLike F α β]
[CompleteLattice α]
[CompleteLattice β]
[CompleteLatticeHomClass F α β]
:
BoundedLatticeHomClass F α β
Equations
- ⋯ = ⋯
instance
OrderIsoClass.tosSupHomClass
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[EquivLike F α β]
[CompleteLattice α]
[CompleteLattice β]
[OrderIsoClass F α β]
:
sSupHomClass F α β
Equations
- ⋯ = ⋯
instance
OrderIsoClass.tosInfHomClass
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[EquivLike F α β]
[CompleteLattice α]
[CompleteLattice β]
[OrderIsoClass F α β]
:
sInfHomClass F α β
Equations
- ⋯ = ⋯
instance
OrderIsoClass.toCompleteLatticeHomClass
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[EquivLike F α β]
[CompleteLattice α]
[CompleteLattice β]
[OrderIsoClass F α β]
:
CompleteLatticeHomClass F α β
Equations
- ⋯ = ⋯
@[simp]
theorem
OrderIso.toCompleteLatticeHom_toFun
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
(f : α ≃o β)
(a : α)
:
(OrderIso.toCompleteLatticeHom f).toFun a = f a
def
OrderIso.toCompleteLatticeHom
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
(f : α ≃o β)
:
Reinterpret an order isomorphism as a morphism of complete lattices.
Equations
- OrderIso.toCompleteLatticeHom f = { tosInfHom := { toFun := ⇑f, map_sInf' := ⋯ }, map_sSup' := ⋯ }
instance
instCoeTCFrameHom
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[FunLike F α β]
[CompleteLattice α]
[CompleteLattice β]
[FrameHomClass F α β]
:
Equations
- instCoeTCFrameHom = { coe := fun (f : F) => { toInfTopHom := { toInfHom := { toFun := ⇑f, map_inf' := ⋯ }, map_top' := ⋯ }, map_sSup' := ⋯ } }
instance
instCoeTCCompleteLatticeHom
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[FunLike F α β]
[CompleteLattice α]
[CompleteLattice β]
[CompleteLatticeHomClass F α β]
:
CoeTC F (CompleteLatticeHom α β)
Equations
- instCoeTCCompleteLatticeHom = { coe := fun (f : F) => { tosInfHom := { toFun := ⇑f, map_sInf' := ⋯ }, map_sSup' := ⋯ } }
Supremum homomorphisms #
instance
sSupHom.instSSupHomClassSSupHomInstFunLikeSSupHom
{α : Type u_2}
{β : Type u_3}
[SupSet α]
[SupSet β]
:
sSupHomClass (sSupHom α β) α β
Equations
- ⋯ = ⋯
@[simp]
theorem
sSupHom.coe_copy
{α : Type u_2}
{β : Type u_3}
[SupSet α]
[SupSet β]
(f : sSupHom α β)
(f' : α → β)
(h : f' = ⇑f)
:
⇑(sSupHom.copy f f' h) = f'
theorem
sSupHom.copy_eq
{α : Type u_2}
{β : Type u_3}
[SupSet α]
[SupSet β]
(f : sSupHom α β)
(f' : α → β)
(h : f' = ⇑f)
:
sSupHom.copy f f' h = f
Equations
- sSupHom.id α = { toFun := id, map_sSup' := ⋯ }
Equations
- sSupHom.instInhabitedSSupHom α = { default := sSupHom.id α }
@[simp]
theorem
sSupHom.comp_assoc
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
{δ : Type u_5}
[SupSet α]
[SupSet β]
[SupSet γ]
[SupSet δ]
(f : sSupHom γ δ)
(g : sSupHom β γ)
(h : sSupHom α β)
:
sSupHom.comp (sSupHom.comp f g) h = sSupHom.comp f (sSupHom.comp g h)
@[simp]
theorem
sSupHom.comp_id
{α : Type u_2}
{β : Type u_3}
[SupSet α]
[SupSet β]
(f : sSupHom α β)
:
sSupHom.comp f (sSupHom.id α) = f
@[simp]
theorem
sSupHom.id_comp
{α : Type u_2}
{β : Type u_3}
[SupSet α]
[SupSet β]
(f : sSupHom α β)
:
sSupHom.comp (sSupHom.id β) f = f
@[simp]
theorem
sSupHom.cancel_right
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[SupSet α]
[SupSet β]
[SupSet γ]
{g₁ : sSupHom β γ}
{g₂ : sSupHom β γ}
{f : sSupHom α β}
(hf : Function.Surjective ⇑f)
:
sSupHom.comp g₁ f = sSupHom.comp g₂ f ↔ g₁ = g₂
@[simp]
theorem
sSupHom.cancel_left
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[SupSet α]
[SupSet β]
[SupSet γ]
{g : sSupHom β γ}
{f₁ : sSupHom α β}
{f₂ : sSupHom α β}
(hg : Function.Injective ⇑g)
:
sSupHom.comp g f₁ = sSupHom.comp g f₂ ↔ f₁ = f₂
instance
sSupHom.instPartialOrderSSupHomToSupSet
{α : Type u_2}
{β : Type u_3}
[SupSet α]
:
{x : CompleteLattice β} → PartialOrder (sSupHom α β)
Equations
- sSupHom.instPartialOrderSSupHomToSupSet = PartialOrder.lift (fun (f : sSupHom α β) => ⇑f) ⋯
instance
sSupHom.instBotSSupHomToSupSet
{α : Type u_2}
{β : Type u_3}
[SupSet α]
:
{x : CompleteLattice β} → Bot (sSupHom α β)
instance
sSupHom.instOrderBotSSupHomToSupSetToLEToPreorderInstPartialOrderSSupHomToSupSet
{α : Type u_2}
{β : Type u_3}
[SupSet α]
:
{x : CompleteLattice β} → OrderBot (sSupHom α β)
Equations
- sSupHom.instOrderBotSSupHomToSupSetToLEToPreorderInstPartialOrderSSupHomToSupSet = OrderBot.mk ⋯
@[simp]
@[simp]
theorem
sSupHom.bot_apply
{α : Type u_2}
{β : Type u_3}
[SupSet α]
:
∀ {x : CompleteLattice β} (a : α), ⊥ a = ⊥
Infimum homomorphisms #
instance
sInfHom.instSInfHomClassSInfHomInstFunLikeSInfHom
{α : Type u_2}
{β : Type u_3}
[InfSet α]
[InfSet β]
:
sInfHomClass (sInfHom α β) α β
Equations
- ⋯ = ⋯
@[simp]
theorem
sInfHom.coe_copy
{α : Type u_2}
{β : Type u_3}
[InfSet α]
[InfSet β]
(f : sInfHom α β)
(f' : α → β)
(h : f' = ⇑f)
:
⇑(sInfHom.copy f f' h) = f'
theorem
sInfHom.copy_eq
{α : Type u_2}
{β : Type u_3}
[InfSet α]
[InfSet β]
(f : sInfHom α β)
(f' : α → β)
(h : f' = ⇑f)
:
sInfHom.copy f f' h = f
Equations
- sInfHom.id α = { toFun := id, map_sInf' := ⋯ }
Equations
- sInfHom.instInhabitedSInfHom α = { default := sInfHom.id α }
@[simp]
theorem
sInfHom.comp_assoc
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
{δ : Type u_5}
[InfSet α]
[InfSet β]
[InfSet γ]
[InfSet δ]
(f : sInfHom γ δ)
(g : sInfHom β γ)
(h : sInfHom α β)
:
sInfHom.comp (sInfHom.comp f g) h = sInfHom.comp f (sInfHom.comp g h)
@[simp]
theorem
sInfHom.comp_id
{α : Type u_2}
{β : Type u_3}
[InfSet α]
[InfSet β]
(f : sInfHom α β)
:
sInfHom.comp f (sInfHom.id α) = f
@[simp]
theorem
sInfHom.id_comp
{α : Type u_2}
{β : Type u_3}
[InfSet α]
[InfSet β]
(f : sInfHom α β)
:
sInfHom.comp (sInfHom.id β) f = f
@[simp]
theorem
sInfHom.cancel_right
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[InfSet α]
[InfSet β]
[InfSet γ]
{g₁ : sInfHom β γ}
{g₂ : sInfHom β γ}
{f : sInfHom α β}
(hf : Function.Surjective ⇑f)
:
sInfHom.comp g₁ f = sInfHom.comp g₂ f ↔ g₁ = g₂
@[simp]
theorem
sInfHom.cancel_left
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[InfSet α]
[InfSet β]
[InfSet γ]
{g : sInfHom β γ}
{f₁ : sInfHom α β}
{f₂ : sInfHom α β}
(hg : Function.Injective ⇑g)
:
sInfHom.comp g f₁ = sInfHom.comp g f₂ ↔ f₁ = f₂
instance
sInfHom.instPartialOrderSInfHomToInfSet
{α : Type u_2}
{β : Type u_3}
[InfSet α]
[CompleteLattice β]
:
PartialOrder (sInfHom α β)
Equations
- sInfHom.instPartialOrderSInfHomToInfSet = PartialOrder.lift (fun (f : sInfHom α β) => ⇑f) ⋯
instance
sInfHom.instTopSInfHomToInfSet
{α : Type u_2}
{β : Type u_3}
[InfSet α]
[CompleteLattice β]
:
instance
sInfHom.instOrderTopSInfHomToInfSetToLEToPreorderInstPartialOrderSInfHomToInfSet
{α : Type u_2}
{β : Type u_3}
[InfSet α]
[CompleteLattice β]
:
Equations
- sInfHom.instOrderTopSInfHomToInfSetToLEToPreorderInstPartialOrderSInfHomToInfSet = OrderTop.mk ⋯
@[simp]
@[simp]
Frame homomorphisms #
instance
FrameHom.instFunLikeFrameHom
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
:
instance
FrameHom.instFrameHomClassFrameHomInstFunLikeFrameHom
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
:
FrameHomClass (FrameHom α β) α β
Equations
- ⋯ = ⋯
def
FrameHom.toLatticeHom
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
(f : FrameHom α β)
:
LatticeHom α β
Reinterpret a FrameHom as a LatticeHom.
Equations
- FrameHom.toLatticeHom f = { toSupHom := { toFun := ⇑f, map_sup' := ⋯ }, map_inf' := ⋯ }
theorem
FrameHom.toFun_eq_coe
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
(f : FrameHom α β)
:
f.toFun = ⇑f
@[simp]
theorem
FrameHom.coe_toInfTopHom
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
(f : FrameHom α β)
:
⇑f.toInfTopHom = ⇑f
@[simp]
theorem
FrameHom.coe_toLatticeHom
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
(f : FrameHom α β)
:
⇑(FrameHom.toLatticeHom f) = ⇑f
@[simp]
theorem
FrameHom.coe_mk
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
(f : InfTopHom α β)
(hf : ∀ (s : Set α), f.toFun (sSup s) = sSup (f.toFun '' s))
:
⇑{ toInfTopHom := f, map_sSup' := hf } = ⇑f
theorem
FrameHom.ext
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
{f : FrameHom α β}
{g : FrameHom α β}
(h : ∀ (a : α), f a = g a)
:
f = g
def
FrameHom.copy
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
(f : FrameHom α β)
(f' : α → β)
(h : f' = ⇑f)
:
FrameHom α β
Copy of a FrameHom with a new toFun equal to the old one. Useful to fix definitional
equalities.
Equations
- FrameHom.copy f f' h = let __src := sSupHom.copy { toFun := ⇑f, map_sSup' := ⋯ } f' h; { toInfTopHom := InfTopHom.copy f.toInfTopHom f' h, map_sSup' := ⋯ }
@[simp]
theorem
FrameHom.coe_copy
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
(f : FrameHom α β)
(f' : α → β)
(h : f' = ⇑f)
:
⇑(FrameHom.copy f f' h) = f'
theorem
FrameHom.copy_eq
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
(f : FrameHom α β)
(f' : α → β)
(h : f' = ⇑f)
:
FrameHom.copy f f' h = f
Equations
- FrameHom.id α = let __src := sSupHom.id α; { toInfTopHom := InfTopHom.id α, map_sSup' := ⋯ }
Equations
- FrameHom.instInhabitedFrameHom α = { default := FrameHom.id α }
@[simp]
def
FrameHom.comp
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[CompleteLattice α]
[CompleteLattice β]
[CompleteLattice γ]
(f : FrameHom β γ)
(g : FrameHom α β)
:
FrameHom α γ
Composition of FrameHoms as a FrameHom.
Equations
- FrameHom.comp f g = let __src := sSupHom.comp { toFun := ⇑f, map_sSup' := ⋯ } { toFun := ⇑g, map_sSup' := ⋯ }; { toInfTopHom := InfTopHom.comp f.toInfTopHom g.toInfTopHom, map_sSup' := ⋯ }
@[simp]
theorem
FrameHom.coe_comp
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[CompleteLattice α]
[CompleteLattice β]
[CompleteLattice γ]
(f : FrameHom β γ)
(g : FrameHom α β)
:
⇑(FrameHom.comp f g) = ⇑f ∘ ⇑g
@[simp]
theorem
FrameHom.comp_apply
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[CompleteLattice α]
[CompleteLattice β]
[CompleteLattice γ]
(f : FrameHom β γ)
(g : FrameHom α β)
(a : α)
:
(FrameHom.comp f g) a = f (g a)
@[simp]
theorem
FrameHom.comp_assoc
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
{δ : Type u_5}
[CompleteLattice α]
[CompleteLattice β]
[CompleteLattice γ]
[CompleteLattice δ]
(f : FrameHom γ δ)
(g : FrameHom β γ)
(h : FrameHom α β)
:
FrameHom.comp (FrameHom.comp f g) h = FrameHom.comp f (FrameHom.comp g h)
@[simp]
theorem
FrameHom.comp_id
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
(f : FrameHom α β)
:
FrameHom.comp f (FrameHom.id α) = f
@[simp]
theorem
FrameHom.id_comp
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
(f : FrameHom α β)
:
FrameHom.comp (FrameHom.id β) f = f
@[simp]
theorem
FrameHom.cancel_right
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[CompleteLattice α]
[CompleteLattice β]
[CompleteLattice γ]
{g₁ : FrameHom β γ}
{g₂ : FrameHom β γ}
{f : FrameHom α β}
(hf : Function.Surjective ⇑f)
:
FrameHom.comp g₁ f = FrameHom.comp g₂ f ↔ g₁ = g₂
@[simp]
theorem
FrameHom.cancel_left
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[CompleteLattice α]
[CompleteLattice β]
[CompleteLattice γ]
{g : FrameHom β γ}
{f₁ : FrameHom α β}
{f₂ : FrameHom α β}
(hg : Function.Injective ⇑g)
:
FrameHom.comp g f₁ = FrameHom.comp g f₂ ↔ f₁ = f₂
instance
FrameHom.instPartialOrderFrameHom
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
:
PartialOrder (FrameHom α β)
Equations
- FrameHom.instPartialOrderFrameHom = PartialOrder.lift (fun (f : FrameHom α β) => ⇑f) ⋯
Complete lattice homomorphisms #
instance
CompleteLatticeHom.instFunLikeCompleteLatticeHom
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
:
FunLike (CompleteLatticeHom α β) α β
Equations
- CompleteLatticeHom.instFunLikeCompleteLatticeHom = { coe := fun (f : CompleteLatticeHom α β) => f.toFun, coe_injective' := ⋯ }
instance
CompleteLatticeHom.instCompleteLatticeHomClassCompleteLatticeHomInstFunLikeCompleteLatticeHom
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
:
CompleteLatticeHomClass (CompleteLatticeHom α β) α β
Equations
- ⋯ = ⋯
def
CompleteLatticeHom.tosSupHom
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
(f : CompleteLatticeHom α β)
:
sSupHom α β
Reinterpret a CompleteLatticeHom as a sSupHom.
Equations
- CompleteLatticeHom.tosSupHom f = { toFun := ⇑f, map_sSup' := ⋯ }
def
CompleteLatticeHom.toBoundedLatticeHom
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
(f : CompleteLatticeHom α β)
:
Reinterpret a CompleteLatticeHom as a BoundedLatticeHom.
Equations
- One or more equations did not get rendered due to their size.
theorem
CompleteLatticeHom.toFun_eq_coe
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
(f : CompleteLatticeHom α β)
:
f.toFun = ⇑f
@[simp]
theorem
CompleteLatticeHom.coe_tosInfHom
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
(f : CompleteLatticeHom α β)
:
⇑f.tosInfHom = ⇑f
@[simp]
theorem
CompleteLatticeHom.coe_tosSupHom
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
(f : CompleteLatticeHom α β)
:
⇑(CompleteLatticeHom.tosSupHom f) = ⇑f
@[simp]
theorem
CompleteLatticeHom.coe_toBoundedLatticeHom
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
(f : CompleteLatticeHom α β)
:
@[simp]
theorem
CompleteLatticeHom.coe_mk
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
(f : sInfHom α β)
(hf : ∀ (s : Set α), f.toFun (sSup s) = sSup (f.toFun '' s))
:
⇑{ tosInfHom := f, map_sSup' := hf } = ⇑f
theorem
CompleteLatticeHom.ext
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
{f : CompleteLatticeHom α β}
{g : CompleteLatticeHom α β}
(h : ∀ (a : α), f a = g a)
:
f = g
def
CompleteLatticeHom.copy
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
(f : CompleteLatticeHom α β)
(f' : α → β)
(h : f' = ⇑f)
:
Copy of a CompleteLatticeHom with a new toFun equal to the old one. Useful to fix
definitional equalities.
Equations
- CompleteLatticeHom.copy f f' h = let __src := sSupHom.copy (CompleteLatticeHom.tosSupHom f) f' h; { tosInfHom := sInfHom.copy f.tosInfHom f' h, map_sSup' := ⋯ }
@[simp]
theorem
CompleteLatticeHom.coe_copy
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
(f : CompleteLatticeHom α β)
(f' : α → β)
(h : f' = ⇑f)
:
⇑(CompleteLatticeHom.copy f f' h) = f'
theorem
CompleteLatticeHom.copy_eq
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
(f : CompleteLatticeHom α β)
(f' : α → β)
(h : f' = ⇑f)
:
CompleteLatticeHom.copy f f' h = f
id as a CompleteLatticeHom.
Equations
- CompleteLatticeHom.id α = let __src := sSupHom.id α; let __src := sInfHom.id α; { tosInfHom := { toFun := id, map_sInf' := ⋯ }, map_sSup' := ⋯ }
instance
CompleteLatticeHom.instInhabitedCompleteLatticeHom
(α : Type u_2)
[CompleteLattice α]
:
Inhabited (CompleteLatticeHom α α)
Equations
- CompleteLatticeHom.instInhabitedCompleteLatticeHom α = { default := CompleteLatticeHom.id α }
@[simp]
theorem
CompleteLatticeHom.coe_id
(α : Type u_2)
[CompleteLattice α]
:
⇑(CompleteLatticeHom.id α) = id
@[simp]
theorem
CompleteLatticeHom.id_apply
{α : Type u_2}
[CompleteLattice α]
(a : α)
:
(CompleteLatticeHom.id α) a = a
def
CompleteLatticeHom.comp
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[CompleteLattice α]
[CompleteLattice β]
[CompleteLattice γ]
(f : CompleteLatticeHom β γ)
(g : CompleteLatticeHom α β)
:
Composition of CompleteLatticeHoms as a CompleteLatticeHom.
Equations
- CompleteLatticeHom.comp f g = let __src := sSupHom.comp (CompleteLatticeHom.tosSupHom f) (CompleteLatticeHom.tosSupHom g); { tosInfHom := sInfHom.comp f.tosInfHom g.tosInfHom, map_sSup' := ⋯ }
@[simp]
theorem
CompleteLatticeHom.coe_comp
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[CompleteLattice α]
[CompleteLattice β]
[CompleteLattice γ]
(f : CompleteLatticeHom β γ)
(g : CompleteLatticeHom α β)
:
⇑(CompleteLatticeHom.comp f g) = ⇑f ∘ ⇑g
@[simp]
theorem
CompleteLatticeHom.comp_apply
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[CompleteLattice α]
[CompleteLattice β]
[CompleteLattice γ]
(f : CompleteLatticeHom β γ)
(g : CompleteLatticeHom α β)
(a : α)
:
(CompleteLatticeHom.comp f g) a = f (g a)
@[simp]
theorem
CompleteLatticeHom.comp_assoc
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
{δ : Type u_5}
[CompleteLattice α]
[CompleteLattice β]
[CompleteLattice γ]
[CompleteLattice δ]
(f : CompleteLatticeHom γ δ)
(g : CompleteLatticeHom β γ)
(h : CompleteLatticeHom α β)
:
@[simp]
theorem
CompleteLatticeHom.comp_id
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
(f : CompleteLatticeHom α β)
:
@[simp]
theorem
CompleteLatticeHom.id_comp
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
(f : CompleteLatticeHom α β)
:
@[simp]
theorem
CompleteLatticeHom.cancel_right
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[CompleteLattice α]
[CompleteLattice β]
[CompleteLattice γ]
{g₁ : CompleteLatticeHom β γ}
{g₂ : CompleteLatticeHom β γ}
{f : CompleteLatticeHom α β}
(hf : Function.Surjective ⇑f)
:
CompleteLatticeHom.comp g₁ f = CompleteLatticeHom.comp g₂ f ↔ g₁ = g₂
@[simp]
theorem
CompleteLatticeHom.cancel_left
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[CompleteLattice α]
[CompleteLattice β]
[CompleteLattice γ]
{g : CompleteLatticeHom β γ}
{f₁ : CompleteLatticeHom α β}
{f₂ : CompleteLatticeHom α β}
(hg : Function.Injective ⇑g)
:
CompleteLatticeHom.comp g f₁ = CompleteLatticeHom.comp g f₂ ↔ f₁ = f₂
Dual homs #
@[simp]
@[simp]
theorem
sSupHom.dual_comp
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[SupSet α]
[SupSet β]
[SupSet γ]
(g : sSupHom β γ)
(f : sSupHom α β)
:
sSupHom.dual (sSupHom.comp g f) = sInfHom.comp (sSupHom.dual g) (sSupHom.dual f)
@[simp]
theorem
sSupHom.symm_dual_id
{α : Type u_2}
[SupSet α]
:
sSupHom.dual.symm (sInfHom.id αᵒᵈ) = sSupHom.id α
@[simp]
@[simp]
theorem
sInfHom.dual_comp
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[InfSet α]
[InfSet β]
[InfSet γ]
(g : sInfHom β γ)
(f : sInfHom α β)
:
sInfHom.dual (sInfHom.comp g f) = sSupHom.comp (sInfHom.dual g) (sInfHom.dual f)
@[simp]
theorem
sInfHom.symm_dual_id
{α : Type u_2}
[InfSet α]
:
sInfHom.dual.symm (sSupHom.id αᵒᵈ) = sInfHom.id α
@[simp]
theorem
CompleteLatticeHom.dual_symm_apply_toFun
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
(f : CompleteLatticeHom αᵒᵈ βᵒᵈ)
:
@[simp]
theorem
CompleteLatticeHom.dual_apply_toFun
{α : Type u_2}
{β : Type u_3}
[CompleteLattice α]
[CompleteLattice β]
(f : CompleteLatticeHom α β)
:
Reinterpret a complete lattice homomorphism as a complete lattice homomorphism between the dual lattices.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CompleteLatticeHom.dual_id
{α : Type u_2}
[CompleteLattice α]
:
CompleteLatticeHom.dual (CompleteLatticeHom.id α) = CompleteLatticeHom.id αᵒᵈ
@[simp]
theorem
CompleteLatticeHom.dual_comp
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[CompleteLattice α]
[CompleteLattice β]
[CompleteLattice γ]
(g : CompleteLatticeHom β γ)
(f : CompleteLatticeHom α β)
:
CompleteLatticeHom.dual (CompleteLatticeHom.comp g f) = CompleteLatticeHom.comp (CompleteLatticeHom.dual g) (CompleteLatticeHom.dual f)
@[simp]
theorem
CompleteLatticeHom.symm_dual_id
{α : Type u_2}
[CompleteLattice α]
:
CompleteLatticeHom.dual.symm (CompleteLatticeHom.id αᵒᵈ) = CompleteLatticeHom.id α
@[simp]
theorem
CompleteLatticeHom.symm_dual_comp
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[CompleteLattice α]
[CompleteLattice β]
[CompleteLattice γ]
(g : CompleteLatticeHom βᵒᵈ γᵒᵈ)
(f : CompleteLatticeHom αᵒᵈ βᵒᵈ)
:
CompleteLatticeHom.dual.symm (CompleteLatticeHom.comp g f) = CompleteLatticeHom.comp (CompleteLatticeHom.dual.symm g) (CompleteLatticeHom.dual.symm f)
Concrete homs #
def
CompleteLatticeHom.setPreimage
{α : Type u_2}
{β : Type u_3}
(f : α → β)
:
CompleteLatticeHom (Set β) (Set α)
Set.preimage as a complete lattice homomorphism.
See also sSupHom.setImage.
Equations
- CompleteLatticeHom.setPreimage f = { tosInfHom := { toFun := Set.preimage f, map_sInf' := ⋯ }, map_sSup' := ⋯ }
@[simp]
@[simp]
theorem
CompleteLatticeHom.setPreimage_apply
{α : Type u_2}
{β : Type u_3}
(f : α → β)
(s : Set β)
:
(CompleteLatticeHom.setPreimage f) s = f ⁻¹' s
@[simp]
theorem
CompleteLatticeHom.setPreimage_comp
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
(g : β → γ)
(f : α → β)
:
@[simp]
theorem
sSupHom.setImage_toFun
{α : Type u_2}
{β : Type u_3}
(f : α → β)
(s : Set α)
:
(sSupHom.setImage f) s = f '' s
Using Set.image, a function between types yields a sSupHom between their lattices of
subsets.
See also CompleteLatticeHom.setPreimage.
Equations
- sSupHom.setImage f = { toFun := Set.image f, map_sSup' := ⋯ }
@[simp]
theorem
Equiv.toOrderIsoSet_apply
{α : Type u_2}
{β : Type u_3}
(e : α ≃ β)
(s : Set α)
:
(Equiv.toOrderIsoSet e) s = ⇑e '' s
@[simp]
theorem
Equiv.toOrderIsoSet_symm_apply
{α : Type u_2}
{β : Type u_3}
(e : α ≃ β)
(s : Set β)
:
(RelIso.symm (Equiv.toOrderIsoSet e)) s = ⇑e.symm '' s
An equivalence of types yields an order isomorphism between their lattices of subsets.
The map (a, b) ↦ a ⊔ b as a sSupHom.
The map (a, b) ↦ a ⊓ b as an sInfHom.
@[simp]
@[simp]