Mathlib.Order.Hom.BoundedLattice

SupBotHom structure

(α β : Type*) [Max α] [Max β] [Bot α] [Bot β] extends SupHom α β

Full source

/-- The type of finitary supremum-preserving homomorphisms from `α` to `β`. -/
structure SupBotHom (α β : Type*) [Max α] [Max β] [Bot α] [Bot β] extends SupHom α β where
  /-- A `SupBotHom` preserves the bottom element.

  Do not use this directly. Use `map_bot` instead. -/
  map_bot' : toFun ⊥ = ⊥

Finitary supremum-preserving homomorphism

Informal description

The structure representing finitary supremum-preserving homomorphisms between types `α` and `β`, where both types are equipped with a maximum operation `⊔` and a bottom element `⊥`. A `SupBotHom` preserves both the supremum operation and the bottom element.

InfTopHom structure

(α β : Type*) [Min α] [Min β] [Top α] [Top β] extends InfHom α β

Full source

/-- The type of finitary infimum-preserving homomorphisms from `α` to `β`. -/
structure InfTopHom (α β : Type*) [Min α] [Min β] [Top α] [Top β] extends InfHom α β where
  /-- An `InfTopHom` preserves the top element.

  Do not use this directly. Use `map_top` instead. -/
  map_top' : toFun ⊤ = ⊤

Finitary infimum-preserving homomorphism

Informal description

The structure representing finitary infimum-preserving homomorphisms from a type $\alpha$ to a type $\beta$, where both types are equipped with a minimum operation $\sqcap$ and a top element $\top$. This extends the structure of infimum-preserving homomorphisms (`InfHom`), requiring additionally that the top element is preserved.

BoundedLatticeHom structure

(α β : Type*) [Lattice α] [Lattice β] [BoundedOrder α]
  [BoundedOrder β] extends LatticeHom α β

Full source

/-- The type of bounded lattice homomorphisms from `α` to `β`. -/
structure BoundedLatticeHom (α β : Type*) [Lattice α] [Lattice β] [BoundedOrder α]
  [BoundedOrder β] extends LatticeHom α β where
  /-- A `BoundedLatticeHom` preserves the top element.

  Do not use this directly. Use `map_top` instead. -/
  map_top' : toFun ⊤ = ⊤
  /-- A `BoundedLatticeHom` preserves the bottom element.

  Do not use this directly. Use `map_bot` instead. -/
  map_bot' : toFun ⊥ = ⊥

Bounded Lattice Homomorphism

Informal description

The structure representing bounded lattice homomorphisms from a lattice $\alpha$ to a lattice $\beta$, where both lattices are equipped with a greatest element $\top$ and a least element $\bot$. A bounded lattice homomorphism preserves the lattice operations $\sqcup$ (supremum) and $\sqcap$ (infimum), as well as the top and bottom elements.

SupBotHomClass structure

(F α β : Type*) [Max α] [Max β] [Bot α] [Bot β] [FunLike F α β] : Prop
  extends SupHomClass F α β

Full source

/-- `SupBotHomClass F α β` states that `F` is a type of finitary supremum-preserving morphisms.

You should extend this class when you extend `SupBotHom`. -/
class SupBotHomClass (F α β : Type*) [Max α] [Max β] [Bot α] [Bot β] [FunLike F α β] : Prop
  extends SupHomClass F α β where
  /-- A `SupBotHomClass` morphism preserves the bottom element. -/
  map_bot (f : F) : f ⊥ = ⊥

Finitary supremum-preserving homomorphism class

Informal description

The class `SupBotHomClass F α β` states that `F` is a type of finitary supremum-preserving morphisms from a type `α` to a type `β`, where both types are equipped with a maximum operation `⊔` and a bottom element `⊥`. A morphism in this class preserves both the supremum operation and the bottom element.

InfTopHomClass structure

(F α β : Type*) [Min α] [Min β] [Top α] [Top β] [FunLike F α β] : Prop
  extends InfHomClass F α β

Full source

/-- `InfTopHomClass F α β` states that `F` is a type of finitary infimum-preserving morphisms.

You should extend this class when you extend `SupBotHom`. -/
class InfTopHomClass (F α β : Type*) [Min α] [Min β] [Top α] [Top β] [FunLike F α β] : Prop
  extends InfHomClass F α β where
  /-- An `InfTopHomClass` morphism preserves the top element. -/
  map_top (f : F) : f ⊤ = ⊤

Finitary infimum-preserving homomorphism class

Informal description

The class `InfTopHomClass F α β` states that `F` is a type of finitary infimum-preserving morphisms from a type `α` to a type `β`, where both types are equipped with a minimum operation `⊓` and a top element `⊤`. A morphism in this class preserves both the infimum operation and the top element.

BoundedLatticeHomClass structure

(F α β : Type*) [Lattice α] [Lattice β] [BoundedOrder α]
    [BoundedOrder β] [FunLike F α β] : Prop
  extends LatticeHomClass F α β

Full source

/-- `BoundedLatticeHomClass F α β` states that `F` is a type of bounded lattice morphisms.

You should extend this class when you extend `BoundedLatticeHom`. -/
class BoundedLatticeHomClass (F α β : Type*) [Lattice α] [Lattice β] [BoundedOrder α]
    [BoundedOrder β] [FunLike F α β] : Prop
  extends LatticeHomClass F α β where
  /-- A `BoundedLatticeHomClass` morphism preserves the top element. -/
  map_top (f : F) : f ⊤ = ⊤
  /-- A `BoundedLatticeHomClass` morphism preserves the bottom element. -/
  map_bot (f : F) : f ⊥ = ⊥

Bounded Lattice Homomorphism Class

Informal description

The class `BoundedLatticeHomClass F α β` states that `F` is a type of bounded lattice homomorphisms between lattices `α` and `β`, where both lattices are equipped with a greatest element $\top$ and a least element $\bot$. A bounded lattice homomorphism is a function that preserves the lattice operations (meet $\sqcap$ and join $\sqcup$) as well as the top and bottom elements.

SupBotHomClass.toBotHomClass instance

[Max α] [Max β] [Bot α] [Bot β] [SupBotHomClass F α β] : BotHomClass F α β

Full source

instance (priority := 100) SupBotHomClass.toBotHomClass [Max α] [Max β] [Bot α]
    [Bot β] [SupBotHomClass F α β] : BotHomClass F α β :=
  { ‹SupBotHomClass F α β› with }

Supremum-Preserving Homomorphisms Preserve Bottom Elements

Informal description

For any types $\alpha$ and $\beta$ equipped with a maximum operation $\sqcup$ and a bottom element $\bot$, every finitary supremum-preserving homomorphism from $\alpha$ to $\beta$ is also a bottom-preserving homomorphism.

InfTopHomClass.toTopHomClass instance

[Min α] [Min β] [Top α] [Top β] [InfTopHomClass F α β] : TopHomClass F α β

Full source

instance (priority := 100) InfTopHomClass.toTopHomClass [Min α] [Min β] [Top α]
    [Top β] [InfTopHomClass F α β] : TopHomClass F α β :=
  { ‹InfTopHomClass F α β› with }

Infimum-Preserving Homomorphisms Preserve Top Elements

Informal description

For any types $\alpha$ and $\beta$ equipped with a minimum operation $\sqcap$ and a top element $\top$, every finitary infimum-preserving homomorphism from $\alpha$ to $\beta$ is also a top-preserving homomorphism.

BoundedLatticeHomClass.toSupBotHomClass instance

[Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] [BoundedLatticeHomClass F α β] : SupBotHomClass F α β

Full source

instance (priority := 100) BoundedLatticeHomClass.toSupBotHomClass [Lattice α] [Lattice β]
    [BoundedOrder α] [BoundedOrder β] [BoundedLatticeHomClass F α β] :
    SupBotHomClass F α β :=
  { ‹BoundedLatticeHomClass F α β› with }

Bounded Lattice Homomorphisms Preserve Suprema and Bottom

Informal description

For any two lattices $\alpha$ and $\beta$ with bounded orders, every bounded lattice homomorphism from $\alpha$ to $\beta$ is also a finitary supremum-preserving homomorphism that preserves the bottom element.

BoundedLatticeHomClass.toInfTopHomClass instance

[Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] [BoundedLatticeHomClass F α β] : InfTopHomClass F α β

Full source

instance (priority := 100) BoundedLatticeHomClass.toInfTopHomClass [Lattice α] [Lattice β]
    [BoundedOrder α] [BoundedOrder β] [BoundedLatticeHomClass F α β] :
    InfTopHomClass F α β :=
  { ‹BoundedLatticeHomClass F α β› with }

Bounded Lattice Homomorphisms Preserve Infima and Top

Informal description

For any two lattices $\alpha$ and $\beta$ with bounded orders, every bounded lattice homomorphism from $\alpha$ to $\beta$ is also a finitary infimum-preserving homomorphism that preserves the top element.

BoundedLatticeHomClass.toBoundedOrderHomClass instance

 [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] [BoundedLatticeHomClass F α β] : BoundedOrderHomClass F α β

Full source

instance (priority := 100) BoundedLatticeHomClass.toBoundedOrderHomClass [Lattice α]
    [Lattice β] [BoundedOrder α] [BoundedOrder β] [BoundedLatticeHomClass F α β] :
    BoundedOrderHomClass F α β :=
{ show OrderHomClass F α β from inferInstance, ‹BoundedLatticeHomClass F α β› with }

Bounded Lattice Homomorphisms are Bounded Order Homomorphisms

Informal description

For any two lattices $\alpha$ and $\beta$ with bounded orders, every bounded lattice homomorphism from $\alpha$ to $\beta$ is also a bounded order homomorphism. That is, it preserves the partial order relation, the greatest element $\top$, and the least element $\bot$.

OrderIsoClass.toSupBotHomClass instance

[SemilatticeSup α] [OrderBot α] [SemilatticeSup β] [OrderBot β] [OrderIsoClass F α β] : SupBotHomClass F α β

Full source

instance (priority := 100) OrderIsoClass.toSupBotHomClass [SemilatticeSup α] [OrderBot α]
    [SemilatticeSup β] [OrderBot β] [OrderIsoClass F α β] : SupBotHomClass F α β :=
  { OrderIsoClass.toSupHomClass, OrderIsoClass.toBotHomClass with }

Order Isomorphisms Preserve Suprema and Bottom Element

Informal description

For any two semilattices with suprema $\alpha$ and $\beta$ that are also equipped with bottom elements $\bot$, every order isomorphism between them preserves both suprema and the bottom element. That is, if $F$ is a type of order isomorphisms from $\alpha$ to $\beta$, then any $f \in F$ satisfies $f(x \sqcup y) = f(x) \sqcup f(y)$ for all $x, y \in \alpha$ and $f(\bot) = \bot$.

OrderIsoClass.toInfTopHomClass instance

[SemilatticeInf α] [OrderTop α] [SemilatticeInf β] [OrderTop β] [OrderIsoClass F α β] : InfTopHomClass F α β

Full source

instance (priority := 100) OrderIsoClass.toInfTopHomClass [SemilatticeInf α] [OrderTop α]
    [SemilatticeInf β] [OrderTop β] [OrderIsoClass F α β] : InfTopHomClass F α β :=
  { OrderIsoClass.toInfHomClass, OrderIsoClass.toTopHomClass with }

Order Isomorphisms Preserve Infima and Top Elements

Informal description

For any semilattice infima $\alpha$ and $\beta$ with top elements, every order isomorphism between them preserves both finite infima and the top element. That is, if $F$ is a type of order isomorphisms from $\alpha$ to $\beta$, then any $f \in F$ satisfies $f(x \sqcap y) = f(x) \sqcap f(y)$ for all $x, y \in \alpha$ and $f(\top_\alpha) = \top_\beta$.

OrderIsoClass.toBoundedLatticeHomClass instance

[Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] [OrderIsoClass F α β] : BoundedLatticeHomClass F α β

Full source

instance (priority := 100) OrderIsoClass.toBoundedLatticeHomClass [Lattice α] [Lattice β]
    [BoundedOrder α] [BoundedOrder β] [OrderIsoClass F α β] :
    BoundedLatticeHomClass F α β :=
  { OrderIsoClass.toLatticeHomClass, OrderIsoClass.toBoundedOrderHomClass with }

Order Isomorphisms are Bounded Lattice Homomorphisms

Informal description

For any lattices $\alpha$ and $\beta$ equipped with both top and bottom elements, every order isomorphism between them is a bounded lattice homomorphism. That is, it preserves finite suprema, finite infima, the top element $\top$, and the bottom element $\bot$.

Disjoint.map theorem

 [OrderBot α] [OrderBot β] [BotHomClass F α β] [InfHomClass F α β] {a b : α} (f : F) (h : Disjoint a b) :
  Disjoint (f a) (f b)

Full source

theorem Disjoint.map [OrderBot α] [OrderBot β] [BotHomClass F α β] [InfHomClass F α β] {a b : α}
    (f : F) (h : Disjoint a b) : Disjoint (f a) (f b) := by
  rw [disjoint_iff, ← map_inf, h.eq_bot, map_bot]

Preservation of Disjointness under Bottom and Inf-Preserving Morphisms

Informal description

Let $\alpha$ and $\beta$ be ordered sets with bottom elements $\bot_\alpha$ and $\bot_\beta$ respectively. Let $F$ be a type of morphisms from $\alpha$ to $\beta$ that preserve the bottom element and finite infima. Given two elements $a, b \in \alpha$ that are disjoint (i.e., $a \sqcap b = \bot_\alpha$) and a morphism $f \in F$, then $f(a)$ and $f(b)$ are disjoint in $\beta$ (i.e., $f(a) \sqcap f(b) = \bot_\beta$).

Codisjoint.map theorem

 [OrderTop α] [OrderTop β] [TopHomClass F α β] [SupHomClass F α β] {a b : α} (f : F) (h : Codisjoint a b) :
  Codisjoint (f a) (f b)

Full source

theorem Codisjoint.map [OrderTop α] [OrderTop β] [TopHomClass F α β] [SupHomClass F α β] {a b : α}
    (f : F) (h : Codisjoint a b) : Codisjoint (f a) (f b) := by
  rw [codisjoint_iff, ← map_sup, h.eq_top, map_top]

Preservation of Codisjointness under Top and Sup-Preserving Morphisms

Informal description

Let $\alpha$ and $\beta$ be ordered sets with top elements $\top_\alpha$ and $\top_\beta$ respectively. Let $F$ be a type of morphisms from $\alpha$ to $\beta$ that preserve the top element and finite suprema. Given two elements $a, b \in \alpha$ that are codisjoint (i.e., $a \sqcup b = \top_\alpha$) and a morphism $f \in F$, then $f(a)$ and $f(b)$ are codisjoint in $\beta$ (i.e., $f(a) \sqcup f(b) = \top_\beta$).

IsCompl.map theorem

 [BoundedOrder α] [BoundedOrder β] [BoundedLatticeHomClass F α β] {a b : α} (f : F) (h : IsCompl a b) :
  IsCompl (f a) (f b)

Full source

theorem IsCompl.map [BoundedOrder α] [BoundedOrder β] [BoundedLatticeHomClass F α β] {a b : α}
    (f : F) (h : IsCompl a b) : IsCompl (f a) (f b) :=
  ⟨h.1.map _, h.2.map _⟩

Preservation of Complements under Bounded Lattice Homomorphisms

Informal description

Let $\alpha$ and $\beta$ be bounded lattices, and let $F$ be a type of bounded lattice homomorphisms from $\alpha$ to $\beta$. For any two elements $a, b \in \alpha$ that are complements (i.e., $a \sqcap b = \bot_\alpha$ and $a \sqcup b = \top_\alpha$) and any homomorphism $f \in F$, the images $f(a)$ and $f(b)$ are complements in $\beta$ (i.e., $f(a) \sqcap f(b) = \bot_\beta$ and $f(a) \sqcup f(b) = \top_\beta$).

map_compl' theorem

(a : α) : f aᶜ = (f a)ᶜ

Full source

/-- Special case of `map_compl` for boolean algebras. -/
theorem map_compl' (a : α) : f aᶜ = (f a)ᶜ :=
  (isCompl_compl.map _).compl_eq.symm

Preservation of Complements under Bounded Lattice Homomorphisms

Informal description

Let $\alpha$ and $\beta$ be Boolean algebras, and let $f$ be a bounded lattice homomorphism from $\alpha$ to $\beta$. For any element $a \in \alpha$, the homomorphism $f$ preserves complements, i.e., $f(a^\complement) = (f(a))^\complement$.

map_sdiff' theorem

(a b : α) : f (a \ b) = f a \ f b

Full source

/-- Special case of `map_sdiff` for boolean algebras. -/
theorem map_sdiff' (a b : α) : f (a \ b) = f a \ f b := by
  rw [sdiff_eq, sdiff_eq, map_inf, map_compl']

Preservation of Relative Complement under Bounded Lattice Homomorphisms

Informal description

Let $\alpha$ and $\beta$ be Boolean algebras, and let $f$ be a bounded lattice homomorphism from $\alpha$ to $\beta$. For any elements $a, b \in \alpha$, the homomorphism $f$ preserves the relative complement (set difference), i.e., $f(a \setminus b) = f(a) \setminus f(b)$.

map_symmDiff' theorem

(a b : α) : f (a ∆ b) = f a ∆ f b

Full source

/-- Special case of `map_symmDiff` for boolean algebras. -/
theorem map_symmDiff' (a b : α) : f (a ∆ b) = f a ∆ f b := by
  rw [symmDiff, symmDiff, map_sup, map_sdiff', map_sdiff']

Preservation of Symmetric Difference under Bounded Lattice Homomorphisms

Informal description

Let $\alpha$ and $\beta$ be Boolean algebras, and let $f$ be a bounded lattice homomorphism from $\alpha$ to $\beta$. For any elements $a, b \in \alpha$, the homomorphism $f$ preserves the symmetric difference operation, i.e., $f(a \triangle b) = f(a) \triangle f(b)$, where $\triangle$ denotes the symmetric difference operation.

instCoeTCSupBotHomOfSupBotHomClass instance

[Max α] [Max β] [Bot α] [Bot β] [SupBotHomClass F α β] : CoeTC F (SupBotHom α β)

Full source

instance [Max α] [Max β] [Bot α] [Bot β] [SupBotHomClass F α β] : CoeTC F (SupBotHom α β) :=
  ⟨fun f => ⟨f, map_bot f⟩⟩

Canonical View of Supremum-Preserving Morphisms as `SupBotHom`

Informal description

For any types $\alpha$ and $\beta$ equipped with a maximum operation $\sqcup$ and a bottom element $\bot$, and any type $F$ of finitary supremum-preserving morphisms from $\alpha$ to $\beta$, there is a canonical way to view elements of $F$ as `SupBotHom` morphisms.

instCoeTCInfTopHomOfInfTopHomClass instance

[Min α] [Min β] [Top α] [Top β] [InfTopHomClass F α β] : CoeTC F (InfTopHom α β)

Full source

instance [Min α] [Min β] [Top α] [Top β] [InfTopHomClass F α β] : CoeTC F (InfTopHom α β) :=
  ⟨fun f => ⟨f, map_top f⟩⟩

Canonical View of Infimum-Preserving Morphisms as `InfTopHom`

Informal description

For any types $\alpha$ and $\beta$ equipped with a minimum operation $\sqcap$ and a top element $\top$, and any type $F$ of finitary infimum-preserving morphisms from $\alpha$ to $\beta$, there is a canonical way to view elements of $F$ as `InfTopHom` morphisms.

instCoeTCBoundedLatticeHomOfBoundedLatticeHomClass instance

 [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] [BoundedLatticeHomClass F α β] :
  CoeTC F (BoundedLatticeHom α β)

Full source

instance [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] [BoundedLatticeHomClass F α β] :
    CoeTC F (BoundedLatticeHom α β) :=
  ⟨fun f =>
    { (f : LatticeHom α β) with
      toFun := f
      map_top' := map_top f
      map_bot' := map_bot f }⟩

Canonical View of Bounded Lattice Homomorphisms

Informal description

For any lattices $\alpha$ and $\beta$ with bounded orders (i.e., having both a greatest element $\top$ and a least element $\bot$), and any type $F$ of bounded lattice homomorphisms from $\alpha$ to $\beta$, there is a canonical way to view elements of $F$ as bounded lattice homomorphisms $\text{BoundedLatticeHom}(\alpha, \beta)$. This means that any function $f \in F$ preserves the lattice operations $\sqcup$ (supremum) and $\sqcap$ (infimum), as well as the top and bottom elements.

SupBotHom.toBotHom definition

(f : SupBotHom α β) : BotHom α β

Full source

/-- Reinterpret a `SupBotHom` as a `BotHom`. -/
def toBotHom (f : SupBotHom α β) : BotHom α β :=
  { f with }

Reinterpretation of supremum-preserving homomorphism as bottom-preserving homomorphism

Informal description

Given a finitary supremum-preserving homomorphism $f$ between types $\alpha$ and $\beta$ (both equipped with a supremum operation $\sqcup$ and a bottom element $\bot$), this function reinterprets $f$ as a bottom-preserving homomorphism. That is, it preserves the bottom element $\bot$ while discarding the information about preserving suprema.

SupBotHom.instFunLike instance

: FunLike (SupBotHom α β) α β

Full source

instance : FunLike (SupBotHom α β) α β where
  coe f := f.toFun
  coe_injective' f g h := by
    obtain ⟨⟨_, _⟩, _⟩ := f
    obtain ⟨⟨_, _⟩, _⟩ := g
    congr

Function-Like Structure of Supremum-Preserving Homomorphisms

Informal description

For any two types $\alpha$ and $\beta$ equipped with a supremum operation $\sqcup$ and a bottom element $\bot$, the type of finitary supremum-preserving homomorphisms $\text{SupBotHom}(\alpha, \beta)$ is naturally a function-like type, meaning its elements can be coerced to functions from $\alpha$ to $\beta$ in an injective way.

SupBotHom.instSupBotHomClass instance

: SupBotHomClass (SupBotHom α β) α β

Full source

instance : SupBotHomClass (SupBotHom α β) α β where
  map_sup f := f.map_sup'
  map_bot f := f.map_bot'

Class of Supremum and Bottom-Preserving Homomorphisms

Informal description

For any two types $\alpha$ and $\beta$ equipped with a supremum operation $\sqcup$ and a bottom element $\bot$, the type of finitary supremum-preserving homomorphisms $\text{SupBotHom}(\alpha, \beta)$ forms a class of morphisms that preserve both the supremum operation and the bottom element.

SupBotHom.toFun_eq_coe theorem

(f : SupBotHom α β) : f.toFun = f

Full source

lemma toFun_eq_coe (f : SupBotHom α β) : f.toFun = f := rfl

Equality of Underlying Function and Coercion for Supremum-Preserving Homomorphisms

Informal description

For any finitary supremum-preserving homomorphism $f : \text{SupBotHom}(\alpha, \beta)$, the underlying function $f.\text{toFun}$ is equal to the coercion of $f$ to a function.

SupBotHom.coe_toSupHom theorem

(f : SupBotHom α β) : ⇑f.toSupHom = f

Full source

@[simp] lemma coe_toSupHom (f : SupBotHom α β) : ⇑f.toSupHom = f := rfl

Equality of Supremum-Preserving Part and Original Homomorphism

Informal description

For any finitary supremum-preserving homomorphism $f \colon \alpha \to \beta$ between types $\alpha$ and $\beta$ equipped with a supremum operation $\sqcup$ and a bottom element $\bot$, the underlying function of the supremum-preserving part of $f$ (denoted $f.\text{toSupHom}$) is equal to $f$ itself when viewed as a function.

SupBotHom.coe_toBotHom theorem

(f : SupBotHom α β) : ⇑f.toBotHom = f

Full source

@[simp] lemma coe_toBotHom (f : SupBotHom α β) : ⇑f.toBotHom = f := rfl

Equality of Bottom-Preserving Part and Original Supremum-Preserving Homomorphism

Informal description

For any finitary supremum-preserving homomorphism $f \colon \alpha \to \beta$ between types $\alpha$ and $\beta$ equipped with a supremum operation $\sqcup$ and a bottom element $\bot$, the underlying function of the bottom-preserving part of $f$ (denoted $f.\text{toBotHom}$) is equal to $f$ itself when viewed as a function.

SupBotHom.coe_mk theorem

(f : SupHom α β) (hf) : ⇑(mk f hf) = f

Full source

@[simp] lemma coe_mk (f : SupHom α β) (hf) : ⇑(mk f hf) = f := rfl

Underlying Function of Constructed Supremum-Bottom Homomorphism

Informal description

For any supremum-preserving homomorphism $f \colon \alpha \to \beta$ between types $\alpha$ and $\beta$ equipped with a supremum operation $\sqcup$, and any proof $hf$ that $f$ preserves the bottom element $\bot$, the underlying function of the constructed `SupBotHom` is equal to $f$. That is, if $g = \text{mk}(f, hf)$, then $g = f$ as functions.

SupBotHom.ext theorem

{f g : SupBotHom α β} (h : ∀ a, f a = g a) : f = g

Full source

@[ext]
theorem ext {f g : SupBotHom α β} (h : ∀ a, f a = g a) : f = g :=
  DFunLike.ext f g h

Extensionality of Supremum-Bottom-Preserving Homomorphisms

Informal description

For any two finitary supremum-preserving homomorphisms $f, g \colon \alpha \to \beta$ between types $\alpha$ and $\beta$ equipped with a supremum operation $\sqcup$ and a bottom element $\bot$, if $f(a) = g(a)$ for all $a \in \alpha$, then $f = g$.

SupBotHom.copy definition

(f : SupBotHom α β) (f' : α → β) (h : f' = f) : SupBotHom α β

Full source

/-- Copy of a `SupBotHom` with a new `toFun` equal to the old one. Useful to fix definitional
equalities. -/
protected def copy (f : SupBotHom α β) (f' : α → β) (h : f' = f) : SupBotHom α β :=
  { f.toBotHom.copy f' h with toSupHom := f.toSupHom.copy f' h }

Copy of a supremum-bottom-preserving homomorphism with a new underlying function

Informal description

Given a finitary supremum-preserving homomorphism $f \colon \alpha \to \beta$ (where $\alpha$ and $\beta$ are types equipped with a supremum operation $\sqcup$ and a bottom element $\bot$) and a function $f' \colon \alpha \to \beta$ that is definitionally equal to $f$, this constructs a new supremum-preserving homomorphism with $f'$ as its underlying function, while preserving both the supremum and bottom-preserving properties of $f$.

SupBotHom.coe_copy theorem

(f : SupBotHom α β) (f' : α → β) (h : f' = f) : ⇑(f.copy f' h) = f'

Full source

@[simp]
theorem coe_copy (f : SupBotHom α β) (f' : α → β) (h : f' = f) : ⇑(f.copy f' h) = f' :=
  rfl

Underlying Function of Copied Supremum-Bottom-Preserving Homomorphism

Informal description

Let $f \colon \alpha \to \beta$ be a finitary supremum-preserving homomorphism between types $\alpha$ and $\beta$ equipped with a supremum operation $\sqcup$ and a bottom element $\bot$. Given a function $f' \colon \alpha \to \beta$ such that $f' = f$, the underlying function of the copy of $f$ with $f'$ as its function is equal to $f'$.

SupBotHom.copy_eq theorem

(f : SupBotHom α β) (f' : α → β) (h : f' = f) : f.copy f' h = f

Full source

theorem copy_eq (f : SupBotHom α β) (f' : α → β) (h : f' = f) : f.copy f' h = f :=
  DFunLike.ext' h

Copy of a Supremum-Bottom-Preserving Homomorphism Equals Original

Informal description

Let $f \colon \alpha \to \beta$ be a finitary supremum-preserving homomorphism between types $\alpha$ and $\beta$ equipped with a supremum operation $\sqcup$ and a bottom element $\bot$. For any function $f' \colon \alpha \to \beta$ such that $f' = f$, the copy of $f$ with underlying function $f'$ is equal to $f$ itself.

SupBotHom.id definition

: SupBotHom α α

Full source

/-- `id` as a `SupBotHom`. -/
@[simps]
protected def id : SupBotHom α α :=
  ⟨SupHom.id α, rfl⟩

Identity finitary supremum-preserving homomorphism

Informal description

The identity function on a type $\alpha$ equipped with a supremum operation $\sqcup$ and a bottom element $\bot$, viewed as a finitary supremum-preserving homomorphism. It preserves both the supremum operation and the bottom element, satisfying $\text{id}(x \sqcup y) = \text{id}(x) \sqcup \text{id}(y)$ for any $x, y \in \alpha$ and $\text{id}(\bot) = \bot$.

SupBotHom.instInhabited instance

: Inhabited (SupBotHom α α)

Full source

instance : Inhabited (SupBotHom α α) :=
  ⟨SupBotHom.id α⟩

Inhabitedness of Finitary Supremum-Preserving Homomorphisms

Informal description

For any type $\alpha$ equipped with a supremum operation $\sqcup$ and a bottom element $\bot$, the type of finitary supremum-preserving homomorphisms from $\alpha$ to itself is inhabited (by the identity homomorphism).

SupBotHom.coe_id theorem

: ⇑(SupBotHom.id α) = id

Full source

@[simp, norm_cast]
theorem coe_id : ⇑(SupBotHom.id α) = id :=
  rfl

Identity Supremum-Preserving Homomorphism Coerces to Identity Function

Informal description

The coercion of the identity finitary supremum-preserving homomorphism on a type $\alpha$ (equipped with a supremum operation $\sqcup$ and a bottom element $\bot$) is equal to the identity function on $\alpha$.

SupBotHom.id_apply theorem

(a : α) : SupBotHom.id α a = a

Full source

@[simp]
theorem id_apply (a : α) : SupBotHom.id α a = a :=
  rfl

Identity Finitary Supremum-Preserving Homomorphism Acts as Identity Function

Informal description

For any element $a$ in a type $\alpha$ equipped with a supremum operation $\sqcup$ and a bottom element $\bot$, the identity finitary supremum-preserving homomorphism evaluated at $a$ is equal to $a$ itself, i.e., $\text{id}(a) = a$.

SupBotHom.comp definition

(f : SupBotHom β γ) (g : SupBotHom α β) : SupBotHom α γ

Full source

/-- Composition of `SupBotHom`s as a `SupBotHom`. -/
def comp (f : SupBotHom β γ) (g : SupBotHom α β) : SupBotHom α γ :=
  { f.toSupHom.comp g.toSupHom, f.toBotHom.comp g.toBotHom with }

Composition of finitary supremum-preserving homomorphisms

Informal description

The composition of two finitary supremum-preserving homomorphisms $ f : \beta \to \gamma $ and $ g : \alpha \to \beta $ is a finitary supremum-preserving homomorphism $ f \circ g : \alpha \to \gamma $, where the composition preserves both the supremum operation and the bottom element. That is, $(f \circ g)(a \sqcup b) = f(g(a)) \sqcup f(g(b))$ for all $ a, b \in \alpha $, and $(f \circ g)(\bot) = \bot$.

SupBotHom.coe_comp theorem

(f : SupBotHom β γ) (g : SupBotHom α β) : (f.comp g : α → γ) = f ∘ g

Full source

@[simp]
theorem coe_comp (f : SupBotHom β γ) (g : SupBotHom α β) : (f.comp g : α → γ) = f ∘ g :=
  rfl

Composition of Finitary Supremum-Preserving Homomorphisms as Function Composition

Informal description

For any two finitary supremum-preserving homomorphisms $f \colon \beta \to \gamma$ and $g \colon \alpha \to \beta$, the underlying function of their composition $f \circ g \colon \alpha \to \gamma$ is equal to the composition of their underlying functions, i.e., $(f \circ g)(a) = f(g(a))$ for all $a \in \alpha$.

SupBotHom.comp_apply theorem

(f : SupBotHom β γ) (g : SupBotHom α β) (a : α) : (f.comp g) a = f (g a)

Full source

@[simp]
theorem comp_apply (f : SupBotHom β γ) (g : SupBotHom α β) (a : α) : (f.comp g) a = f (g a) :=
  rfl

Application of Composition of Supremum-Preserving Homomorphisms

Informal description

For any finitary supremum-preserving homomorphisms $f \colon \beta \to \gamma$ and $g \colon \alpha \to \beta$, and for any element $a \in \alpha$, the application of the composition $f \circ g$ to $a$ is equal to the application of $f$ to $g(a)$, i.e., $(f \circ g)(a) = f(g(a))$.

SupBotHom.comp_assoc theorem

(f : SupBotHom γ δ) (g : SupBotHom β γ) (h : SupBotHom α β) : (f.comp g).comp h = f.comp (g.comp h)

Full source

@[simp]
theorem comp_assoc (f : SupBotHom γ δ) (g : SupBotHom β γ) (h : SupBotHom α β) :
    (f.comp g).comp h = f.comp (g.comp h) :=
  rfl

Associativity of Composition for Supremum-Preserving Homomorphisms

Informal description

For any finitary supremum-preserving homomorphisms $f : \gamma \to \delta$, $g : \beta \to \gamma$, and $h : \alpha \to \beta$, the composition operation is associative, i.e., $(f \circ g) \circ h = f \circ (g \circ h)$.

SupBotHom.comp_id theorem

(f : SupBotHom α β) : f.comp (SupBotHom.id α) = f

Full source

@[simp] theorem comp_id (f : SupBotHom α β) : f.comp (SupBotHom.id α) = f := rfl

Right Identity Law for Composition of Supremum-Preserving Homomorphisms

Informal description

For any finitary supremum-preserving homomorphism $f$ from a type $\alpha$ to a type $\beta$, the composition of $f$ with the identity homomorphism on $\alpha$ is equal to $f$ itself, i.e., $f \circ \text{id} = f$.

SupBotHom.id_comp theorem

(f : SupBotHom α β) : (SupBotHom.id β).comp f = f

Full source

@[simp] theorem id_comp (f : SupBotHom α β) : (SupBotHom.id β).comp f = f := rfl

Identity Homomorphism Composition: $\text{id}_\beta \circ f = f$

Informal description

For any finitary supremum-preserving homomorphism $f : \alpha \to \beta$, the composition of the identity homomorphism on $\beta$ with $f$ equals $f$ itself, i.e., $\text{id}_\beta \circ f = f$.

SupBotHom.cancel_right theorem

{g₁ g₂ : SupBotHom β γ} {f : SupBotHom α β} (hf : Surjective f) : g₁.comp f = g₂.comp f ↔ g₁ = g₂

Full source

@[simp]
theorem cancel_right {g₁ g₂ : SupBotHom β γ} {f : SupBotHom α β} (hf : Surjective f) :
    g₁.comp f = g₂.comp f ↔ g₁ = g₂ :=
  ⟨fun h => ext <| hf.forall.2 <| DFunLike.ext_iff.1 h, fun h => congr_arg₂ _ h rfl⟩

Right Cancellation Property for Composition of Supremum-Preserving Homomorphisms

Informal description

Let $f \colon \alpha \to \beta$ be a surjective finitary supremum-preserving homomorphism between types $\alpha$ and $\beta$ equipped with a supremum operation $\sqcup$ and a bottom element $\bot$. For any two finitary supremum-preserving homomorphisms $g_1, g_2 \colon \beta \to \gamma$, the compositions $g_1 \circ f$ and $g_2 \circ f$ are equal if and only if $g_1 = g_2$.

SupBotHom.cancel_left theorem

{g : SupBotHom β γ} {f₁ f₂ : SupBotHom α β} (hg : Injective g) : g.comp f₁ = g.comp f₂ ↔ f₁ = f₂

Full source

@[simp]
theorem cancel_left {g : SupBotHom β γ} {f₁ f₂ : SupBotHom α β} (hg : Injective g) :
    g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
  ⟨fun h => SupBotHom.ext fun a => hg <| by rw [← comp_apply, h, comp_apply], congr_arg _⟩

Left Cancellation Property for Composition of Supremum-Preserving Homomorphisms

Informal description

Let $g \colon \beta \to \gamma$ be an injective finitary supremum-preserving homomorphism between types $\beta$ and $\gamma$ equipped with a supremum operation $\sqcup$ and a bottom element $\bot$. For any two finitary supremum-preserving homomorphisms $f_1, f_2 \colon \alpha \to \beta$, the compositions $g \circ f_1$ and $g \circ f_2$ are equal if and only if $f_1 = f_2$.

SupBotHom.instMax instance

: Max (SupBotHom α β)

Full source

instance : Max (SupBotHom α β) :=
  ⟨fun f g => { f.toBotHom ⊔ g.toBotHom with toSupHom := f.toSupHom ⊔ g.toSupHom }⟩

Maximum Operation on Finitary Supremum-Preserving Homomorphisms

Informal description

For any two types $\alpha$ and $\beta$ equipped with a maximum operation $\sqcup$ and a bottom element $\bot$, the type of finitary supremum-preserving homomorphisms $\mathrm{SupBotHom}(\alpha, \beta)$ is itself equipped with a maximum operation.

SupBotHom.instSemilatticeSup instance

: SemilatticeSup (SupBotHom α β)

Full source

instance : SemilatticeSup (SupBotHom α β) :=
  (DFunLike.coe_injective.semilatticeSup _) fun _ _ => rfl

Semilattice Structure on Finitary Supremum-Preserving Homomorphisms

Informal description

For any two types $\alpha$ and $\beta$ equipped with a maximum operation $\sqcup$ and a bottom element $\bot$, the type of finitary supremum-preserving homomorphisms $\mathrm{SupBotHom}(\alpha, \beta)$ forms a semilattice with a supremum operation. This means that for any two homomorphisms $f$ and $g$ in $\mathrm{SupBotHom}(\alpha, \beta)$, their supremum $f \sqcup g$ is also a finitary supremum-preserving homomorphism, and this operation is associative, commutative, and idempotent.

SupBotHom.instOrderBot instance

: OrderBot (SupBotHom α β)

Full source

instance : OrderBot (SupBotHom α β) where
  bot := ⟨⊥, rfl⟩
  bot_le _ _ := bot_le

Bottom Element in the Order of Supremum-Preserving Homomorphisms

Informal description

For any two types $\alpha$ and $\beta$ equipped with a supremum operation $\sqcup$ and a bottom element $\bot$, the type of finitary supremum-preserving homomorphisms $\mathrm{SupBotHom}(\alpha, \beta)$ forms an order with a bottom element. The bottom element is given by the constant function that maps every element of $\alpha$ to $\bot$ in $\beta$, and this is indeed the least element in the pointwise order on homomorphisms.

SupBotHom.coe_sup theorem

(f g : SupBotHom α β) : DFunLike.coe (f ⊔ g) = f ⊔ g

Full source

@[simp]
theorem coe_sup (f g : SupBotHom α β) : DFunLike.coe (f ⊔ g) = f ⊔ g :=
  rfl

Pointwise Supremum of Supremum-Preserving Homomorphisms

Informal description

For any two finitary supremum-preserving homomorphisms $f, g : \alpha \to \beta$ between types $\alpha$ and $\beta$ equipped with a supremum operation $\sqcup$ and a bottom element $\bot$, the underlying function of the supremum $f \sqcup g$ is equal to the pointwise supremum of the functions $f$ and $g$. That is, $(f \sqcup g)(a) = f(a) \sqcup g(a)$ for all $a \in \alpha$.

SupBotHom.coe_bot theorem

: ⇑(⊥ : SupBotHom α β) = ⊥

Full source

@[simp]
theorem coe_bot : ⇑(⊥ : SupBotHom α β) = ⊥ :=
  rfl

Bottom Homomorphism is Constant Bottom Function

Informal description

For any two types $\alpha$ and $\beta$ equipped with a supremum operation $\sqcup$ and a bottom element $\bot$, the underlying function of the bottom element in the order of finitary supremum-preserving homomorphisms $\mathrm{SupBotHom}(\alpha, \beta)$ is equal to the constant function that maps every element of $\alpha$ to $\bot$ in $\beta$. In other words, $(\bot : \mathrm{SupBotHom}(\alpha, \beta))(a) = \bot$ for all $a \in \alpha$.

SupBotHom.sup_apply theorem

(f g : SupBotHom α β) (a : α) : (f ⊔ g) a = f a ⊔ g a

Full source

@[simp]
theorem sup_apply (f g : SupBotHom α β) (a : α) : (f ⊔ g) a = f a ⊔ g a :=
  rfl

Supremum-Preserving Homomorphism Preserves Pointwise Supremum

Informal description

For any two finitary supremum-preserving homomorphisms $f, g \colon \alpha \to \beta$ between types $\alpha$ and $\beta$ equipped with a maximum operation $\sqcup$ and a bottom element $\bot$, and for any element $a \in \alpha$, the evaluation of the supremum of $f$ and $g$ at $a$ is equal to the supremum of $f(a)$ and $g(a)$, i.e., $(f \sqcup g)(a) = f(a) \sqcup g(a)$.

SupBotHom.bot_apply theorem

(a : α) : (⊥ : SupBotHom α β) a = ⊥

Full source

@[simp]
theorem bot_apply (a : α) : (⊥ : SupBotHom α β) a = ⊥ :=
  rfl

Bottom Homomorphism Evaluates to Bottom Element

Informal description

For any element $a$ in a type $\alpha$ equipped with a bottom element $\bot$, the evaluation of the bottom homomorphism (the constant function mapping every element to $\bot$) at $a$ is equal to $\bot$.

SupBotHom.subtypeVal definition

 {P : β → Prop} (Pbot : P ⊥) (Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y)) :
  letI := Subtype.orderBot Pbot
  letI := Subtype.semilatticeSup Psup
  SupBotHom { x : β // P x } β

Full source

/-- `Subtype.val` as a `SupBotHom`. -/
def subtypeVal {P : β → Prop}
    (Pbot : P ⊥) (Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y)) :
    letI := Subtype.orderBot Pbot
    letI := Subtype.semilatticeSup Psup
    SupBotHom {x : β // P x} β :=
  letI := Subtype.orderBot Pbot
  letI := Subtype.semilatticeSup Psup
  .mk (SupHom.subtypeVal Psup) (by simp [Subtype.coe_bot Pbot])

Canonical supremum- and bottom-preserving homomorphism from a subtype

Informal description

Given a predicate $ P $ on a type $ \beta $ such that $ P $ holds for the bottom element $ \bot $ and is closed under the supremum operation $ \sqcup $, the function `SupBotHom.subtypeVal` is the canonical supremum- and bottom-preserving homomorphism from the subtype $ \{x : \beta \mid P x\} $ to $ \beta $. Here, the subtype is equipped with the induced order and lattice structure from $ \beta $.

SupBotHom.subtypeVal_apply theorem

 {P : β → Prop} (Pbot : P ⊥) (Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y)) (x : { x : β // P x }) :
  subtypeVal Pbot Psup x = x

Full source

@[simp]
lemma subtypeVal_apply {P : β → Prop}
    (Pbot : P ⊥) (Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y)) (x : {x : β // P x}) :
    subtypeVal Pbot Psup x = x := rfl

Canonical Subtype Homomorphism Acts as Identity on Subtype Elements

Informal description

Let $\beta$ be a type with a supremum operation $\sqcup$ and a bottom element $\bot$, and let $P$ be a predicate on $\beta$ such that $P(\bot)$ holds and $P$ is closed under $\sqcup$. For any element $x$ in the subtype $\{x \in \beta \mid P(x)\}$, the canonical supremum- and bottom-preserving homomorphism `subtypeVal` from the subtype to $\beta$ satisfies `subtypeVal Pbot Psup x = x`.

SupBotHom.subtypeVal_coe theorem

 {P : β → Prop} (Pbot : P ⊥) (Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y)) : ⇑(subtypeVal Pbot Psup) = Subtype.val

Full source

@[simp]
lemma subtypeVal_coe {P : β → Prop}
    (Pbot : P ⊥) (Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y)) :
    ⇑(subtypeVal Pbot Psup) = Subtype.val := rfl

Canonical SupBotHom Subtype Projection

Informal description

Given a predicate $P$ on a type $\beta$ such that $P(\bot)$ holds and $P$ is closed under the supremum operation $\sqcup$, the underlying function of the canonical supremum- and bottom-preserving homomorphism from the subtype $\{x \in \beta \mid P(x)\}$ to $\beta$ is equal to the subtype projection function.

InfTopHom.toTopHom definition

(f : InfTopHom α β) : TopHom α β

Full source

/-- Reinterpret an `InfTopHom` as a `TopHom`. -/
def toTopHom (f : InfTopHom α β) : TopHom α β :=
  { f with }

Reinterpretation of infimum-preserving homomorphism as top-preserving function

Informal description

Given a finitary infimum-preserving homomorphism $f$ from a type $\alpha$ to a type $\beta$ (both equipped with infimum operations $\sqcap$ and top elements $\top$), this function reinterprets $f$ as a top-preserving function, i.e., a function that preserves the top element $\top$.

InfTopHom.instFunLike instance

: FunLike (InfTopHom α β) α β

Full source

instance : FunLike (InfTopHom α β) α β where
  coe f := f.toFun
  coe_injective' f g h := by
    obtain ⟨⟨_, _⟩, _⟩ := f
    obtain ⟨⟨_, _⟩, _⟩ := g
    congr

Function-Like Structure for Infimum-Preserving Homomorphisms

Informal description

For any types $\alpha$ and $\beta$ equipped with infimum operations $\sqcap$ and top elements $\top$, the type of finitary infimum-preserving homomorphisms $\text{InfTopHom}(\alpha, \beta)$ has a function-like structure, meaning each homomorphism can be treated as a function from $\alpha$ to $\beta$.

InfTopHom.instInfTopHomClass instance

: InfTopHomClass (InfTopHom α β) α β

Full source

instance : InfTopHomClass (InfTopHom α β) α β where
  map_inf f := f.map_inf'
  map_top f := f.map_top'

InfTopHom as InfTopHomClass Instance

Informal description

For any types $\alpha$ and $\beta$ equipped with infimum operations $\sqcap$ and top elements $\top$, the type of finitary infimum-preserving homomorphisms $\text{InfTopHom}(\alpha, \beta)$ forms an instance of the class $\text{InfTopHomClass}$, meaning each homomorphism in this type preserves both the infimum operation and the top element.

InfTopHom.toFun_eq_coe theorem

(f : InfTopHom α β) : f.toFun = f

Full source

theorem toFun_eq_coe (f : InfTopHom α β) : f.toFun = f := rfl

Underlying Function of Infimum-Preserving Homomorphism Equals Itself

Informal description

For any finitary infimum-preserving homomorphism $f$ from $\alpha$ to $\beta$, the underlying function of $f$ is equal to $f$ itself, i.e., $f.\text{toFun} = f$.

InfTopHom.coe_toInfHom theorem

(f : InfTopHom α β) : ⇑f.toInfHom = f

Full source

@[simp] lemma coe_toInfHom (f : InfTopHom α β) : ⇑f.toInfHom = f := rfl

Infimum-Preserving Component of InfTopHom Equals Itself

Informal description

For any finitary infimum-preserving homomorphism $f$ from $\alpha$ to $\beta$, the underlying function of the infimum-preserving part of $f$ is equal to $f$ itself, i.e., $f.\text{toInfHom} = f$.

InfTopHom.coe_toTopHom theorem

(f : InfTopHom α β) : ⇑f.toTopHom = f

Full source

@[simp] lemma coe_toTopHom (f : InfTopHom α β) : ⇑f.toTopHom = f := rfl

Top-preserving component of infimum-top homomorphism equals original function

Informal description

For any finitary infimum-preserving homomorphism $f$ from a type $\alpha$ to a type $\beta$ (both equipped with minimum operations $\sqcap$ and top elements $\top$), the underlying function of the top-preserving component of $f$ is equal to $f$ itself, i.e., $f.\text{toTopHom} = f$.

InfTopHom.coe_mk theorem

(f : InfHom α β) (hf) : ⇑(mk f hf) = f

Full source

@[simp] lemma coe_mk (f : InfHom α β) (hf) : ⇑(mk f hf) = f := rfl

Underlying function of constructed infimum-top homomorphism equals original function

Informal description

For any infimum-preserving function $f \colon \alpha \to \beta$ between types with minimum operations, and any proof $hf$ that $f$ preserves the top element, the underlying function of the constructed `InfTopHom` is equal to $f$.

InfTopHom.ext theorem

{f g : InfTopHom α β} (h : ∀ a, f a = g a) : f = g

Full source

@[ext]
theorem ext {f g : InfTopHom α β} (h : ∀ a, f a = g a) : f = g :=
  DFunLike.ext f g h

Extensionality of Infimum-Top Preserving Homomorphisms

Informal description

For any two finitary infimum-preserving homomorphisms $f, g \colon \alpha \to \beta$ between types with minimum operations $\sqcap$ and top elements $\top$, if $f(a) = g(a)$ for all $a \in \alpha$, then $f = g$.

InfTopHom.copy definition

(f : InfTopHom α β) (f' : α → β) (h : f' = f) : InfTopHom α β

Full source

/-- Copy of an `InfTopHom` with a new `toFun` equal to the old one. Useful to fix definitional
equalities. -/
protected def copy (f : InfTopHom α β) (f' : α → β) (h : f' = f) : InfTopHom α β :=
  { f.toTopHom.copy f' h with toInfHom := f.toInfHom.copy f' h }

Copy of a finitary infimum-top preserving homomorphism with new function representation

Informal description

Given a finitary infimum-preserving homomorphism $f \colon \alpha \to \beta$ (where $\alpha$ and $\beta$ are types equipped with infimum operations $\sqcap$ and top elements $\top$) and a function $f' \colon \alpha \to \beta$ that is definitionally equal to $f$, the function `InfTopHom.copy` constructs a new finitary infimum-preserving homomorphism with $f'$ as its underlying function while preserving both the infimum-preserving and top-preserving properties of $f$.

InfTopHom.coe_copy theorem

(f : InfTopHom α β) (f' : α → β) (h : f' = f) : ⇑(f.copy f' h) = f'

Full source

@[simp]
theorem coe_copy (f : InfTopHom α β) (f' : α → β) (h : f' = f) : ⇑(f.copy f' h) = f' :=
  rfl

Underlying function of copied infimum-top preserving homomorphism equals copied function

Informal description

Let $f \colon \alpha \to \beta$ be a finitary infimum-preserving homomorphism between types $\alpha$ and $\beta$ equipped with infimum operations $\sqcap$ and top elements $\top$. Given a function $f' \colon \alpha \to \beta$ such that $f' = f$, the underlying function of the copied homomorphism $f.copy\, f'\, h$ is equal to $f'$.

InfTopHom.copy_eq theorem

(f : InfTopHom α β) (f' : α → β) (h : f' = f) : f.copy f' h = f

Full source

theorem copy_eq (f : InfTopHom α β) (f' : α → β) (h : f' = f) : f.copy f' h = f :=
  DFunLike.ext' h

Copy of Infimum-Top Preserving Homomorphism Equals Original

Informal description

Let $f \colon \alpha \to \beta$ be a finitary infimum-preserving homomorphism between types $\alpha$ and $\beta$ equipped with infimum operations $\sqcap$ and top elements $\top$. For any function $f' \colon \alpha \to \beta$ such that $f' = f$, the copy of $f$ with underlying function $f'$ is equal to $f$ itself. That is, $f.\text{copy}(f', h) = f$ where $h$ is the proof that $f' = f$.

InfTopHom.id definition

: InfTopHom α α

Full source

/-- `id` as an `InfTopHom`. -/
@[simps]
protected def id : InfTopHom α α :=
  ⟨InfHom.id α, rfl⟩

Identity finitary infimum-preserving homomorphism

Informal description

The identity function on a type $\alpha$ equipped with an infimum operation $\sqcap$ and a top element $\top$, viewed as a finitary infimum-preserving homomorphism. This function maps each element to itself, preserves the infimum operation (i.e., $\text{id}(x \sqcap y) = \text{id}(x) \sqcap \text{id}(y)$ for any $x, y \in \alpha$), and preserves the top element (i.e., $\text{id}(\top) = \top$).

InfTopHom.instInhabited instance

: Inhabited (InfTopHom α α)

Full source

instance : Inhabited (InfTopHom α α) :=
  ⟨InfTopHom.id α⟩

Inhabitedness of Finitary Infimum-Preserving Homomorphisms

Informal description

For any type $\alpha$ equipped with an infimum operation $\sqcap$ and a top element $\top$, the type of finitary infimum-preserving homomorphisms from $\alpha$ to itself is inhabited.

InfTopHom.coe_id theorem

: ⇑(InfTopHom.id α) = id

Full source

@[simp, norm_cast]
theorem coe_id : ⇑(InfTopHom.id α) = id :=
  rfl

Identity InfTopHom as Identity Function

Informal description

The underlying function of the identity finitary infimum-preserving homomorphism on a type $\alpha$ is equal to the identity function on $\alpha$.

InfTopHom.id_apply theorem

(a : α) : InfTopHom.id α a = a

Full source

@[simp]
theorem id_apply (a : α) : InfTopHom.id α a = a :=
  rfl

Identity InfTopHom Acts as Identity Function

Informal description

For any element $a$ in a type $\alpha$ equipped with an infimum operation $\sqcap$ and a top element $\top$, the identity finitary infimum-preserving homomorphism evaluated at $a$ equals $a$, i.e., $\text{id}(a) = a$.

InfTopHom.comp definition

(f : InfTopHom β γ) (g : InfTopHom α β) : InfTopHom α γ

Full source

/-- Composition of `InfTopHom`s as an `InfTopHom`. -/
def comp (f : InfTopHom β γ) (g : InfTopHom α β) : InfTopHom α γ :=
  { f.toInfHom.comp g.toInfHom, f.toTopHom.comp g.toTopHom with }

Composition of finitary infimum-preserving homomorphisms

Informal description

The composition of two finitary infimum-preserving homomorphisms $ f \colon \beta \to \gamma $ and $ g \colon \alpha \to \beta $ is a finitary infimum-preserving homomorphism $ f \circ g \colon \alpha \to \gamma $. This means that for any $ a, b \in \alpha $, the composition satisfies $ (f \circ g)(a \sqcap b) = f(g(a)) \sqcap f(g(b)) $ and $ (f \circ g)(\top_\alpha) = \top_\gamma $, where $ \sqcap $ denotes the infimum operation and $ \top $ denotes the top element in the respective lattices.

InfTopHom.coe_comp theorem

(f : InfTopHom β γ) (g : InfTopHom α β) : (f.comp g : α → γ) = f ∘ g

Full source

@[simp]
theorem coe_comp (f : InfTopHom β γ) (g : InfTopHom α β) : (f.comp g : α → γ) = f ∘ g :=
  rfl

Composition of InfTopHoms as Function Composition

Informal description

For any finitary infimum-preserving homomorphisms $f \colon \beta \to \gamma$ and $g \colon \alpha \to \beta$, the underlying function of their composition $f \circ g$ is equal to the composition of their underlying functions, i.e., $(f \circ g)(x) = f(g(x))$ for all $x \in \alpha$.

InfTopHom.comp_apply theorem

(f : InfTopHom β γ) (g : InfTopHom α β) (a : α) : (f.comp g) a = f (g a)

Full source

@[simp]
theorem comp_apply (f : InfTopHom β γ) (g : InfTopHom α β) (a : α) : (f.comp g) a = f (g a) :=
  rfl

Application of Composition of Infimum-Preserving Homomorphisms

Informal description

For any finitary infimum-preserving homomorphisms $f \colon \beta \to \gamma$ and $g \colon \alpha \to \beta$, and any element $a \in \alpha$, the composition $(f \circ g)(a)$ equals $f(g(a))$.

InfTopHom.comp_assoc theorem

(f : InfTopHom γ δ) (g : InfTopHom β γ) (h : InfTopHom α β) : (f.comp g).comp h = f.comp (g.comp h)

Full source

@[simp]
theorem comp_assoc (f : InfTopHom γ δ) (g : InfTopHom β γ) (h : InfTopHom α β) :
    (f.comp g).comp h = f.comp (g.comp h) :=
  rfl

Associativity of Composition for Finitary Infimum-Preserving Homomorphisms

Informal description

For any finitary infimum-preserving homomorphisms $f \colon \gamma \to \delta$, $g \colon \beta \to \gamma$, and $h \colon \alpha \to \beta$, the composition operation satisfies the associativity property $(f \circ g) \circ h = f \circ (g \circ h)$.

InfTopHom.comp_id theorem

(f : InfTopHom α β) : f.comp (InfTopHom.id α) = f

Full source

@[simp] theorem comp_id (f : InfTopHom α β) : f.comp (InfTopHom.id α) = f := rfl

Right Identity Law for Composition of Infimum-Preserving Homomorphisms

Informal description

For any finitary infimum-preserving homomorphism $f \colon \alpha \to \beta$, the composition of $f$ with the identity homomorphism on $\alpha$ equals $f$ itself, i.e., $f \circ \text{id}_\alpha = f$.

InfTopHom.id_comp theorem

(f : InfTopHom α β) : (InfTopHom.id β).comp f = f

Full source

@[simp] theorem id_comp (f : InfTopHom α β) : (InfTopHom.id β).comp f = f := rfl

Right Identity Property for Composition of Infimum-Preserving Homomorphisms

Informal description

For any finitary infimum-preserving homomorphism $f \colon \alpha \to \beta$, the composition of the identity homomorphism on $\beta$ with $f$ equals $f$ itself, i.e., $\text{id}_\beta \circ f = f$.

InfTopHom.cancel_right theorem

{g₁ g₂ : InfTopHom β γ} {f : InfTopHom α β} (hf : Surjective f) : g₁.comp f = g₂.comp f ↔ g₁ = g₂

Full source

@[simp]
theorem cancel_right {g₁ g₂ : InfTopHom β γ} {f : InfTopHom α β} (hf : Surjective f) :
    g₁.comp f = g₂.comp f ↔ g₁ = g₂ :=
  ⟨fun h => ext <| hf.forall.2 <| DFunLike.ext_iff.1 h, fun h => congr_arg₂ _ h rfl⟩

Right Cancellation Property for Composition of Infimum-Preserving Homomorphisms

Informal description

Let $f \colon \alpha \to \beta$ be a surjective finitary infimum-preserving homomorphism, and let $g_1, g_2 \colon \beta \to \gamma$ be finitary infimum-preserving homomorphisms. Then the compositions $g_1 \circ f$ and $g_2 \circ f$ are equal if and only if $g_1 = g_2$.

InfTopHom.cancel_left theorem

{g : InfTopHom β γ} {f₁ f₂ : InfTopHom α β} (hg : Injective g) : g.comp f₁ = g.comp f₂ ↔ f₁ = f₂

Full source

@[simp]
theorem cancel_left {g : InfTopHom β γ} {f₁ f₂ : InfTopHom α β} (hg : Injective g) :
    g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
  ⟨fun h => InfTopHom.ext fun a => hg <| by rw [← comp_apply, h, comp_apply], congr_arg _⟩

Left Cancellation Property for Composition of Infimum-Preserving Homomorphisms

Informal description

Let $g \colon \beta \to \gamma$ be an injective finitary infimum-preserving homomorphism, and let $f_1, f_2 \colon \alpha \to \beta$ be finitary infimum-preserving homomorphisms. Then the compositions $g \circ f_1$ and $g \circ f_2$ are equal if and only if $f_1 = f_2$.

InfTopHom.instMin instance

: Min (InfTopHom α β)

Full source

instance : Min (InfTopHom α β) :=
  ⟨fun f g => { f.toTopHom ⊓ g.toTopHom with toInfHom := f.toInfHom ⊓ g.toInfHom }⟩

Minimum Operation on Finitary Infimum-Preserving Homomorphisms

Informal description

For any types $\alpha$ and $\beta$ equipped with infimum operations $\sqcap$ and top elements $\top$, the type of finitary infimum-preserving homomorphisms $\text{InfTopHom}(\alpha, \beta)$ is equipped with a minimum operation.

InfTopHom.instSemilatticeInf instance

: SemilatticeInf (InfTopHom α β)

Full source

instance : SemilatticeInf (InfTopHom α β) :=
  (DFunLike.coe_injective.semilatticeInf _) fun _ _ => rfl

Meet-Semilattice Structure on Finitary Infimum-Preserving Homomorphisms

Informal description

For any types $\alpha$ and $\beta$ equipped with infimum operations $\sqcap$ and top elements $\top$, the type of finitary infimum-preserving homomorphisms $\text{InfTopHom}(\alpha, \beta)$ forms a meet-semilattice. This means that the set of such homomorphisms is equipped with a partial order and a meet operation that is associative, commutative, and idempotent.

InfTopHom.instOrderTop instance

: OrderTop (InfTopHom α β)

Full source

instance : OrderTop (InfTopHom α β) where
  top := ⟨⊤, rfl⟩
  le_top _ _ := le_top

Order with Top Element on Infimum-Preserving Homomorphisms

Informal description

For any types $\alpha$ and $\beta$ equipped with infimum operations $\sqcap$ and top elements $\top$, the type of finitary infimum-preserving homomorphisms $\text{InfTopHom}(\alpha, \beta)$ forms an order with a top element. The top element in this order is the constant function that maps every element of $\alpha$ to $\top \in \beta$.

InfTopHom.coe_inf theorem

(f g : InfTopHom α β) : DFunLike.coe (f ⊓ g) = f ⊓ g

Full source

@[simp]
theorem coe_inf (f g : InfTopHom α β) : DFunLike.coe (f ⊓ g) = f ⊓ g :=
  rfl

Pointwise Infimum of Infimum-Preserving Homomorphisms

Informal description

For any two finitary infimum-preserving homomorphisms $f, g : \text{InfTopHom}(\alpha, \beta)$, the underlying function of their infimum $f \sqcap g$ is equal to the pointwise infimum of the functions $f$ and $g$, i.e., $(f \sqcap g)(a) = f(a) \sqcap g(a)$ for all $a \in \alpha$.

InfTopHom.coe_top theorem

: ⇑(⊤ : InfTopHom α β) = ⊤

Full source

@[simp]
theorem coe_top : ⇑(⊤ : InfTopHom α β) = ⊤ :=
  rfl

Top Infimum-Preserving Homomorphism is Constant Top Function

Informal description

For any types $\alpha$ and $\beta$ equipped with infimum operations $\sqcap$ and top elements $\top$, the underlying function of the top element in $\text{InfTopHom}(\alpha, \beta)$ is equal to the constant top function, i.e., $(\top)(a) = \top$ for all $a \in \alpha$.

InfTopHom.inf_apply theorem

(f g : InfTopHom α β) (a : α) : (f ⊓ g) a = f a ⊓ g a

Full source

@[simp]
theorem inf_apply (f g : InfTopHom α β) (a : α) : (f ⊓ g) a = f a ⊓ g a :=
  rfl

Evaluation of Infimum of Infimum-Preserving Homomorphisms: $(f \sqcap g)(a) = f(a) \sqcap g(a)$

Informal description

For any two finitary infimum-preserving homomorphisms $f, g \colon \alpha \to \beta$ and any element $a \in \alpha$, the evaluation of the infimum homomorphism $f \sqcap g$ at $a$ is equal to the infimum of the evaluations $f(a) \sqcap g(a)$.

InfTopHom.top_apply theorem

(a : α) : (⊤ : InfTopHom α β) a = ⊤

Full source

@[simp]
theorem top_apply (a : α) : (⊤ : InfTopHom α β) a = ⊤ :=
  rfl

Top Homomorphism Evaluates to Top Element: $(\top)(a) = \top$

Informal description

For any element $a$ in a type $\alpha$ equipped with a top element $\top$, the evaluation of the top homomorphism $\top \colon \text{InfTopHom}(\alpha, \beta)$ at $a$ is equal to the top element $\top$ in $\beta$.

InfTopHom.subtypeVal definition

 {P : β → Prop} (Ptop : P ⊤) (Pinf : ∀ ⦃x y : β⦄, P x → P y → P (x ⊓ y)) :
  letI := Subtype.orderTop Ptop
  letI := Subtype.semilatticeInf Pinf
  InfTopHom { x : β // P x } β

Full source

/-- `Subtype.val` as an `InfTopHom`. -/
def subtypeVal {P : β → Prop}
    (Ptop : P ⊤) (Pinf : ∀ ⦃x y : β⦄, P x → P y → P (x ⊓ y)) :
    letI := Subtype.orderTop Ptop
    letI := Subtype.semilatticeInf Pinf
    InfTopHom {x : β // P x} β :=
  letI := Subtype.orderTop Ptop
  letI := Subtype.semilatticeInf Pinf
  .mk (InfHom.subtypeVal Pinf) (by simp [Subtype.coe_top Ptop])

Inclusion map as an infimum- and top-preserving homomorphism

Informal description

Given a predicate $ P $ on a type $ \beta $ with a top element $ \top $ and an infimum operation $ \sqcap $, if $ P(\top) $ holds and $ P $ is closed under $ \sqcap $ (i.e., for any $ x, y \in \beta $, $ P(x) $ and $ P(y) $ imply $ P(x \sqcap y) $), then the canonical inclusion map from the subtype $ \{x \in \beta \mid P(x)\} $ to $ \beta $ is an infimum- and top-preserving homomorphism. Here, the subtype is equipped with the order structure inherited from $ \beta $, including the top element and infimum operation.

InfTopHom.subtypeVal_apply theorem

 {P : β → Prop} (Ptop : P ⊤) (Pinf : ∀ ⦃x y : β⦄, P x → P y → P (x ⊓ y)) (x : { x : β // P x }) :
  subtypeVal Ptop Pinf x = x

Full source

@[simp]
lemma subtypeVal_apply {P : β → Prop}
    (Ptop : P ⊤) (Pinf : ∀ ⦃x y : β⦄, P x → P y → P (x ⊓ y)) (x : {x : β // P x}) :
    subtypeVal Ptop Pinf x = x := rfl

Inclusion Map Acts as Identity on Subtype Elements

Informal description

Let $\beta$ be a type with a top element $\top$ and an infimum operation $\sqcap$, and let $P$ be a predicate on $\beta$ such that $P(\top)$ holds and $P$ is closed under $\sqcap$ (i.e., for any $x, y \in \beta$, $P(x)$ and $P(y)$ imply $P(x \sqcap y)$). Then for any element $x$ in the subtype $\{x \in \beta \mid P(x)\}$, the inclusion map $\text{subtypeVal}$ satisfies $\text{subtypeVal}(x) = x$.

InfTopHom.subtypeVal_coe theorem

 {P : β → Prop} (Ptop : P ⊤) (Pinf : ∀ ⦃x y : β⦄, P x → P y → P (x ⊓ y)) : ⇑(subtypeVal Ptop Pinf) = Subtype.val

Full source

@[simp]
lemma subtypeVal_coe {P : β → Prop}
    (Ptop : P ⊤) (Pinf : ∀ ⦃x y : β⦄, P x → P y → P (x ⊓ y)) :
    ⇑(subtypeVal Ptop Pinf) = Subtype.val := rfl

Inclusion Homomorphism Equals Subtype Projection for Inf-Top Preserving Predicates

Informal description

Let $\beta$ be a type with a top element $\top$ and an infimum operation $\sqcap$, and let $P$ be a predicate on $\beta$ such that: 1. $P(\top)$ holds, and 2. For any $x, y \in \beta$, if $P(x)$ and $P(y)$ hold, then $P(x \sqcap y)$ holds. Then the underlying function of the inclusion homomorphism $\text{subtypeVal}$ from the subtype $\{x \in \beta \mid P(x)\}$ to $\beta$ is equal to the canonical projection $\text{Subtype.val}$.

BoundedLatticeHom.toSupBotHom definition

(f : BoundedLatticeHom α β) : SupBotHom α β

Full source

/-- Reinterpret a `BoundedLatticeHom` as a `SupBotHom`. -/
def toSupBotHom (f : BoundedLatticeHom α β) : SupBotHom α β :=
  { f with }

Reinterpretation of bounded lattice homomorphism as supremum-and-bottom-preserving homomorphism

Informal description

Given a bounded lattice homomorphism $f$ from a lattice $\alpha$ to a lattice $\beta$, the function $f$ can be reinterpreted as a finitary supremum-preserving homomorphism that also preserves the bottom element. This means $f$ preserves both the supremum operation $\sqcup$ and the least element $\bot$.

BoundedLatticeHom.toInfTopHom definition

(f : BoundedLatticeHom α β) : InfTopHom α β

Full source

/-- Reinterpret a `BoundedLatticeHom` as an `InfTopHom`. -/
def toInfTopHom (f : BoundedLatticeHom α β) : InfTopHom α β :=
  { f with }

Reinterpretation of bounded lattice homomorphism as infimum-and-top-preserving homomorphism

Informal description

Given a bounded lattice homomorphism $f$ from a lattice $\alpha$ to a lattice $\beta$, the function $f$ can be reinterpreted as a finitary infimum-preserving homomorphism that also preserves the top element. This means $f$ preserves both the infimum operation $\sqcap$ and the greatest element $\top$.

BoundedLatticeHom.toBoundedOrderHom definition

(f : BoundedLatticeHom α β) : BoundedOrderHom α β

Full source

/-- Reinterpret a `BoundedLatticeHom` as a `BoundedOrderHom`. -/
def toBoundedOrderHom (f : BoundedLatticeHom α β) : BoundedOrderHom α β :=
  { f, (f.toLatticeHom : α →o β) with }

Reinterpretation of bounded lattice homomorphism as bounded order homomorphism

Informal description

Given a bounded lattice homomorphism $f$ from a lattice $\alpha$ to a lattice $\beta$, this function reinterprets $f$ as a bounded order homomorphism. This means $f$ is viewed as a monotone function that preserves both the greatest element $\top$ and the least element $\bot$ of the lattices.

BoundedLatticeHom.instFunLike instance

: FunLike (BoundedLatticeHom α β) α β

Full source

instance instFunLike : FunLike (BoundedLatticeHom α β) α β where
  coe f := f.toFun
  coe_injective' f g h := by obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := f; obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := g; congr

Function-Like Structure for Bounded Lattice Homomorphisms

Informal description

For any two lattices $\alpha$ and $\beta$ with bounded orders, the type of bounded lattice homomorphisms from $\alpha$ to $\beta$ has a function-like structure, meaning it can be coerced to a function from $\alpha$ to $\beta$.

BoundedLatticeHom.instBoundedLatticeHomClass instance

: BoundedLatticeHomClass (BoundedLatticeHom α β) α β

Full source

instance instBoundedLatticeHomClass : BoundedLatticeHomClass (BoundedLatticeHom α β) α β where
  map_sup f := f.map_sup'
  map_inf f := f.map_inf'
  map_top f := f.map_top'
  map_bot f := f.map_bot'

Bounded Lattice Homomorphisms Form a BoundedLatticeHomClass

Informal description

For any two lattices $\alpha$ and $\beta$ with bounded orders (having both a greatest element $\top$ and a least element $\bot$), the type of bounded lattice homomorphisms from $\alpha$ to $\beta$ forms a `BoundedLatticeHomClass`. This means that any bounded lattice homomorphism preserves the lattice operations (supremum $\sqcup$ and infimum $\sqcap$) as well as the top and bottom elements.

BoundedLatticeHom.toFun_eq_coe theorem

(f : BoundedLatticeHom α β) : f.toFun = f

Full source

@[simp] lemma toFun_eq_coe (f : BoundedLatticeHom α β) : f.toFun = f := rfl

Equality of Underlying Function and Bounded Lattice Homomorphism

Informal description

For any bounded lattice homomorphism $f$ from a lattice $\alpha$ to a lattice $\beta$, the underlying function $f.\text{toFun}$ is equal to $f$ itself.

BoundedLatticeHom.coe_toLatticeHom theorem

(f : BoundedLatticeHom α β) : ⇑f.toLatticeHom = f

Full source

@[simp] lemma coe_toLatticeHom (f : BoundedLatticeHom α β) : ⇑f.toLatticeHom = f := rfl

Underlying Function of Bounded Lattice Homomorphism as Lattice Homomorphism

Informal description

For any bounded lattice homomorphism $f$ from a lattice $\alpha$ to a lattice $\beta$, the underlying function of the lattice homomorphism obtained by restricting $f$ is equal to $f$ itself. In other words, if $f$ is viewed as a lattice homomorphism (ignoring the preservation of $\top$ and $\bot$), its function application coincides with $f$.

BoundedLatticeHom.coe_toSupBotHom theorem

(f : BoundedLatticeHom α β) : ⇑f.toSupBotHom = f

Full source

@[simp] lemma coe_toSupBotHom (f : BoundedLatticeHom α β) : ⇑f.toSupBotHom = f := rfl

Equality of Bounded Lattice Homomorphism and its Supremum-Bottom-Preserving Restriction

Informal description

For any bounded lattice homomorphism $f$ from a lattice $\alpha$ to a lattice $\beta$, the underlying function of the supremum-and-bottom-preserving homomorphism obtained from $f$ is equal to $f$ itself. In other words, if $f$ is viewed as a supremum-and-bottom-preserving homomorphism, its function application coincides with $f$.

BoundedLatticeHom.coe_toInfTopHom theorem

(f : BoundedLatticeHom α β) : ⇑f.toInfTopHom = f

Full source

@[simp] lemma coe_toInfTopHom (f : BoundedLatticeHom α β) : ⇑f.toInfTopHom = f := rfl

Underlying Function of Infimum-Top Homomorphism from Bounded Lattice Homomorphism Equals Original Function

Informal description

For any bounded lattice homomorphism $f$ from a lattice $\alpha$ to a lattice $\beta$, the underlying function of the infimum-and-top-preserving homomorphism obtained from $f$ is equal to $f$ itself.

BoundedLatticeHom.coe_toBoundedOrderHom theorem

(f : BoundedLatticeHom α β) : ⇑f.toBoundedOrderHom = f

Full source

@[simp] lemma coe_toBoundedOrderHom (f : BoundedLatticeHom α β) : ⇑f.toBoundedOrderHom = f := rfl

Equality of Bounded Lattice Homomorphism and its Bounded Order Homomorphism Restriction

Informal description

For any bounded lattice homomorphism $f$ from a bounded lattice $\alpha$ to a bounded lattice $\beta$, the underlying function of the bounded order homomorphism obtained from $f$ is equal to $f$ itself.

BoundedLatticeHom.coe_mk theorem

(f : LatticeHom α β) (hf hf') : ⇑(mk f hf hf') = f

Full source

@[simp] lemma coe_mk (f : LatticeHom α β) (hf hf') : ⇑(mk f hf hf') = f := rfl

Underlying Function of Constructed Bounded Lattice Homomorphism Equals Original Function

Informal description

Let $f : \alpha \to \beta$ be a lattice homomorphism between bounded lattices $\alpha$ and $\beta$, and let $hf$ and $hf'$ be proofs that $f$ preserves the top and bottom elements respectively. Then the underlying function of the bounded lattice homomorphism constructed from $f$ with these preservation properties is equal to $f$ itself.

BoundedLatticeHom.ext theorem

{f g : BoundedLatticeHom α β} (h : ∀ a, f a = g a) : f = g

Full source

@[ext]
theorem ext {f g : BoundedLatticeHom α β} (h : ∀ a, f a = g a) : f = g :=
  DFunLike.ext f g h

Extensionality of Bounded Lattice Homomorphisms

Informal description

Let $f$ and $g$ be bounded lattice homomorphisms between two bounded lattices $\alpha$ and $\beta$. If $f(a) = g(a)$ for all $a \in \alpha$, then $f = g$.

BoundedLatticeHom.copy definition

(f : BoundedLatticeHom α β) (f' : α → β) (h : f' = f) : BoundedLatticeHom α β

Full source

/-- Copy of a `BoundedLatticeHom` with a new `toFun` equal to the old one. Useful to fix
definitional equalities. -/
protected def copy (f : BoundedLatticeHom α β) (f' : α → β) (h : f' = f) : BoundedLatticeHom α β :=
  { f.toLatticeHom.copy f' h, f.toBoundedOrderHom.copy f' h with }

Copy of a bounded lattice homomorphism with a new function definition

Informal description

Given a bounded lattice homomorphism $ f \colon \alpha \to \beta $ and a function $ f' \colon \alpha \to \beta $ that is definitionally equal to $ f $, this constructs a new bounded lattice homomorphism with $ f' $ as its underlying function, preserving both the lattice operations (supremum and infimum) and the top and bottom elements.

BoundedLatticeHom.coe_copy theorem

(f : BoundedLatticeHom α β) (f' : α → β) (h : f' = f) : ⇑(f.copy f' h) = f'

Full source

@[simp]
theorem coe_copy (f : BoundedLatticeHom α β) (f' : α → β) (h : f' = f) : ⇑(f.copy f' h) = f' :=
  rfl

Underlying function of copied bounded lattice homomorphism equals copied function

Informal description

Let $f \colon \alpha \to \beta$ be a bounded lattice homomorphism between bounded lattices $\alpha$ and $\beta$, and let $f' \colon \alpha \to \beta$ be a function such that $f' = f$. Then the underlying function of the copied homomorphism $f.copy\ f'\ h$ is equal to $f'$.

BoundedLatticeHom.copy_eq theorem

(f : BoundedLatticeHom α β) (f' : α → β) (h : f' = f) : f.copy f' h = f

Full source

theorem copy_eq (f : BoundedLatticeHom α β) (f' : α → β) (h : f' = f) : f.copy f' h = f :=
  DFunLike.ext' h

Equality of Copied Bounded Lattice Homomorphism

Informal description

Let $\alpha$ and $\beta$ be lattices with bounded orders, and let $f \colon \alpha \to \beta$ be a bounded lattice homomorphism. For any function $f' \colon \alpha \to \beta$ such that $f' = f$, the copy of $f$ defined via $f'$ is equal to $f$ itself. In other words, if $f'$ coincides with $f$, then the constructed homomorphism $f.copy\ f'\ h$ is identical to $f$.

BoundedLatticeHom.id definition

: BoundedLatticeHom α α

Full source

/-- `id` as a `BoundedLatticeHom`. -/
protected def id : BoundedLatticeHom α α :=
  { LatticeHom.id α, BoundedOrderHom.id α with }

Identity bounded lattice homomorphism

Informal description

The identity function viewed as a bounded lattice homomorphism from a lattice $\alpha$ to itself, preserving both the supremum ($\sqcup$) and infimum ($\sqcap$) operations, as well as the greatest element ($\top$) and least element ($\bot$).

BoundedLatticeHom.instInhabited instance

: Inhabited (BoundedLatticeHom α α)

Full source

instance : Inhabited (BoundedLatticeHom α α) :=
  ⟨BoundedLatticeHom.id α⟩

Inhabited Type of Bounded Lattice Homomorphisms on a Lattice

Informal description

For any lattice $\alpha$ with a bounded order structure, the type of bounded lattice homomorphisms from $\alpha$ to itself is inhabited (i.e., contains at least one element).

BoundedLatticeHom.coe_id theorem

: ⇑(BoundedLatticeHom.id α) = id

Full source

@[simp, norm_cast]
theorem coe_id : ⇑(BoundedLatticeHom.id α) = id :=
  rfl

Identity Bounded Lattice Homomorphism Equals Identity Function

Informal description

The identity bounded lattice homomorphism on a lattice $\alpha$ is equal to the identity function, i.e., $\text{id}_\alpha = \text{id}$.

BoundedLatticeHom.id_apply theorem

(a : α) : BoundedLatticeHom.id α a = a

Full source

@[simp]
theorem id_apply (a : α) : BoundedLatticeHom.id α a = a :=
  rfl

Identity Bounded Lattice Homomorphism Acts as Identity Function

Informal description

For any element $a$ in a bounded lattice $\alpha$, the identity bounded lattice homomorphism evaluated at $a$ equals $a$, i.e., $\text{id}(a) = a$.

BoundedLatticeHom.comp definition

(f : BoundedLatticeHom β γ) (g : BoundedLatticeHom α β) : BoundedLatticeHom α γ

Full source

/-- Composition of `BoundedLatticeHom`s as a `BoundedLatticeHom`. -/
def comp (f : BoundedLatticeHom β γ) (g : BoundedLatticeHom α β) : BoundedLatticeHom α γ :=
  { f.toLatticeHom.comp g.toLatticeHom, f.toBoundedOrderHom.comp g.toBoundedOrderHom with }

Composition of bounded lattice homomorphisms

Informal description

The composition of two bounded lattice homomorphisms $ f \colon \beta \to \gamma $ and $ g \colon \alpha \to \beta $ is a bounded lattice homomorphism $ f \circ g \colon \alpha \to \gamma $. This composition preserves the lattice operations $\sqcup$ (supremum) and $\sqcap$ (infimum), as well as the top element $\top$ and the bottom element $\bot$.

BoundedLatticeHom.coe_comp theorem

(f : BoundedLatticeHom β γ) (g : BoundedLatticeHom α β) : (f.comp g : α → γ) = f ∘ g

Full source

@[simp]
theorem coe_comp (f : BoundedLatticeHom β γ) (g : BoundedLatticeHom α β) :
    (f.comp g : α → γ) = f ∘ g :=
  rfl

Composition of Bounded Lattice Homomorphisms as Function Composition

Informal description

For any bounded lattice homomorphisms $f \colon \beta \to \gamma$ and $g \colon \alpha \to \beta$, the underlying function of their composition $f \circ g$ is equal to the pointwise composition of the underlying functions of $f$ and $g$, i.e., $(f \circ g)(a) = f(g(a))$ for all $a \in \alpha$.

BoundedLatticeHom.comp_apply theorem

(f : BoundedLatticeHom β γ) (g : BoundedLatticeHom α β) (a : α) : (f.comp g) a = f (g a)

Full source

@[simp]
theorem comp_apply (f : BoundedLatticeHom β γ) (g : BoundedLatticeHom α β) (a : α) :
    (f.comp g) a = f (g a) :=
  rfl

Application of Composition of Bounded Lattice Homomorphisms

Informal description

Let $f \colon \beta \to \gamma$ and $g \colon \alpha \to \beta$ be bounded lattice homomorphisms between lattices with top and bottom elements. For any element $a \in \alpha$, the composition $(f \circ g)(a)$ equals $f(g(a))$.

BoundedLatticeHom.coe_comp_lattice_hom' theorem

 (f : BoundedLatticeHom β γ) (g : BoundedLatticeHom α β) :
  (⟨(f : SupHom β γ).comp g, map_inf (f.comp g)⟩ : LatticeHom α γ) = (f : LatticeHom β γ).comp g

Full source

@[simp]
-- `simp`-normal form of `coe_comp_lattice_hom`
theorem coe_comp_lattice_hom' (f : BoundedLatticeHom β γ) (g : BoundedLatticeHom α β) :
    (⟨(f : SupHom β γ).comp g, map_inf (f.comp g)⟩ : LatticeHom α γ) =
      (f : LatticeHom β γ).comp g :=
  rfl

Composition of Bounded Lattice Homomorphisms as Lattice Homomorphisms

Informal description

Let $f \colon \beta \to \gamma$ and $g \colon \alpha \to \beta$ be bounded lattice homomorphisms between lattices with top and bottom elements. Then the lattice homomorphism structure induced by the composition $f \circ g$ (which preserves both suprema and infima) is equal to the composition of $f$ and $g$ viewed as lattice homomorphisms.

BoundedLatticeHom.coe_comp_lattice_hom theorem

 (f : BoundedLatticeHom β γ) (g : BoundedLatticeHom α β) : (f.comp g : LatticeHom α γ) = (f : LatticeHom β γ).comp g

Full source

theorem coe_comp_lattice_hom (f : BoundedLatticeHom β γ) (g : BoundedLatticeHom α β) :
    (f.comp g : LatticeHom α γ) = (f : LatticeHom β γ).comp g :=
  rfl

Composition of Bounded Lattice Homomorphisms as Lattice Homomorphisms

Informal description

Let $f \colon \beta \to \gamma$ and $g \colon \alpha \to \beta$ be bounded lattice homomorphisms between lattices with top and bottom elements. Then the composition $f \circ g$, viewed as a lattice homomorphism from $\alpha$ to $\gamma$, equals the composition of $f$ and $g$ as lattice homomorphisms.

BoundedLatticeHom.coe_comp_sup_hom' theorem

 (f : BoundedLatticeHom β γ) (g : BoundedLatticeHom α β) : ⟨f ∘ g, map_sup (f.comp g)⟩ = (f : SupHom β γ).comp g

Full source

@[simp]
-- `simp`-normal form of `coe_comp_sup_hom`
theorem coe_comp_sup_hom' (f : BoundedLatticeHom β γ) (g : BoundedLatticeHom α β) :
    ⟨f ∘ g, map_sup (f.comp g)⟩ = (f : SupHom β γ).comp g :=
  rfl

Composition of Bounded Lattice Homomorphisms as Supremum-Preserving Homomorphisms

Informal description

Let $f \colon \beta \to \gamma$ and $g \colon \alpha \to \beta$ be bounded lattice homomorphisms between lattices with bounded orders. Then the supremum-preserving homomorphism obtained by composing $f$ and $g$ (as bounded lattice homomorphisms) is equal to the composition of $f$ and $g$ viewed as supremum-preserving homomorphisms. That is, $\langle f \circ g, \text{map\_sup}(f \circ g)\rangle = (f \colon \text{SupHom} \beta \gamma) \circ g$.

BoundedLatticeHom.coe_comp_sup_hom theorem

(f : BoundedLatticeHom β γ) (g : BoundedLatticeHom α β) : (f.comp g : SupHom α γ) = (f : SupHom β γ).comp g

Full source

theorem coe_comp_sup_hom (f : BoundedLatticeHom β γ) (g : BoundedLatticeHom α β) :
    (f.comp g : SupHom α γ) = (f : SupHom β γ).comp g :=
  rfl

Composition of Bounded Lattice Homomorphisms as Supremum-Preserving Homomorphisms

Informal description

Let $f \colon \beta \to \gamma$ and $g \colon \alpha \to \beta$ be bounded lattice homomorphisms between lattices with bounded orders. Then the composition $f \circ g$, viewed as a supremum-preserving homomorphism from $\alpha$ to $\gamma$, equals the composition of $f$ and $g$ viewed as supremum-preserving homomorphisms. In other words, the following diagram commutes in the category of supremum-preserving homomorphisms: $$(f \circ g)_{\text{SupHom}} = f_{\text{SupHom}} \circ g_{\text{SupHom}}$$

BoundedLatticeHom.coe_comp_inf_hom' theorem

 (f : BoundedLatticeHom β γ) (g : BoundedLatticeHom α β) : ⟨f ∘ g, map_inf (f.comp g)⟩ = (f : InfHom β γ).comp g

Full source

@[simp]
-- `simp`-normal form of `coe_comp_inf_hom`
theorem coe_comp_inf_hom' (f : BoundedLatticeHom β γ) (g : BoundedLatticeHom α β) :
    ⟨f ∘ g, map_inf (f.comp g)⟩ = (f : InfHom β γ).comp g :=
  rfl

Compatibility of Infimum-Preserving Function with Composition of Bounded Lattice Homomorphisms

Informal description

Let $f \colon \beta \to \gamma$ and $g \colon \alpha \to \beta$ be bounded lattice homomorphisms. Then the infimum-preserving function associated to their composition $f \circ g$ is equal to the composition of the infimum-preserving functions associated to $f$ and $g$. That is, $\langle f \circ g, \text{map\_inf}(f \circ g) \rangle = f_{\text{Inf}} \circ g$, where $f_{\text{Inf}}$ denotes the infimum-preserving function associated to $f$.

BoundedLatticeHom.coe_comp_inf_hom theorem

(f : BoundedLatticeHom β γ) (g : BoundedLatticeHom α β) : (f.comp g : InfHom α γ) = (f : InfHom β γ).comp g

Full source

theorem coe_comp_inf_hom (f : BoundedLatticeHom β γ) (g : BoundedLatticeHom α β) :
    (f.comp g : InfHom α γ) = (f : InfHom β γ).comp g :=
  rfl

Compatibility of Infimum-Preserving Structure with Composition of Bounded Lattice Homomorphisms

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be lattices with bounded orders, and let $f \colon \beta \to \gamma$ and $g \colon \alpha \to \beta$ be bounded lattice homomorphisms. Then the infimum-preserving function associated with the composition $f \circ g$ is equal to the composition of the infimum-preserving functions associated with $f$ and $g$. In other words, $(f \circ g)_{\text{inf}} = f_{\text{inf}} \circ g_{\text{inf}}$, where the subscript denotes the restriction to the infimum-preserving structure.

BoundedLatticeHom.comp_assoc theorem

 (f : BoundedLatticeHom γ δ) (g : BoundedLatticeHom β γ) (h : BoundedLatticeHom α β) :
  (f.comp g).comp h = f.comp (g.comp h)

Full source

@[simp]
theorem comp_assoc (f : BoundedLatticeHom γ δ) (g : BoundedLatticeHom β γ)
    (h : BoundedLatticeHom α β) : (f.comp g).comp h = f.comp (g.comp h) :=
  rfl

Associativity of Composition for Bounded Lattice Homomorphisms

Informal description

For any bounded lattice homomorphisms $f \colon \gamma \to \delta$, $g \colon \beta \to \gamma$, and $h \colon \alpha \to \beta$, the composition of homomorphisms is associative, i.e., $(f \circ g) \circ h = f \circ (g \circ h)$.

BoundedLatticeHom.comp_id theorem

(f : BoundedLatticeHom α β) : f.comp (BoundedLatticeHom.id α) = f

Full source

@[simp] theorem comp_id (f : BoundedLatticeHom α β) : f.comp (BoundedLatticeHom.id α) = f := rfl

Right Identity Law for Bounded Lattice Homomorphism Composition

Informal description

For any bounded lattice homomorphism $f \colon \alpha \to \beta$, the composition of $f$ with the identity bounded lattice homomorphism on $\alpha$ equals $f$ itself, i.e., $f \circ \text{id}_\alpha = f$.

BoundedLatticeHom.id_comp theorem

(f : BoundedLatticeHom α β) : (BoundedLatticeHom.id β).comp f = f

Full source

@[simp] theorem id_comp (f : BoundedLatticeHom α β) : (BoundedLatticeHom.id β).comp f = f := rfl

Identity Bounded Lattice Homomorphism Composed with $f$ Equals $f$

Informal description

For any bounded lattice homomorphism $f \colon \alpha \to \beta$, the composition of the identity bounded lattice homomorphism on $\beta$ with $f$ equals $f$ itself, i.e., $\text{id}_\beta \circ f = f$.

BoundedLatticeHom.cancel_right theorem

 {g₁ g₂ : BoundedLatticeHom β γ} {f : BoundedLatticeHom α β} (hf : Surjective f) : g₁.comp f = g₂.comp f ↔ g₁ = g₂

Full source

@[simp]
theorem cancel_right {g₁ g₂ : BoundedLatticeHom β γ} {f : BoundedLatticeHom α β}
    (hf : Surjective f) : g₁.comp f = g₂.comp f ↔ g₁ = g₂ :=
  ⟨fun h => BoundedLatticeHom.ext <| hf.forall.2 <| DFunLike.ext_iff.1 h,
    fun h => congr_arg₂ _ h rfl⟩

Right Cancellation Property for Composition of Bounded Lattice Homomorphisms

Informal description

Let $f \colon \alpha \to \beta$ be a surjective bounded lattice homomorphism between bounded lattices $\alpha$ and $\beta$, and let $g_1, g_2 \colon \beta \to \gamma$ be bounded lattice homomorphisms to another bounded lattice $\gamma$. Then the compositions $g_1 \circ f$ and $g_2 \circ f$ are equal if and only if $g_1 = g_2$.

BoundedLatticeHom.cancel_left theorem

 {g : BoundedLatticeHom β γ} {f₁ f₂ : BoundedLatticeHom α β} (hg : Injective g) : g.comp f₁ = g.comp f₂ ↔ f₁ = f₂

Full source

@[simp]
theorem cancel_left {g : BoundedLatticeHom β γ} {f₁ f₂ : BoundedLatticeHom α β} (hg : Injective g) :
    g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
  ⟨fun h => ext fun a => hg <| by rw [← comp_apply, h, comp_apply], congr_arg _⟩

Left Cancellation Property for Composition of Bounded Lattice Homomorphisms

Informal description

Let $g \colon \beta \to \gamma$ be an injective bounded lattice homomorphism between bounded lattices $\beta$ and $\gamma$, and let $f_1, f_2 \colon \alpha \to \beta$ be bounded lattice homomorphisms from a bounded lattice $\alpha$ to $\beta$. Then the compositions $g \circ f_1$ and $g \circ f_2$ are equal if and only if $f_1 = f_2$.

BoundedLatticeHom.subtypeVal definition

 {P : β → Prop} (Pbot : P ⊥) (Ptop : P ⊤) (Psup : ∀ ⦃x y⦄, P x → P y → P (x ⊔ y))
  (Pinf : ∀ ⦃x y⦄, P x → P y → P (x ⊓ y)) :
  letI := Subtype.lattice Psup Pinf
  letI := Subtype.boundedOrder Pbot Ptop
  BoundedLatticeHom { x : β // P x } β

Full source

/-- `Subtype.val` as a `BoundedLatticeHom`. -/
def subtypeVal {P : β → Prop} (Pbot : P ⊥) (Ptop : P ⊤)
    (Psup : ∀ ⦃x y⦄, P x → P y → P (x ⊔ y)) (Pinf : ∀ ⦃x y⦄, P x → P y → P (x ⊓ y)) :
    letI := Subtype.lattice Psup Pinf
    letI := Subtype.boundedOrder Pbot Ptop
    BoundedLatticeHom {x : β // P x} β :=
  letI := Subtype.lattice Psup Pinf
  letI := Subtype.boundedOrder Pbot Ptop
  .mk (.subtypeVal Psup Pinf) (by simp [Subtype.coe_top Ptop]) (by simp [Subtype.coe_bot Pbot])

Canonical bounded lattice homomorphism from a subtype

Informal description

Given a predicate $ P $ on a lattice $ \beta $ such that $ P $ holds for the bottom element $ \bot $ and the top element $ \top $, and $ P $ is closed under both the supremum $ \sqcup $ and infimum $ \sqcap $ operations, the function `BoundedLatticeHom.subtypeVal` is the canonical bounded lattice homomorphism from the subtype $ \{x : \beta \mid P x\} $ to $ \beta $. Here, the subtype is equipped with the induced lattice and bounded order structure from $ \beta $.

BoundedLatticeHom.subtypeVal_apply theorem

 {P : β → Prop} (Pbot : P ⊥) (Ptop : P ⊤) (Psup : ∀ ⦃x y⦄, P x → P y → P (x ⊔ y))
  (Pinf : ∀ ⦃x y⦄, P x → P y → P (x ⊓ y)) (x : { x : β // P x }) : subtypeVal Pbot Ptop Psup Pinf x = x

Full source

@[simp]
lemma subtypeVal_apply {P : β → Prop}
    (Pbot : P ⊥) (Ptop : P ⊤) (Psup : ∀ ⦃x y⦄, P x → P y → P (x ⊔ y))
    (Pinf : ∀ ⦃x y⦄, P x → P y → P (x ⊓ y)) (x : {x : β // P x}) :
    subtypeVal Pbot Ptop Psup Pinf x = x := rfl

Canonical Bounded Lattice Homomorphism Acts as Identity on Subtype

Informal description

Let $\beta$ be a lattice with a bounded order (having a greatest element $\top$ and a least element $\bot$), and let $P$ be a predicate on $\beta$ such that: 1. $P(\bot)$ and $P(\top)$ hold, 2. $P$ is closed under the supremum operation $\sqcup$ (i.e., for any $x, y \in \beta$, if $P(x)$ and $P(y)$ hold, then $P(x \sqcup y)$ holds), 3. $P$ is closed under the infimum operation $\sqcap$ (i.e., for any $x, y \in \beta$, if $P(x)$ and $P(y)$ hold, then $P(x \sqcap y)$ holds). Then, for any element $x$ in the subtype $\{x \in \beta \mid P(x)\}$, the canonical bounded lattice homomorphism $\text{subtypeVal}$ from this subtype to $\beta$ satisfies $\text{subtypeVal}(x) = x$.

BoundedLatticeHom.subtypeVal_coe theorem

 {P : β → Prop} (Pbot : P ⊥) (Ptop : P ⊤) (Psup : ∀ ⦃x y⦄, P x → P y → P (x ⊔ y))
  (Pinf : ∀ ⦃x y⦄, P x → P y → P (x ⊓ y)) : ⇑(subtypeVal Pbot Ptop Psup Pinf) = Subtype.val

Full source

@[simp]
lemma subtypeVal_coe {P : β → Prop} (Pbot : P ⊥) (Ptop : P ⊤)
    (Psup : ∀ ⦃x y⦄, P x → P y → P (x ⊔ y)) (Pinf : ∀ ⦃x y⦄, P x → P y → P (x ⊓ y)) :
    ⇑(subtypeVal Pbot Ptop Psup Pinf) = Subtype.val := rfl

Canonical Bounded Lattice Homomorphism Equals Subtype Inclusion

Informal description

Let $\beta$ be a lattice with a greatest element $\top$ and a least element $\bot$, and let $P$ be a predicate on $\beta$ such that: 1. $P(\bot)$ holds, 2. $P(\top)$ holds, 3. For any $x, y \in \beta$, if $P(x)$ and $P(y)$ hold, then $P(x \sqcup y)$ holds, 4. For any $x, y \in \beta$, if $P(x)$ and $P(y)$ hold, then $P(x \sqcap y)$ holds. Then the canonical bounded lattice homomorphism from the subtype $\{x \in \beta \mid P(x)\}$ to $\beta$ is equal to the subtype inclusion function $\text{val}$ (which maps each element of the subtype to its underlying element in $\beta$).

SupBotHom.dual definition

: SupBotHom α β ≃ InfTopHom αᵒᵈ βᵒᵈ

Full source

/-- Reinterpret a finitary supremum homomorphism as a finitary infimum homomorphism between the dual
lattices. -/
def dual : SupBotHomSupBotHom α β ≃ InfTopHom αᵒᵈ βᵒᵈ where
  toFun f := ⟨SupHom.dual f.toSupHom, f.map_bot'⟩
  invFun f := ⟨SupHom.dual.symm f.toInfHom, f.map_top'⟩
  left_inv _ := rfl
  right_inv _ := rfl

Duality between finitary supremum and infimum homomorphisms

Informal description

The equivalence between the type of finitary supremum-preserving homomorphisms $\text{SupBotHom}(\alpha, \beta)$ and the type of finitary infimum-preserving homomorphisms $\text{InfTopHom}(\alpha^\text{op}, \beta^\text{op})$, where $\alpha^\text{op}$ and $\beta^\text{op}$ are the order-dual lattices of $\alpha$ and $\beta$ respectively. Given a finitary supremum-preserving homomorphism $f \colon \alpha \to \beta$ that also preserves the bottom element $\bot$, the corresponding finitary infimum-preserving homomorphism maps elements in $\alpha^\text{op}$ to $\beta^\text{op}$ by applying $f$ and preserves the top element $\top$. Conversely, given a finitary infimum-preserving homomorphism $g \colon \alpha^\text{op} \to \beta^\text{op}$ that also preserves the top element $\top$, the corresponding finitary supremum-preserving homomorphism maps elements in $\alpha$ to $\beta$ by applying $g$ and preserves the bottom element $\bot$.

SupBotHom.dual_id theorem

: SupBotHom.dual (SupBotHom.id α) = InfTopHom.id _

Full source

@[simp] theorem dual_id : SupBotHom.dual (SupBotHom.id α) = InfTopHom.id _ := rfl

Dual of Identity Supremum-Preserving Homomorphism is Identity Infimum-Preserving Homomorphism

Informal description

The dual of the identity finitary supremum-preserving homomorphism on a type $\alpha$ is the identity finitary infimum-preserving homomorphism on the order-dual type $\alpha^\text{op}$. That is, under the equivalence between $\text{SupBotHom}(\alpha, \alpha)$ and $\text{InfTopHom}(\alpha^\text{op}, \alpha^\text{op})$, the identity map in $\text{SupBotHom}(\alpha, \alpha)$ corresponds to the identity map in $\text{InfTopHom}(\alpha^\text{op}, \alpha^\text{op})$.

SupBotHom.dual_comp theorem

(g : SupBotHom β γ) (f : SupBotHom α β) : SupBotHom.dual (g.comp f) = (SupBotHom.dual g).comp (SupBotHom.dual f)

Full source

@[simp]
theorem dual_comp (g : SupBotHom β γ) (f : SupBotHom α β) :
    SupBotHom.dual (g.comp f) = (SupBotHom.dual g).comp (SupBotHom.dual f) :=
  rfl

Duality of Composition for Finitary Supremum-Preserving Homomorphisms

Informal description

Let $f \colon \alpha \to \beta$ and $g \colon \beta \to \gamma$ be finitary supremum-preserving homomorphisms between lattices with bottom elements. Then, the dual of their composition $g \circ f$ is equal to the composition of their duals, i.e., $$(g \circ f)^\text{op} = g^\text{op} \circ f^\text{op},$$ where $f^\text{op} \colon \alpha^\text{op} \to \beta^\text{op}$ and $g^\text{op} \colon \beta^\text{op} \to \gamma^\text{op}$ are the corresponding finitary infimum-preserving homomorphisms on the order-dual lattices.

SupBotHom.symm_dual_id theorem

: SupBotHom.dual.symm (InfTopHom.id _) = SupBotHom.id α

Full source

@[simp]
theorem symm_dual_id : SupBotHom.dual.symm (InfTopHom.id _) = SupBotHom.id α :=
  rfl

Inverse Duality of Identity InfTopHom Yields Identity SupBotHom

Informal description

The inverse of the duality equivalence applied to the identity finitary infimum-preserving homomorphism on the order dual of $\alpha$ is equal to the identity finitary supremum-preserving homomorphism on $\alpha$.

SupBotHom.symm_dual_comp theorem

 (g : InfTopHom βᵒᵈ γᵒᵈ) (f : InfTopHom αᵒᵈ βᵒᵈ) :
  SupBotHom.dual.symm (g.comp f) = (SupBotHom.dual.symm g).comp (SupBotHom.dual.symm f)

Full source

@[simp]
theorem symm_dual_comp (g : InfTopHom βᵒᵈ γᵒᵈ) (f : InfTopHom αᵒᵈ βᵒᵈ) :
    SupBotHom.dual.symm (g.comp f) =
      (SupBotHom.dual.symm g).comp (SupBotHom.dual.symm f) :=
  rfl

Compatibility of Duality Inverse with Composition of Infimum-Preserving Homomorphisms

Informal description

For any finitary infimum-preserving homomorphisms $f \colon \alpha^\text{op} \to \beta^\text{op}$ and $g \colon \beta^\text{op} \to \gamma^\text{op}$ that also preserve the top element, the inverse of the duality equivalence applied to the composition $g \circ f$ is equal to the composition of the inverses of the duality equivalence applied to $g$ and $f$ separately. In other words, the following equality holds: \[ \text{SupBotHom.dual.symm}(g \circ f) = (\text{SupBotHom.dual.symm } g) \circ (\text{SupBotHom.dual.symm } f). \]

InfTopHom.dual definition

: InfTopHom α β ≃ SupBotHom αᵒᵈ βᵒᵈ

Full source

/-- Reinterpret a finitary infimum homomorphism as a finitary supremum homomorphism between the dual
lattices. -/
@[simps]
protected def dual : InfTopHomInfTopHom α β ≃ SupBotHom αᵒᵈ βᵒᵈ where
  toFun f := ⟨InfHom.dual f.toInfHom, f.map_top'⟩
  invFun f := ⟨InfHom.dual.symm f.toSupHom, f.map_bot'⟩
  left_inv _ := rfl
  right_inv _ := rfl

Duality between finitary infimum and supremum homomorphisms

Informal description

The equivalence between finitary infimum-preserving homomorphisms from $\alpha$ to $\beta$ and finitary supremum-preserving homomorphisms from the order dual of $\alpha$ to the order dual of $\beta$. Specifically, it maps an infimum-preserving homomorphism $f$ that also preserves the top element to a supremum-preserving homomorphism between the dual lattices that also preserves the bottom element, and vice versa, with both directions being mutual inverses.

InfTopHom.dual_id theorem

: InfTopHom.dual (InfTopHom.id α) = SupBotHom.id _

Full source

@[simp]
theorem dual_id : InfTopHom.dual (InfTopHom.id α) = SupBotHom.id _ :=
  rfl

Duality of Identity Infimum Homomorphism: $\text{dual}(\text{id}_{\alpha}) = \text{id}_{\alpha^{\text{op}}}$

Informal description

The duality equivalence applied to the identity finitary infimum-preserving homomorphism on a type $\alpha$ yields the identity finitary supremum-preserving homomorphism on the order dual of $\alpha$. That is, $\text{dual}(\text{id}_{\alpha}) = \text{id}_{\alpha^{\text{op}}}$.

InfTopHom.dual_comp theorem

(g : InfTopHom β γ) (f : InfTopHom α β) : InfTopHom.dual (g.comp f) = (InfTopHom.dual g).comp (InfTopHom.dual f)

Full source

@[simp]
theorem dual_comp (g : InfTopHom β γ) (f : InfTopHom α β) :
    InfTopHom.dual (g.comp f) = (InfTopHom.dual g).comp (InfTopHom.dual f) :=
  rfl

Duality of Composition for Infimum-Preserving Homomorphisms

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be types equipped with infimum operations $\sqcap$ and top elements $\top$. For any finitary infimum-preserving homomorphisms $f \colon \alpha \to \beta$ and $g \colon \beta \to \gamma$, the dual of their composition $g \circ f$ is equal to the composition of their duals, i.e., \[ \text{dual}(g \circ f) = \text{dual}(g) \circ \text{dual}(f), \] where $\text{dual}$ maps an infimum-preserving homomorphism to the corresponding supremum-preserving homomorphism between the order duals of the types.

InfTopHom.symm_dual_id theorem

: InfTopHom.dual.symm (SupBotHom.id _) = InfTopHom.id α

Full source

@[simp]
theorem symm_dual_id : InfTopHom.dual.symm (SupBotHom.id _) = InfTopHom.id α :=
  rfl

Inverse Duality of Identity Homomorphism: $\text{InfTopHom.dual.symm}(\text{SupBotHom.id}) = \text{InfTopHom.id}$

Informal description

The inverse of the duality equivalence applied to the identity finitary supremum-preserving homomorphism on the order dual of $\alpha$ yields the identity finitary infimum-preserving homomorphism on $\alpha$. In other words, $\text{InfTopHom.dual.symm}(\text{SupBotHom.id}_{\alpha^{\text{op}}}) = \text{InfTopHom.id}_\alpha$.

InfTopHom.symm_dual_comp theorem

 (g : SupBotHom βᵒᵈ γᵒᵈ) (f : SupBotHom αᵒᵈ βᵒᵈ) :
  InfTopHom.dual.symm (g.comp f) = (InfTopHom.dual.symm g).comp (InfTopHom.dual.symm f)

Full source

@[simp]
theorem symm_dual_comp (g : SupBotHom βᵒᵈ γᵒᵈ) (f : SupBotHom αᵒᵈ βᵒᵈ) :
    InfTopHom.dual.symm (g.comp f) =
      (InfTopHom.dual.symm g).comp (InfTopHom.dual.symm f) :=
  rfl

Inverse Duality Equivalence Preserves Composition of Supremum-Preserving Homomorphisms

Informal description

For any finitary supremum-preserving homomorphisms $g \colon \beta^{\text{op}} \to \gamma^{\text{op}}$ and $f \colon \alpha^{\text{op}} \to \beta^{\text{op}}$ between order-dual lattices, the inverse of the duality equivalence applied to the composition $g \circ f$ is equal to the composition of the inverses of the duality equivalence applied to $g$ and $f$ separately. In other words, the following diagram commutes: \[ \text{InfTopHom.dual.symm}(g \circ f) = \text{InfTopHom.dual.symm}(g) \circ \text{InfTopHom.dual.symm}(f). \]

BoundedLatticeHom.dual definition

: BoundedLatticeHom α β ≃ BoundedLatticeHom αᵒᵈ βᵒᵈ

Full source

/-- Reinterpret a bounded lattice homomorphism as a bounded lattice homomorphism between the dual
bounded lattices. -/
@[simps]
protected def dual : BoundedLatticeHomBoundedLatticeHom α β ≃ BoundedLatticeHom αᵒᵈ βᵒᵈ where
  toFun f := ⟨LatticeHom.dual f.toLatticeHom, f.map_bot', f.map_top'⟩
  invFun f := ⟨LatticeHom.dual.symm f.toLatticeHom, f.map_bot', f.map_top'⟩
  left_inv _ := rfl
  right_inv _ := rfl

Duality of bounded lattice homomorphisms

Informal description

The equivalence between the type of bounded lattice homomorphisms from $\alpha$ to $\beta$ and the type of bounded lattice homomorphisms from the order dual $\alpha^\text{op}$ to the order dual $\beta^\text{op}$. Specifically, it maps a bounded lattice homomorphism $f \colon \alpha \to \beta$ to a bounded lattice homomorphism between the dual lattices by preserving both supremum and infimum operations as well as the top and bottom elements, and vice versa, with both directions being mutual inverses.

BoundedLatticeHom.dual_id theorem

: BoundedLatticeHom.dual (BoundedLatticeHom.id α) = BoundedLatticeHom.id _

Full source

@[simp]
theorem dual_id : BoundedLatticeHom.dual (BoundedLatticeHom.id α) = BoundedLatticeHom.id _ :=
  rfl

Duality Equivalence Preserves Identity Homomorphism: $\text{dual}(\text{id}_\alpha) = \text{id}_{\alpha^{\text{op}}}$

Informal description

The duality equivalence applied to the identity bounded lattice homomorphism on a lattice $\alpha$ yields the identity bounded lattice homomorphism on the order dual lattice $\alpha^{\text{op}}$. That is, $\text{dual}(\text{id}_\alpha) = \text{id}_{\alpha^{\text{op}}}$.

BoundedLatticeHom.dual_comp theorem

 (g : BoundedLatticeHom β γ) (f : BoundedLatticeHom α β) :
  BoundedLatticeHom.dual (g.comp f) = (BoundedLatticeHom.dual g).comp (BoundedLatticeHom.dual f)

Full source

@[simp]
theorem dual_comp (g : BoundedLatticeHom β γ) (f : BoundedLatticeHom α β) :
    BoundedLatticeHom.dual (g.comp f) =
      (BoundedLatticeHom.dual g).comp (BoundedLatticeHom.dual f) :=
  rfl

Duality of Composition of Bounded Lattice Homomorphisms: $\text{dual}(g \circ f) = \text{dual}(g) \circ \text{dual}(f)$

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be lattices equipped with both a greatest element $\top$ and a least element $\bot$. For any bounded lattice homomorphisms $f \colon \alpha \to \beta$ and $g \colon \beta \to \gamma$, the dual of their composition $g \circ f$ is equal to the composition of their duals. That is, \[ \text{dual}(g \circ f) = \text{dual}(g) \circ \text{dual}(f), \] where $\text{dual}$ denotes the equivalence between bounded lattice homomorphisms and their counterparts on the order dual lattices.

BoundedLatticeHom.symm_dual_id theorem

: BoundedLatticeHom.dual.symm (BoundedLatticeHom.id _) = BoundedLatticeHom.id α

Full source

@[simp]
theorem symm_dual_id :
    BoundedLatticeHom.dual.symm (BoundedLatticeHom.id _) = BoundedLatticeHom.id α :=
  rfl

Inverse Duality of Identity Bounded Lattice Homomorphism

Informal description

The inverse of the duality equivalence applied to the identity bounded lattice homomorphism on the order dual lattice $\alpha^\text{op}$ yields the identity bounded lattice homomorphism on the original lattice $\alpha$. In other words, $\text{BoundedLatticeHom.dual}^{-1}(\text{id}_{\alpha^\text{op}}) = \text{id}_\alpha$.

BoundedLatticeHom.symm_dual_comp theorem

 (g : BoundedLatticeHom βᵒᵈ γᵒᵈ) (f : BoundedLatticeHom αᵒᵈ βᵒᵈ) :
  BoundedLatticeHom.dual.symm (g.comp f) = (BoundedLatticeHom.dual.symm g).comp (BoundedLatticeHom.dual.symm f)

Full source

@[simp]
theorem symm_dual_comp (g : BoundedLatticeHom βᵒᵈ γᵒᵈ) (f : BoundedLatticeHom αᵒᵈ βᵒᵈ) :
    BoundedLatticeHom.dual.symm (g.comp f) =
      (BoundedLatticeHom.dual.symm g).comp (BoundedLatticeHom.dual.symm f) :=
  rfl

Inverse Duality Preserves Composition of Bounded Lattice Homomorphisms

Informal description

For any bounded lattice homomorphisms $g \colon \beta^\text{op} \to \gamma^\text{op}$ and $f \colon \alpha^\text{op} \to \beta^\text{op}$, the inverse of the duality equivalence applied to the composition $g \circ f$ is equal to the composition of the inverses of the duality equivalences applied to $g$ and $f$ separately. That is, \[ \text{BoundedLatticeHom.dual}^{-1}(g \circ f) = \text{BoundedLatticeHom.dual}^{-1}(g) \circ \text{BoundedLatticeHom.dual}^{-1}(f). \]

Mathlib.Order.Hom.BoundedLattice

Types of morphisms

Typeclasses

TODO