Mathlib.Order.Hom.Lattice

SupHom structure

(α β : Type*) [Max α] [Max β]

Full source

/-- The type of `⊔`-preserving functions from `α` to `β`. -/
structure SupHom (α β : Type*) [Max α] [Max β] where
  /-- The underlying function of a `SupHom`.

  Do not use this function directly. Instead use the coercion coming from the `FunLike`
  instance. -/
  toFun : α → β
  /-- A `SupHom` preserves suprema.

  Do not use this directly. Use `map_sup` instead. -/
  map_sup' (a b : α) : toFun (a ⊔ b) = toFun a ⊔ toFun b

Supremum-preserving homomorphism

Informal description

The structure representing functions between types `α` and `β` that preserve the supremum operation `⊔`, where `α` and `β` are equipped with a maximum operation (denoted by `Max` in the formal statement).

InfHom structure

(α β : Type*) [Min α] [Min β]

Full source

/-- The type of `⊓`-preserving functions from `α` to `β`. -/
structure InfHom (α β : Type*) [Min α] [Min β] where
  /-- The underlying function of an `InfHom`.

  Do not use this function directly. Instead use the coercion coming from the `FunLike`
  instance. -/
  toFun : α → β
  /-- An `InfHom` preserves infima.

  Do not use this directly. Use `map_inf` instead. -/
  map_inf' (a b : α) : toFun (a ⊓ b) = toFun a ⊓ toFun b

Infimum-preserving function

Informal description

The structure representing functions between types `α` and `β` that preserve the infimum operation `⊓`. Here, `α` and `β` are equipped with a minimum operation (denoted by `Min`), and the function maps the infimum of any two elements in `α` to the infimum of their images in `β`.

LatticeHom structure

(α β : Type*) [Lattice α] [Lattice β] extends SupHom α β

Full source

/-- The type of lattice homomorphisms from `α` to `β`. -/
structure LatticeHom (α β : Type*) [Lattice α] [Lattice β] extends SupHom α β where
  /-- A `LatticeHom` preserves infima.

  Do not use this directly. Use `map_inf` instead. -/
  map_inf' (a b : α) : toFun (a ⊓ b) = toFun a ⊓ toFun b

Lattice Homomorphism

Informal description

The structure representing lattice homomorphisms between lattices $\alpha$ and $\beta$, i.e., maps that preserve both the supremum ($\sqcup$) and infimum ($\sqcap$) operations.

SupHomClass structure

(F α β : Type*) [Max α] [Max β] [FunLike F α β]

Full source

/-- `SupHomClass F α β` states that `F` is a type of `⊔`-preserving morphisms.

You should extend this class when you extend `SupHom`. -/
class SupHomClass (F α β : Type*) [Max α] [Max β] [FunLike F α β] : Prop where
  /-- A `SupHomClass` morphism preserves suprema. -/
  map_sup (f : F) (a b : α) : f (a ⊔ b) = f a ⊔ f b

Supremum-preserving morphism class

Informal description

The class `SupHomClass F α β` states that terms of type `F` are supremum-preserving morphisms between types `α` and `β`, where both `α` and `β` are equipped with a supremum operation (`⊔`). This means that for any `f : F` and any elements `x, y ∈ α`, the morphism satisfies: \[ f(x ⊔ y) = f(x) ⊔ f(y). \]

InfHomClass structure

(F α β : Type*) [Min α] [Min β] [FunLike F α β]

Full source

/-- `InfHomClass F α β` states that `F` is a type of `⊓`-preserving morphisms.

You should extend this class when you extend `InfHom`. -/
class InfHomClass (F α β : Type*) [Min α] [Min β] [FunLike F α β] : Prop where
  /-- An `InfHomClass` morphism preserves infima. -/
  map_inf (f : F) (a b : α) : f (a ⊓ b) = f a ⊓ f b

Infimum-preserving morphism class

Informal description

The class `InfHomClass F α β` states that terms of type `F` are infimum-preserving morphisms between types `α` and `β`, where both `α` and `β` are equipped with an infimum operation (`⊓`). This means that for any `f : F` and any elements `x, y : α`, the morphism satisfies `f (x ⊓ y) = f x ⊓ f y`.

LatticeHomClass structure

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

Full source

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

You should extend this class when you extend `LatticeHom`. -/
class LatticeHomClass (F α β : Type*) [Lattice α] [Lattice β] [FunLike F α β] : Prop
  extends SupHomClass F α β where
  /-- A `LatticeHomClass` morphism preserves infima. -/
  map_inf (f : F) (a b : α) : f (a ⊓ b) = f a ⊓ f b

Lattice Homomorphism Class

Informal description

The class `LatticeHomClass F α β` states that terms of type `F` are lattice homomorphisms between lattices `α` and `β`, i.e., maps that preserve both the supremum (`⊔`) and infimum (`⊓`) operations. This means that for any `f : F` and any elements `x, y ∈ α`, the homomorphism satisfies: \[ f(x ⊔ y) = f(x) ⊔ f(y) \quad \text{and} \quad f(x ⊓ y) = f(x) ⊓ f(y). \]

SupHomClass.toOrderHomClass instance

[SemilatticeSup α] [SemilatticeSup β] [SupHomClass F α β] : OrderHomClass F α β

Full source

instance (priority := 100) SupHomClass.toOrderHomClass [SemilatticeSup α] [SemilatticeSup β]
    [SupHomClass F α β] : OrderHomClass F α β :=
  { ‹SupHomClass F α β› with
    map_rel := fun f a b h => by rw [← sup_eq_right, ← map_sup, sup_eq_right.2 h] }

Supremum-Preserving Morphisms are Monotone

Informal description

For any semilattices $\alpha$ and $\beta$ with suprema, every supremum-preserving morphism between them is also an order-preserving morphism. That is, if $F$ is a type of supremum-preserving morphisms from $\alpha$ to $\beta$, then any $f \in F$ is monotone: $x \leq y$ implies $f(x) \leq f(y)$ for all $x, y \in \alpha$.

InfHomClass.toOrderHomClass instance

[SemilatticeInf α] [SemilatticeInf β] [InfHomClass F α β] : OrderHomClass F α β

Full source

instance (priority := 100) InfHomClass.toOrderHomClass [SemilatticeInf α] [SemilatticeInf β]
    [InfHomClass F α β] : OrderHomClass F α β :=
  { ‹InfHomClass F α β› with
    map_rel := fun f a b h => by rw [← inf_eq_left, ← map_inf, inf_eq_left.2 h] }

Infimum-Preserving Morphisms are Monotone

Informal description

For any semilattices $\alpha$ and $\beta$ with infima, every infimum-preserving morphism between them is also an order-preserving morphism. That is, if $F$ is a type of infimum-preserving morphisms from $\alpha$ to $\beta$, then any $f \in F$ is monotone: $x \leq y$ implies $f(x) \leq f(y)$ for all $x, y \in \alpha$.

LatticeHomClass.toInfHomClass instance

[Lattice α] [Lattice β] [LatticeHomClass F α β] : InfHomClass F α β

Full source

instance (priority := 100) LatticeHomClass.toInfHomClass [Lattice α] [Lattice β]
    [LatticeHomClass F α β] : InfHomClass F α β :=
  { ‹LatticeHomClass F α β› with }

Lattice Homomorphisms Preserve Infima

Informal description

For any lattices $\alpha$ and $\beta$, every lattice homomorphism between them preserves infima. That is, if $F$ is a type of lattice homomorphisms 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$.

OrderIsoClass.toSupHomClass instance

[SemilatticeSup α] [SemilatticeSup β] [OrderIsoClass F α β] : SupHomClass F α β

Full source

instance (priority := 100) OrderIsoClass.toSupHomClass [SemilatticeSup α] [SemilatticeSup β]
    [OrderIsoClass F α β] : SupHomClass F α β :=
  { show OrderHomClass F α β from inferInstance with
    map_sup := fun f a b =>
      eq_of_forall_ge_iff fun c => by simp only [← le_map_inv_iff, sup_le_iff] }

Order Isomorphisms Preserve Suprema

Informal description

For any semilattices $\alpha$ and $\beta$ with suprema, every order isomorphism between them preserves suprema. 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$.

OrderIsoClass.toInfHomClass instance

[SemilatticeInf α] [SemilatticeInf β] [OrderIsoClass F α β] : InfHomClass F α β

Full source

instance (priority := 100) OrderIsoClass.toInfHomClass [SemilatticeInf α] [SemilatticeInf β]
    [OrderIsoClass F α β] : InfHomClass F α β :=
  { show OrderHomClass F α β from inferInstance with
    map_inf := fun f a b =>
      eq_of_forall_le_iff fun c => by simp only [← map_inv_le_iff, le_inf_iff] }

Order Isomorphisms Preserve Infima

Informal description

For any semilattice infima $\alpha$ and $\beta$, every order isomorphism between them preserves infima. 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$.

OrderIsoClass.toLatticeHomClass instance

[Lattice α] [Lattice β] [OrderIsoClass F α β] : LatticeHomClass F α β

Full source

instance (priority := 100) OrderIsoClass.toLatticeHomClass [Lattice α] [Lattice β]
    [OrderIsoClass F α β] : LatticeHomClass F α β :=
  { OrderIsoClass.toSupHomClass, OrderIsoClass.toInfHomClass with }

Order Isomorphisms are Lattice Homomorphisms

Informal description

For any lattices $\alpha$ and $\beta$, every order isomorphism between them preserves both suprema and infima. 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) \quad \text{and} \quad f(x \sqcap y) = f(x) \sqcap f(y) \] for all $x, y \in \alpha$.

orderEmbeddingOfInjective definition

[SemilatticeInf α] [SemilatticeInf β] (f : F) [InfHomClass F α β] (hf : Injective f) : α ↪o β

Full source

/-- We can regard an injective map preserving binary infima as an order embedding. -/
@[simps! apply]
def orderEmbeddingOfInjective [SemilatticeInf α] [SemilatticeInf β] (f : F) [InfHomClass F α β]
    (hf : Injective f) : α ↪o β :=
  OrderEmbedding.ofMapLEIff f (fun x y ↦ by
    refine ⟨fun h ↦ ?_, fun h ↦ OrderHomClass.mono f h⟩
    rwa [← inf_eq_left, ← hf.eq_iff, map_inf, inf_eq_left])

Order embedding induced by an injective infimum-preserving map

Informal description

Given a semilattice infimum structure on types $\alpha$ and $\beta$, an injective map $f : \alpha \to \beta$ that preserves binary infima (i.e., $f(x \sqcap y) = f(x) \sqcap f(y)$ for all $x, y \in \alpha$) can be regarded as an order embedding. This means $f$ induces an order isomorphism between $\alpha$ and its image in $\beta$.

instCoeTCSupHomOfSupHomClass instance

[Max α] [Max β] [SupHomClass F α β] : CoeTC F (SupHom α β)

Full source

instance [Max α] [Max β] [SupHomClass F α β] : CoeTC F (SupHom α β) :=
  ⟨fun f => ⟨f, map_sup f⟩⟩

Coercion from Supremum-Preserving Morphism Class to Supremum-Preserving Homomorphisms

Informal description

For any types $\alpha$ and $\beta$ equipped with a maximum operation, and any type $F$ that is a supremum-preserving morphism class from $\alpha$ to $\beta$, there is a canonical way to regard elements of $F$ as supremum-preserving homomorphisms from $\alpha$ to $\beta$.

instCoeTCInfHomOfInfHomClass instance

[Min α] [Min β] [InfHomClass F α β] : CoeTC F (InfHom α β)

Full source

instance [Min α] [Min β] [InfHomClass F α β] : CoeTC F (InfHom α β) :=
  ⟨fun f => ⟨f, map_inf f⟩⟩

Coercion from Infimum-Preserving Morphism Class to Infimum-Preserving Homomorphisms

Informal description

For any types $\alpha$ and $\beta$ equipped with a minimum operation, and any type $F$ that is an infimum-preserving morphism class from $\alpha$ to $\beta$, there is a canonical coercion from $F$ to the type of infimum-preserving homomorphisms from $\alpha$ to $\beta$.

instCoeTCLatticeHomOfLatticeHomClass instance

[Lattice α] [Lattice β] [LatticeHomClass F α β] : CoeTC F (LatticeHom α β)

Full source

instance [Lattice α] [Lattice β] [LatticeHomClass F α β] : CoeTC F (LatticeHom α β) :=
  ⟨fun f =>
    { toFun := f
      map_sup' := map_sup f
      map_inf' := map_inf f }⟩

Coercion from Lattice Homomorphism Class to Lattice Homomorphisms

Informal description

For any two lattices $\alpha$ and $\beta$, and any type $F$ that is a lattice homomorphism class from $\alpha$ to $\beta$, there is a canonical coercion from $F$ to the type of lattice homomorphisms from $\alpha$ to $\beta$.

SupHom.instFunLike instance

: FunLike (SupHom α β) α β

Full source

instance : FunLike (SupHom α β) α β where
  coe := SupHom.toFun
  coe_injective' f g h := by cases f; cases g; congr

Function-Like Structure of Supremum-Preserving Homomorphisms

Informal description

For any two types $\alpha$ and $\beta$ equipped with a supremum operation $\sqcup$, the type of supremum-preserving homomorphisms $\text{SupHom}(\alpha, \beta)$ is a function-like type, meaning its elements can be coerced to functions from $\alpha$ to $\beta$ in a way that preserves the supremum operation.

SupHom.instSupHomClass instance

: SupHomClass (SupHom α β) α β

Full source

instance : SupHomClass (SupHom α β) α β where
  map_sup := SupHom.map_sup'

Supremum-Preserving Homomorphisms Form a SupHomClass

Informal description

For any two types $\alpha$ and $\beta$ equipped with a supremum operation $\sqcup$, the type of supremum-preserving homomorphisms $\text{SupHom}(\alpha, \beta)$ forms a class of supremum-preserving morphisms. This means that every element $f \in \text{SupHom}(\alpha, \beta)$ satisfies the property: \[ f(x \sqcup y) = f(x) \sqcup f(y) \] for all $x, y \in \alpha$.

SupHom.toFun_eq_coe theorem

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

Full source

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

Underlying Function of Supremum-Preserving Homomorphism Equals Itself

Informal description

For any supremum-preserving homomorphism $f \colon \alpha \to \beta$, the underlying function $f.\text{toFun}$ is equal to $f$ itself when viewed as a function.

SupHom.coe_mk theorem

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

Full source

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

Coercion of Constructed Supremum-Preserving Homomorphism Equals Original Function

Informal description

For any function $f \colon \alpha \to \beta$ and proof $hf$ that $f$ preserves suprema, the coercion of the supremum-preserving homomorphism constructed from $f$ and $hf$ is equal to $f$ itself. In other words, if $\varphi$ is the supremum-preserving homomorphism defined by $\varphi(x) = f(x)$, then $\varphi = f$ as functions.

SupHom.ext theorem

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

Full source

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

Extensionality of Supremum-Preserving Homomorphisms

Informal description

For any two supremum-preserving homomorphisms $f, g \colon \alpha \to \beta$, if $f(a) = g(a)$ for all $a \in \alpha$, then $f = g$.

SupHom.copy definition

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

Full source

/-- Copy of a `SupHom` with a new `toFun` equal to the old one. Useful to fix definitional
equalities. -/
protected def copy (f : SupHom α β) (f' : α → β) (h : f' = f) : SupHom α β where
  toFun := f'
  map_sup' := h.symm ▸ f.map_sup'

Copy of a supremum-preserving homomorphism with a new function definition

Informal description

Given a supremum-preserving homomorphism $f \colon \alpha \to \beta$ 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 the property of being supremum-preserving from $f$.

SupHom.coe_copy theorem

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

Full source

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

Underlying Function of Copied Supremum-Preserving Homomorphism Equals Given Function

Informal description

For any supremum-preserving homomorphism $f \colon \alpha \to \beta$ and any 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'$.

SupHom.copy_eq theorem

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

Full source

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

Copy of Supremum-Preserving Homomorphism Equals Original

Informal description

For any supremum-preserving homomorphism $f \colon \alpha \to \beta$ and any function $f' \colon \alpha \to \beta$ such that $f' = f$, the copy of $f$ with underlying function $f'$ is equal to $f$ itself.

SupHom.id definition

: SupHom α α

Full source

/-- `id` as a `SupHom`. -/
protected def id : SupHom α α :=
  ⟨id, fun _ _ => rfl⟩

Identity supremum-preserving homomorphism

Informal description

The identity function on a type $\alpha$ equipped with a supremum operation, viewed as a supremum-preserving homomorphism. It preserves the supremum operation $\sqcup$ in the sense that for any $x, y \in \alpha$, we have $\text{id}(x \sqcup y) = \text{id}(x) \sqcup \text{id}(y)$.

SupHom.instInhabited instance

: Inhabited (SupHom α α)

Full source

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

Inhabited Type of Supremum-Preserving Homomorphisms

Informal description

For any type $\alpha$ equipped with a supremum operation, the type of supremum-preserving homomorphisms from $\alpha$ to itself is inhabited, with the identity function as a canonical element.

SupHom.coe_id theorem

: ⇑(SupHom.id α) = id

Full source

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

Identity Supremum-Preserving Homomorphism Coincides with Identity Function

Informal description

The coercion of the identity supremum-preserving homomorphism on a type $\alpha$ equipped with a supremum operation is equal to the identity function on $\alpha$, i.e., $\text{SupHom.id}_\alpha = \text{id}_\alpha$.

SupHom.id_apply theorem

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

Full source

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

Identity Supremum-Preserving Homomorphism Acts as Identity Function

Informal description

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

SupHom.comp definition

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

Full source

/-- Composition of `SupHom`s as a `SupHom`. -/
def comp (f : SupHom β γ) (g : SupHom α β) : SupHom α γ where
  toFun := f ∘ g
  map_sup' a b := by rw [comp_apply, map_sup, map_sup]; rfl

Composition of supremum-preserving homomorphisms

Informal description

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

SupHom.coe_comp theorem

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

Full source

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

Composition of Supremum-Preserving Homomorphisms as Function Composition

Informal description

For any two 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 pointwise composition of $f$ and $g$, i.e., $(f \circ g)(a) = f(g(a))$ for all $a \in \alpha$.

SupHom.comp_apply theorem

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

Full source

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

Application of Composition of Supremum-Preserving Homomorphisms

Informal description

For any supremum-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))$.

SupHom.comp_assoc theorem

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

Full source

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

Associativity of Composition for Supremum-Preserving Homomorphisms

Informal description

For any supremum-preserving 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)$.

SupHom.comp_id theorem

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

Full source

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

Right Identity Law for Composition of Supremum-Preserving Homomorphisms

Informal description

For any supremum-preserving homomorphism $f \colon \alpha \to \beta$, the composition of $f$ with the identity supremum-preserving homomorphism on $\alpha$ equals $f$ itself.

SupHom.id_comp theorem

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

Full source

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

Left Identity Law for Composition of Supremum-Preserving Homomorphisms

Informal description

For any supremum-preserving homomorphism $f \colon \alpha \to \beta$, the composition of the identity supremum-preserving homomorphism on $\beta$ with $f$ equals $f$ itself.

SupHom.cancel_right theorem

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

Full source

@[simp]
theorem cancel_right {g₁ g₂ : SupHom β γ} {f : SupHom α β} (hf : Surjective f) :
    g₁.comp f = g₂.comp f ↔ g₁ = g₂ :=
  ⟨fun h => SupHom.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 supremum-preserving homomorphism, and let $g_1, g_2 \colon \beta \to \gamma$ be two supremum-preserving homomorphisms. Then the compositions $g_1 \circ f$ and $g_2 \circ f$ are equal if and only if $g_1 = g_2$.

SupHom.cancel_left theorem

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

Full source

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

Left Cancellation Property for Composition of Supremum-Preserving Homomorphisms

Informal description

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

SupHom.const definition

(b : β) : SupHom α β

Full source

/-- The constant function as a `SupHom`. -/
def const (b : β) : SupHom α β := ⟨fun _ ↦ b, fun _ _ ↦ (sup_idem _).symm⟩

Constant supremum-preserving homomorphism

Informal description

The constant function that maps every element of a type $\alpha$ to a fixed element $b$ of a type $\beta$, viewed as a supremum-preserving homomorphism. This means the function preserves the supremum operation, i.e., the supremum of any two elements in $\alpha$ is mapped to the supremum of their images in $\beta$, which is just $b$ itself since the function is constant.

SupHom.coe_const theorem

(b : β) : ⇑(const α b) = Function.const α b

Full source

@[simp]
theorem coe_const (b : β) : ⇑(const α b) = Function.const α b :=
  rfl

Coefficient of Constant Supremum-Preserving Homomorphism Equals Constant Function

Informal description

For any fixed element $b$ in a type $\beta$, the supremum-preserving homomorphism $\text{const}_\alpha(b)$ from a type $\alpha$ to $\beta$ is equal to the constant function that maps every element of $\alpha$ to $b$.

SupHom.const_apply theorem

(b : β) (a : α) : const α b a = b

Full source

@[simp]
theorem const_apply (b : β) (a : α) : const α b a = b :=
  rfl

Evaluation of Constant Supremum-Preserving Homomorphism

Informal description

For any fixed element $b$ in a type $\beta$ and any element $a$ in a type $\alpha$, the constant supremum-preserving homomorphism $\text{const}_\alpha(b)$ evaluated at $a$ equals $b$.

SupHom.instMax instance

: Max (SupHom α β)

Full source

instance : Max (SupHom α β) :=
  ⟨fun f g =>
    ⟨f ⊔ g, fun a b => by
      rw [Pi.sup_apply, map_sup, map_sup]
      exact sup_sup_sup_comm _ _ _ _⟩⟩

Maximum Operation on Supremum-Preserving Homomorphisms

Informal description

For any two types $\alpha$ and $\beta$ equipped with a maximum operation, the type of supremum-preserving homomorphisms $\text{SupHom}(\alpha, \beta)$ is itself equipped with a maximum operation.

SupHom.instSemilatticeSup instance

: SemilatticeSup (SupHom α β)

Full source

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

Semilattice Structure on Supremum-Preserving Homomorphisms

Informal description

For any two types $\alpha$ and $\beta$ equipped with a supremum operation $\sqcup$, the type of supremum-preserving homomorphisms $\text{SupHom}(\alpha, \beta)$ forms a semilattice with respect to the supremum operation. This means that $\text{SupHom}(\alpha, \beta)$ is equipped with a partial order where every pair of elements has a least upper bound, and the supremum operation is associative, commutative, and idempotent.

SupHom.instBot instance

[Bot β] : Bot (SupHom α β)

Full source

instance [Bot β] : Bot (SupHom α β) :=
  ⟨SupHom.const α ⊥⟩

Bottom Element in Supremum-Preserving Homomorphisms

Informal description

For any type $\beta$ with a bottom element $\bot$, the type of supremum-preserving homomorphisms $\text{SupHom}(\alpha, \beta)$ also has a bottom element, given by the constant function that maps every element of $\alpha$ to $\bot$.

SupHom.instTop instance

[Top β] : Top (SupHom α β)

Full source

instance [Top β] : Top (SupHom α β) :=
  ⟨SupHom.const α ⊤⟩

Top Element in Supremum-Preserving Homomorphisms

Informal description

For any type $\beta$ with a top element $\top$, the type of supremum-preserving homomorphisms $\text{SupHom}(\alpha, \beta)$ also has a top element, given by the constant function that maps every element of $\alpha$ to $\top$.

SupHom.instOrderBot instance

[OrderBot β] : OrderBot (SupHom α β)

Full source

instance [OrderBot β] : OrderBot (SupHom α β) :=
  OrderBot.lift ((↑) : _ → α → β) (fun _ _ => id) rfl

Order with Bottom Element in Supremum-Preserving Homomorphisms

Informal description

For any type $\beta$ with an order and a bottom element $\bot$, the type of supremum-preserving homomorphisms $\text{SupHom}(\alpha, \beta)$ inherits an order with a bottom element, where the bottom element is the constant function that maps every element of $\alpha$ to $\bot$.

SupHom.instOrderTop instance

[OrderTop β] : OrderTop (SupHom α β)

Full source

instance [OrderTop β] : OrderTop (SupHom α β) :=
  OrderTop.lift ((↑) : _ → α → β) (fun _ _ => id) rfl

Greatest Element in Supremum-Preserving Homomorphisms

Informal description

For any type $\beta$ with a greatest element $\top$ (i.e., $\beta$ is an `OrderTop`), the type of supremum-preserving homomorphisms $\text{SupHom}(\alpha, \beta)$ also has a greatest element. This greatest element is given by the constant function that maps every element of $\alpha$ to $\top$.

SupHom.instBoundedOrder instance

[BoundedOrder β] : BoundedOrder (SupHom α β)

Full source

instance [BoundedOrder β] : BoundedOrder (SupHom α β) :=
  BoundedOrder.lift ((↑) : _ → α → β) (fun _ _ => id) rfl rfl

Bounded Order Structure on Supremum-Preserving Homomorphisms

Informal description

For any type $\beta$ with a bounded order (i.e., equipped with both a greatest element $\top$ and a least element $\bot$), the type of supremum-preserving homomorphisms $\text{SupHom}(\alpha, \beta)$ also forms a bounded order, where the top and bottom elements are given by the constant functions that map every element of $\alpha$ to $\top$ and $\bot$ respectively.

SupHom.coe_sup theorem

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

Full source

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

Supremum of Supremum-Preserving Homomorphisms is Pointwise Supremum

Informal description

For any two supremum-preserving homomorphisms $f$ and $g$ between types $\alpha$ and $\beta$ equipped with a supremum operation, the underlying function of their supremum $f \sqcup g$ is equal to the pointwise supremum of the functions $f$ and $g$.

SupHom.coe_bot theorem

[Bot β] : ⇑(⊥ : SupHom α β) = ⊥

Full source

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

Bottom Supremum-Preserving Homomorphism is Constant Bottom Function

Informal description

For any type $\beta$ with a bottom element $\bot$, the underlying function of the bottom element in the type of supremum-preserving homomorphisms $\text{SupHom}(\alpha, \beta)$ is the constant function that maps every element of $\alpha$ to $\bot$.

SupHom.coe_top theorem

[Top β] : ⇑(⊤ : SupHom α β) = ⊤

Full source

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

Top Supremum-Preserving Homomorphism is Constant Top Function

Informal description

For any type $\beta$ with a top element $\top$, the underlying function of the top element in the type of supremum-preserving homomorphisms $\text{SupHom}(\alpha, \beta)$ is the constant function that maps every element of $\alpha$ to $\top$.

SupHom.sup_apply theorem

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

Full source

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

Evaluation of Supremum of Supremum-Preserving Homomorphisms

Informal description

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

SupHom.bot_apply theorem

[Bot β] (a : α) : (⊥ : SupHom α β) a = ⊥

Full source

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

Evaluation of Bottom Supremum-Preserving Homomorphism Yields Bottom Element

Informal description

For any type $\beta$ with a bottom element $\bot$ and any element $a \in \alpha$, the evaluation of the bottom element in the type of supremum-preserving homomorphisms $\text{SupHom}(\alpha, \beta)$ at $a$ equals $\bot$.

SupHom.top_apply theorem

[Top β] (a : α) : (⊤ : SupHom α β) a = ⊤

Full source

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

Evaluation of Top Supremum-Preserving Homomorphism Yields Top Element

Informal description

For any type $\beta$ with a top element $\top$ and any element $a \in \alpha$, the evaluation of the top element in the type of supremum-preserving homomorphisms $\text{SupHom}(\alpha, \beta)$ at $a$ equals $\top$.

SupHom.subtypeVal definition

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

Full source

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

Canonical supremum-preserving homomorphism from a subtype

Informal description

Given a predicate $ P $ on a type $ \beta $ such that $ P $ is closed under the supremum operation $ \sqcup $, the function `SupHom.subtypeVal` is the canonical supremum-preserving homomorphism from the subtype $ \{x : \beta \mid P x\} $ to $ \beta $. Here, the subtype is equipped with the induced supremum operation from $ \beta $.

SupHom.subtypeVal_apply theorem

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

Full source

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

Canonical Supremum-Preserving Homomorphism Acts as Identity on Subtype Elements

Informal description

Let $\beta$ be a type with a supremum operation $\sqcup$, and let $P$ be a predicate on $\beta$ such that for any $x, y \in \beta$ satisfying $P$, their supremum $x \sqcup y$ also satisfies $P$. Then for any element $x$ in the subtype $\{x \in \beta \mid P x\}$, the application of the canonical supremum-preserving homomorphism $\text{subtypeVal}$ to $x$ equals $x$ itself.

SupHom.subtypeVal_coe theorem

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

Full source

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

Canonical Supremum-Preserving Homomorphism Coincides with Subtype Inclusion

Informal description

Given a type $\beta$ with a supremum operation $\sqcup$ and a predicate $P$ on $\beta$ that is closed under $\sqcup$ (i.e., for any $x, y \in \beta$ satisfying $P$, their supremum $x \sqcup y$ also satisfies $P$), the underlying function of the canonical supremum-preserving homomorphism $\text{subtypeVal}$ from the subtype $\{x \in \beta \mid P x\}$ to $\beta$ is equal to the subtype inclusion function $\text{Subtype.val}$.

InfHom.instFunLike instance

: FunLike (InfHom α β) α β

Full source

instance : FunLike (InfHom α β) α β where
  coe := InfHom.toFun
  coe_injective' f g h := by cases f; cases g; congr

Function-Like Structure of Infimum-Preserving Functions

Informal description

For any types $\alpha$ and $\beta$ equipped with infimum operations, the type of infimum-preserving functions $\text{InfHom}(\alpha, \beta)$ can be treated as a function-like type, meaning there is a canonical way to view an infimum-preserving function as a plain function from $\alpha$ to $\beta$.

InfHom.instInfHomClass instance

: InfHomClass (InfHom α β) α β

Full source

instance : InfHomClass (InfHom α β) α β where
  map_inf := InfHom.map_inf'

Infimum-Preserving Homomorphisms Form an InfHomClass

Informal description

For any types $\alpha$ and $\beta$ equipped with infimum operations, the type of infimum-preserving homomorphisms $\text{InfHom}(\alpha, \beta)$ forms an instance of the class $\text{InfHomClass}$. This means that every infimum-preserving homomorphism between $\alpha$ and $\beta$ preserves the infimum operation, i.e., for any $f \in \text{InfHom}(\alpha, \beta)$ and $x, y \in \alpha$, we have $f(x \sqcap y) = f(x) \sqcap f(y)$.

InfHom.toFun_eq_coe theorem

(f : InfHom α β) : f.toFun = (f : α → β)

Full source

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

Underlying Function of Infimum-Preserving Homomorphism Equals Its Coercion

Informal description

For any infimum-preserving homomorphism $f \colon \alpha \to \beta$, the underlying function $f.\text{toFun}$ is equal to the coercion of $f$ to a function.

InfHom.coe_mk theorem

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

Full source

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

Coefficient of Infimum-Preserving Homomorphism Construction Equals Original Function

Informal description

For any function $f \colon \alpha \to \beta$ and proof $hf$ that $f$ preserves infima, the underlying function of the infimum-preserving homomorphism $\text{InfHom.mk}\, f\, hf$ is equal to $f$.

InfHom.ext theorem

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

Full source

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

Extensionality of Infimum-Preserving Homomorphisms

Informal description

For any two infimum-preserving homomorphisms $f, g \colon \alpha \to \beta$, if $f(a) = g(a)$ for all $a \in \alpha$, then $f = g$.

InfHom.copy definition

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

Full source

/-- Copy of an `InfHom` with a new `toFun` equal to the old one. Useful to fix definitional
equalities. -/
protected def copy (f : InfHom α β) (f' : α → β) (h : f' = f) : InfHom α β where
  toFun := f'
  map_inf' := h.symm ▸ f.map_inf'

Copy of an infimum-preserving function with a new underlying function

Informal description

Given an infimum-preserving function $f \colon \alpha \to \beta$ and a function $f' \colon \alpha \to \beta$ that is definitionally equal to $f$, the function `InfHom.copy` constructs a new infimum-preserving function with $f'$ as its underlying function, while preserving the infimum-preserving property of $f$.

InfHom.coe_copy theorem

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

Full source

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

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

Informal description

For any infimum-preserving function $f \colon \alpha \to \beta$ and any function $f' \colon \alpha \to \beta$ such that $f' = f$, the underlying function of the copied infimum-preserving function $f.copy\, f'\, h$ is equal to $f'$.

InfHom.copy_eq theorem

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

Full source

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

Copy of Infimum-Preserving Function Equals Original

Informal description

Let $f \colon \alpha \to \beta$ be an infimum-preserving function between types $\alpha$ and $\beta$ equipped with infimum operations. 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.

InfHom.id definition

: InfHom α α

Full source

/-- `id` as an `InfHom`. -/
protected def id : InfHom α α :=
  ⟨id, fun _ _ => rfl⟩

Identity infimum-preserving homomorphism

Informal description

The identity function on a type $\alpha$ equipped with an infimum operation, viewed as an infimum-preserving homomorphism. That is, the function maps each element to itself and preserves the infimum operation: for any two elements $x, y \in \alpha$, the infimum of $x$ and $y$ is mapped to the infimum of their images (which are $x$ and $y$ themselves).

InfHom.instInhabited instance

: Inhabited (InfHom α α)

Full source

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

Inhabited Type of Infimum-Preserving Homomorphisms

Informal description

For any type $\alpha$ equipped with an infimum operation, the type of infimum-preserving homomorphisms from $\alpha$ to itself is inhabited.

InfHom.coe_id theorem

: ⇑(InfHom.id α) = id

Full source

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

Identity Infimum-Preserving Homomorphism as Identity Function

Informal description

The underlying function of the identity infimum-preserving homomorphism on a type $\alpha$ equipped with an infimum operation is equal to the identity function on $\alpha$, i.e., $\text{id}_\alpha$.

InfHom.id_apply theorem

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

Full source

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

Identity Infimum-Preserving Homomorphism Acts as Identity Function

Informal description

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

InfHom.comp definition

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

Full source

/-- Composition of `InfHom`s as an `InfHom`. -/
def comp (f : InfHom β γ) (g : InfHom α β) : InfHom α γ where
  toFun := f ∘ g
  map_inf' a b := by rw [comp_apply, map_inf, map_inf]; rfl

Composition of infimum-preserving functions

Informal description

The composition of two infimum-preserving functions $ f \colon \beta \to \gamma $ and $ g \colon \alpha \to \beta $ is an infimum-preserving function $ f \circ g \colon \alpha \to \gamma $. Specifically, for any $ a, b \in \alpha $, the function satisfies $ (f \circ g)(a \sqcap b) = f(g(a)) \sqcap f(g(b)) $.

InfHom.coe_comp theorem

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

Full source

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

Composition of Infimum-Preserving Functions as Pointwise Composition

Informal description

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

InfHom.comp_apply theorem

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

Full source

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

Composition of Infimum-Preserving Functions Evaluated at a Point

Informal description

For any infimum-preserving functions $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))$.

InfHom.comp_assoc theorem

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

Full source

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

Associativity of Composition for Infimum-Preserving Functions

Informal description

For any infimum-preserving functions $f \colon \gamma \to \delta$, $g \colon \beta \to \gamma$, and $h \colon \alpha \to \beta$, the composition of functions is associative, i.e., $(f \circ g) \circ h = f \circ (g \circ h)$.

InfHom.comp_id theorem

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

Full source

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

Right Identity Law for Composition of Infimum-Preserving Functions

Informal description

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

InfHom.id_comp theorem

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

Full source

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

Left Identity Law for Composition of Infimum-Preserving Functions

Informal description

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

InfHom.cancel_right theorem

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

Full source

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

Right Cancellation Property for Composition of Infimum-Preserving Functions

Informal description

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

InfHom.cancel_left theorem

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

Full source

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

Left Cancellation Property for Composition of Infimum-Preserving Functions

Informal description

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

InfHom.const definition

(b : β) : InfHom α β

Full source

/-- The constant function as an `InfHom`. -/
def const (b : β) : InfHom α β := ⟨fun _ ↦ b, fun _ _ ↦ (inf_idem _).symm⟩

Constant infimum-preserving function

Informal description

The constant function that maps every element of a type $\alpha$ to a fixed element $b$ in a type $\beta$ is an infimum-preserving function. This means that for any two elements in $\alpha$, their infimum is mapped to the infimum of their images in $\beta$, which is simply $b$ since the function is constant.

InfHom.coe_const theorem

(b : β) : ⇑(const α b) = Function.const α b

Full source

@[simp]
theorem coe_const (b : β) : ⇑(const α b) = Function.const α b :=
  rfl

Constant Infimum-Preserving Map as Constant Function

Informal description

For a fixed element $b$ in a type $\beta$ equipped with an infimum operation, the underlying function of the constant infimum-preserving map from $\alpha$ to $\beta$ is equal to the constant function that maps every element of $\alpha$ to $b$. In symbols: if $\text{const}_{\alpha}(b) : \text{InfHom}(\alpha, \beta)$ is the constant infimum-preserving map, then its underlying function $\text{const}_{\alpha}(b)(a) = b$ for all $a \in \alpha$.

InfHom.const_apply theorem

(b : β) (a : α) : const α b a = b

Full source

@[simp]
theorem const_apply (b : β) (a : α) : const α b a = b :=
  rfl

Evaluation of Constant Infimum-Preserving Function

Informal description

For any fixed element $b$ in a type $\beta$ and any element $a$ in a type $\alpha$, the constant infimum-preserving function $\text{const}_{\alpha}(b)$ evaluated at $a$ equals $b$, i.e., $\text{const}_{\alpha}(b)(a) = b$.

InfHom.instMin instance

: Min (InfHom α β)

Full source

instance : Min (InfHom α β) :=
  ⟨fun f g =>
    ⟨f ⊓ g, fun a b => by
      rw [Pi.inf_apply, map_inf, map_inf]
      exact inf_inf_inf_comm _ _ _ _⟩⟩

Minimum Operation on Infimum-Preserving Functions

Informal description

For any types $\alpha$ and $\beta$ equipped with infimum operations, the type of infimum-preserving functions $\text{InfHom}(\alpha, \beta)$ is equipped with a minimum operation.

InfHom.instSemilatticeInf instance

: SemilatticeInf (InfHom α β)

Full source

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

Meet-Semilattice Structure on Infimum-Preserving Functions

Informal description

For any types $\alpha$ and $\beta$ equipped with infimum operations, the type of infimum-preserving functions $\text{InfHom}(\alpha, \beta)$ forms a meet-semilattice, where the infimum operation is defined pointwise.

InfHom.instBot instance

[Bot β] : Bot (InfHom α β)

Full source

instance [Bot β] : Bot (InfHom α β) :=
  ⟨InfHom.const α ⊥⟩

Bottom Element in Infimum-Preserving Functions

Informal description

For any type $\beta$ with a bottom element $\bot$, the type of infimum-preserving functions from $\alpha$ to $\beta$ has a bottom element given by the constant function that maps every element of $\alpha$ to $\bot$.

InfHom.instTop instance

[Top β] : Top (InfHom α β)

Full source

instance [Top β] : Top (InfHom α β) :=
  ⟨InfHom.const α ⊤⟩

Top Element in Infimum-Preserving Functions

Informal description

For any type $\beta$ with a top element $\top$, the type of infimum-preserving functions from $\alpha$ to $\beta$ has a top element given by the constant function that maps every element of $\alpha$ to $\top$.

InfHom.instOrderBot instance

[OrderBot β] : OrderBot (InfHom α β)

Full source

instance [OrderBot β] : OrderBot (InfHom α β) :=
  OrderBot.lift ((↑) : _ → α → β) (fun _ _ => id) rfl

Bottom Element in the Order of Infimum-Preserving Functions

Informal description

For any types $\alpha$ and $\beta$ where $\beta$ has a bottom element $\bot$ in its order, the type of infimum-preserving functions $\text{InfHom}(\alpha, \beta)$ inherits an order with a bottom element. The bottom element is given by the constant function that maps every element of $\alpha$ to $\bot$.

InfHom.instOrderTop instance

[OrderTop β] : OrderTop (InfHom α β)

Full source

instance [OrderTop β] : OrderTop (InfHom α β) :=
  OrderTop.lift ((↑) : _ → α → β) (fun _ _ => id) rfl

Order with Top Element on Infimum-Preserving Functions

Informal description

For any type $\beta$ with a greatest element $\top$ in its order, the type of infimum-preserving functions from $\alpha$ to $\beta$ forms an order with a top element, where the top element is given by the constant function that maps every element of $\alpha$ to $\top$.

InfHom.instBoundedOrder instance

[BoundedOrder β] : BoundedOrder (InfHom α β)

Full source

instance [BoundedOrder β] : BoundedOrder (InfHom α β) :=
  BoundedOrder.lift ((↑) : _ → α → β) (fun _ _ => id) rfl rfl

Bounded Order Structure on Infimum-Preserving Functions

Informal description

For any type $\beta$ with a bounded order (i.e., $\beta$ has both a greatest element $\top$ and a least element $\bot$), the type of infimum-preserving functions $\text{InfHom}(\alpha, \beta)$ also forms a bounded order. The greatest element is the constant function that maps every element of $\alpha$ to $\top$, and the least element is the constant function that maps every element of $\alpha$ to $\bot$.

InfHom.coe_inf theorem

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

Full source

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

Pointwise Infimum of Infimum-Preserving Functions

Informal description

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

InfHom.coe_bot theorem

[Bot β] : ⇑(⊥ : InfHom α β) = ⊥

Full source

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

Bottom Infimum-Preserving Function is Constant $\bot$ Function

Informal description

For any type $\beta$ with a bottom element $\bot$, the underlying function of the bottom element in the type of infimum-preserving functions from $\alpha$ to $\beta$ is the constant function that maps every element of $\alpha$ to $\bot$.

InfHom.coe_top theorem

[Top β] : ⇑(⊤ : InfHom α β) = ⊤

Full source

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

Top Infimum-Preserving Function is Constant $\top$ Function

Informal description

For any type $\beta$ with a top element $\top$, the underlying function of the top element in the type of infimum-preserving functions from $\alpha$ to $\beta$ is the constant function that maps every element of $\alpha$ to $\top$.

InfHom.inf_apply theorem

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

Full source

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

Evaluation of Infimum of Infimum-Preserving Functions

Informal description

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

InfHom.bot_apply theorem

[Bot β] (a : α) : (⊥ : InfHom α β) a = ⊥

Full source

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

Evaluation of Bottom Infimum-Preserving Function Yields Bottom Element

Informal description

For any type $\beta$ with a bottom element $\bot$ and any element $a \in \alpha$, the evaluation of the bottom infimum-preserving function $\bot \colon \text{InfHom}(\alpha, \beta)$ at $a$ equals $\bot$.

InfHom.top_apply theorem

[Top β] (a : α) : (⊤ : InfHom α β) a = ⊤

Full source

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

Evaluation of Top Infimum-Preserving Function Yields Top Element

Informal description

For any type $\beta$ with a top element $\top$ and any element $a \in \alpha$, the evaluation of the top infimum-preserving function $\top \colon \text{InfHom}(\alpha, \beta)$ at $a$ equals $\top$.

InfHom.subtypeVal definition

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

Full source

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

Inclusion map as an infimum-preserving homomorphism

Informal description

Given a predicate $ P $ on a type $ \beta $ and a proof that $ 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) $ also holds), the function `InfHom.subtypeVal` is the canonical inclusion map from the subtype $ \{x \in \beta \mid P(x)\} $ to $ \beta $, viewed as an infimum-preserving homomorphism. Here, the subtype is equipped with the infimum operation inherited from $ \beta $.

InfHom.subtypeVal_apply theorem

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

Full source

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

Inclusion Map Acts as Identity on Subtype Elements

Informal description

Let $P$ be a predicate on a type $\beta$ such that for any $x, y \in \beta$, if $P(x)$ and $P(y)$ hold, then $P(x \sqcap y)$ also holds. For any element $x$ in the subtype $\{x \in \beta \mid P(x)\}$, the inclusion map $\text{subtypeVal}\, P_{\text{inf}}$ satisfies $\text{subtypeVal}\, P_{\text{inf}}(x) = x$.

InfHom.subtypeVal_coe theorem

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

Full source

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

Inclusion Map as Subtype Projection for Infimum-Preserving Predicates

Informal description

Given a predicate $P$ on a type $\beta$ such that for any $x, y \in \beta$, if $P(x)$ and $P(y)$ hold, then $P(x \sqcap y)$ also holds, the underlying function of the inclusion map $\text{subtypeVal}\, P_{\text{inf}}$ is equal to the canonical projection $\text{Subtype.val}$ from the subtype $\{x \in \beta \mid P(x)\}$ to $\beta$.

LatticeHom.toInfHom definition

(f : LatticeHom α β) : InfHom α β

Full source

/-- Reinterpret a `LatticeHom` as an `InfHom`. -/
def toInfHom (f : LatticeHom α β) : InfHom α β :=
  { f with }

Lattice homomorphism as infimum-preserving homomorphism

Informal description

Given a lattice homomorphism $f$ between lattices $\alpha$ and $\beta$, this function reinterprets $f$ as an infimum-preserving homomorphism (i.e., a function that preserves the $\sqcap$ operation).

LatticeHom.instFunLike instance

: FunLike (LatticeHom α β) α β

Full source

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

Lattice Homomorphisms as Functions

Informal description

For any two lattices $\alpha$ and $\beta$, a lattice homomorphism $f : \alpha \to \beta$ can be treated as a function from $\alpha$ to $\beta$.

LatticeHom.instLatticeHomClass instance

: LatticeHomClass (LatticeHom α β) α β

Full source

instance : LatticeHomClass (LatticeHom α β) α β where
  map_sup f := f.map_sup'
  map_inf f := f.map_inf'

Lattice Homomorphisms Form a Lattice Homomorphism Class

Informal description

For any two lattices $\alpha$ and $\beta$, the type `LatticeHom α β` of lattice homomorphisms from $\alpha$ to $\beta$ forms a `LatticeHomClass`, meaning every lattice homomorphism preserves both supremums ($\sqcup$) and infimums ($\sqcap$).

LatticeHom.toFun_eq_coe theorem

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

Full source

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

Lattice Homomorphism Function Equality

Informal description

For any lattice homomorphism $f$ between lattices $\alpha$ and $\beta$, the underlying function $f$ is equal to its coercion to a function.

LatticeHom.coe_toSupHom theorem

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

Full source

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

Equality of Lattice Homomorphism and its Supremum-Preserving Component

Informal description

For any lattice homomorphism $f$ between lattices $\alpha$ and $\beta$, the underlying function of the supremum-preserving homomorphism $f.\text{toSupHom}$ is equal to $f$ itself.

LatticeHom.coe_toInfHom theorem

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

Full source

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

Equality of Lattice Homomorphism and its Infimum-Preserving Component

Informal description

For any lattice homomorphism $f$ between lattices $\alpha$ and $\beta$, the underlying function of the infimum-preserving homomorphism $f.\text{toInfHom}$ is equal to $f$ itself.

LatticeHom.coe_mk theorem

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

Full source

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

Equality of Constructed Lattice Homomorphism with Original Function

Informal description

Given a supremum-preserving homomorphism $f : \alpha \to \beta$ between lattices $\alpha$ and $\beta$, and a proof $hf$ that $f$ also preserves infima, the underlying function of the lattice homomorphism constructed from $f$ and $hf$ is equal to $f$ itself. In other words, if we construct a lattice homomorphism from $f$ by proving it preserves both $\sqcup$ and $\sqcap$, then the resulting homomorphism acts exactly as $f$ on all inputs.

LatticeHom.ext theorem

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

Full source

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

Extensionality of Lattice Homomorphisms

Informal description

For any two lattice homomorphisms $f, g \colon \alpha \to \beta$ between lattices $\alpha$ and $\beta$, if $f(a) = g(a)$ for all $a \in \alpha$, then $f = g$.

LatticeHom.copy definition

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

Full source

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

Copy of a lattice homomorphism with a new function definition

Informal description

Given a 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 lattice homomorphism with $f'$ as its underlying function, while preserving both the supremum and infimum preserving properties of $f$.

LatticeHom.coe_copy theorem

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

Full source

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

Underlying Function of Copied Lattice Homomorphism Equals Given Function

Informal description

Let $f \colon \alpha \to \beta$ be a lattice homomorphism between 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'$.

LatticeHom.copy_eq theorem

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

Full source

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

Copy of Lattice Homomorphism Equals Original

Informal description

Given a lattice homomorphism $f \colon \alpha \to \beta$ and a function $f' \colon \alpha \to \beta$ such that $f' = f$, the copy of $f$ with $f'$ as its underlying function is equal to $f$ itself.

LatticeHom.id definition

: LatticeHom α α

Full source

/-- `id` as a `LatticeHom`. -/
protected def id : LatticeHom α α where
  toFun := id
  map_sup' _ _ := rfl
  map_inf' _ _ := rfl

Identity lattice homomorphism

Informal description

The identity function as a lattice homomorphism from a lattice $\alpha$ to itself, preserving both supremum ($\sqcup$) and infimum ($\sqcap$) operations.

LatticeHom.instInhabited instance

: Inhabited (LatticeHom α α)

Full source

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

Inhabited Type of Lattice Endomorphisms

Informal description

For any lattice $\alpha$, the type of lattice homomorphisms from $\alpha$ to itself is inhabited, with the identity function as a canonical element.

LatticeHom.coe_id theorem

: ⇑(LatticeHom.id α) = id

Full source

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

Identity Lattice Homomorphism as Identity Function

Informal description

The underlying function of the identity lattice homomorphism on a lattice $\alpha$ is equal to the identity function $\text{id} : \alpha \to \alpha$.

LatticeHom.id_apply theorem

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

Full source

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

Identity Lattice Homomorphism Evaluation

Informal description

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

LatticeHom.comp definition

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

Full source

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

Composition of lattice homomorphisms

Informal description

The composition of two lattice homomorphisms $ f \colon \beta \to \gamma $ and $ g \colon \alpha \to \beta $ is a lattice homomorphism $ f \circ g \colon \alpha \to \gamma $. Specifically, for any $ a, b \in \alpha $, the function satisfies both: \[ (f \circ g)(a \sqcup b) = f(g(a)) \sqcup f(g(b)) \quad \text{and} \quad (f \circ g)(a \sqcap b) = f(g(a)) \sqcap f(g(b)). \]

LatticeHom.coe_comp theorem

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

Full source

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

Composition of Lattice Homomorphisms as Function Composition

Informal description

For any 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 $f$ and $g$, i.e., $(f \circ g)(a) = f(g(a))$ for all $a \in \alpha$.

LatticeHom.comp_apply theorem

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

Full source

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

Composition of Lattice Homomorphisms Evaluates Pointwise

Informal description

For any lattice 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))$.

LatticeHom.coe_comp_sup_hom' theorem

(f : LatticeHom β γ) (g : LatticeHom α β) : ⟨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 : LatticeHom β γ) (g : LatticeHom α β) :
    ⟨f ∘ g, map_sup (f.comp g)⟩ = (f : SupHom β γ).comp g :=
  rfl

Composition of Lattice Homomorphisms as Supremum-Preserving Homomorphisms

Informal description

For any lattice homomorphisms $f \colon \beta \to \gamma$ and $g \colon \alpha \to \beta$, the supremum-preserving homomorphism obtained by composing $f$ and $g$ (as lattice homomorphisms) is equal to the composition of $f$ and $g$ viewed as supremum-preserving homomorphisms. Specifically, the underlying function is $f \circ g$ and it preserves suprema.

LatticeHom.coe_comp_sup_hom theorem

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

Full source

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

Compatibility of Lattice Homomorphism Composition with Supremum-Preserving Structure

Informal description

For any lattice homomorphisms $f \colon \beta \to \gamma$ and $g \colon \alpha \to \beta$, the composition $f \circ g$ considered as a supremum-preserving homomorphism from $\alpha$ to $\gamma$ is equal to the composition of $f$ and $g$ considered as supremum-preserving homomorphisms. In other words, the following diagram commutes: \[ (f \circ g)_{\text{SupHom}} = f_{\text{SupHom}} \circ g_{\text{SupHom}} \] where the subscripts denote the respective homomorphism structures.

LatticeHom.coe_comp_inf_hom' theorem

(f : LatticeHom β γ) (g : LatticeHom α β) : ⟨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 : LatticeHom β γ) (g : LatticeHom α β) :
    ⟨f ∘ g, map_inf (f.comp g)⟩ = (f : InfHom β γ).comp g :=
  rfl

Composition of Lattice Homomorphisms as Infimum-Preserving Functions

Informal description

Let $f \colon \beta \to \gamma$ and $g \colon \alpha \to \beta$ be lattice homomorphisms between lattices $\alpha$, $\beta$, and $\gamma$. Then the infimum-preserving function obtained by composing $f$ and $g$ (as lattice homomorphisms) is equal to the composition of $f$ and $g$ viewed as infimum-preserving functions. That is, the pair $\langle f \circ g, \text{map\_inf} (f \circ g) \rangle$ equals $(f \colon \text{InfHom} \beta \gamma) \circ g$.

LatticeHom.coe_comp_inf_hom theorem

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

Full source

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

Compatibility of Lattice Homomorphism Composition with Infimum-Preserving Function Composition

Informal description

For any lattice homomorphisms $f \colon \beta \to \gamma$ and $g \colon \alpha \to \beta$, the infimum-preserving function obtained by composing $f$ and $g$ as lattice homomorphisms is equal to the composition of $f$ and $g$ viewed as infimum-preserving functions. That is, $(f \circ g)_{\text{InfHom}} = f_{\text{InfHom}} \circ g_{\text{InfHom}}$.

LatticeHom.comp_assoc theorem

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

Full source

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

Associativity of Lattice Homomorphism Composition

Informal description

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

LatticeHom.comp_id theorem

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

Full source

@[simp]
theorem comp_id (f : LatticeHom α β) : f.comp (LatticeHom.id α) = f :=
  LatticeHom.ext fun _ => rfl

Right Identity Law for Lattice Homomorphism Composition

Informal description

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

LatticeHom.id_comp theorem

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

Full source

@[simp]
theorem id_comp (f : LatticeHom α β) : (LatticeHom.id β).comp f = f :=
  LatticeHom.ext fun _ => rfl

Left identity property of lattice homomorphism composition

Informal description

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

LatticeHom.cancel_right theorem

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

Full source

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

Right Cancellation Property for Lattice Homomorphisms

Informal description

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

LatticeHom.cancel_left theorem

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

Full source

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

Left Cancellation Property for Injective Lattice Homomorphisms

Informal description

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

LatticeHom.subtypeVal definition

 {P : β → Prop} (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
  LatticeHom { x : β // P x } β

Full source

/-- `Subtype.val` as a `LatticeHom`. -/
def subtypeVal {P : β → Prop}
    (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
    LatticeHom {x : β // P x} β :=
  letI := Subtype.lattice Psup Pinf
  .mk (SupHom.subtypeVal Psup) (by simp [Subtype.coe_inf Pinf])

Canonical lattice homomorphism from a subtype

Informal description

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

LatticeHom.subtypeVal_apply theorem

 {P : β → Prop} (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 Psup Pinf x = x

Full source

@[simp]
lemma subtypeVal_apply {P : β → Prop}
    (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 Psup Pinf x = x := rfl

Subtype Projection as Lattice Homomorphism Preserves Elements

Informal description

Let $\beta$ be a lattice and $P$ a predicate on $\beta$ such that for any $x, y \in \beta$, if $P(x)$ and $P(y)$ hold, then both $P(x \sqcup y)$ and $P(x \sqcap y)$ hold. For any element $x$ in the subtype $\{x : \beta \mid P x\}$, the lattice homomorphism $\text{subtypeVal}$ applied to $x$ equals $x$ itself.

LatticeHom.subtypeVal_coe theorem

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

Full source

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

Subtype Projection as Lattice Homomorphism

Informal description

Given a lattice $\beta$ and a predicate $P$ on $\beta$ that is closed under both the supremum $\sqcup$ and infimum $\sqcap$ operations, the underlying function of the canonical lattice homomorphism from the subtype $\{x : \beta \mid P x\}$ to $\beta$ is equal to the subtype projection function $\text{Subtype.val}$.

OrderHomClass.toLatticeHomClass instance

: LatticeHomClass F α β

Full source

/-- An order homomorphism from a linear order is a lattice homomorphism. -/
instance (priority := 100) toLatticeHomClass : LatticeHomClass F α β :=
  { ‹OrderHomClass F α β› with
    map_sup := fun f a b => by
      obtain h | h := le_total a b
      · rw [sup_eq_right.2 h, sup_eq_right.2 (OrderHomClass.mono f h : f a ≤ f b)]
      · rw [sup_eq_left.2 h, sup_eq_left.2 (OrderHomClass.mono f h : f b ≤ f a)]
    map_inf := fun f a b => by
      obtain h | h := le_total a b
      · rw [inf_eq_left.2 h, inf_eq_left.2 (OrderHomClass.mono f h : f a ≤ f b)]
      · rw [inf_eq_right.2 h, inf_eq_right.2 (OrderHomClass.mono f h : f b ≤ f a)] }

Order-Preserving Functions are Lattice Homomorphisms

Informal description

For any type `F` representing order-preserving functions between two linear orders `α` and `β`, the class `OrderHomClass F α β` implies that `F` is also a `LatticeHomClass`. This means that every order-preserving function between linear orders automatically preserves both the supremum (`⊔`) and infimum (`⊓`) operations.

OrderHomClass.toLatticeHom definition

(f : F) : LatticeHom α β

Full source

/-- Reinterpret an order homomorphism to a linear order as a `LatticeHom`. -/
def toLatticeHom (f : F) : LatticeHom α β := f

Order-preserving function as a lattice homomorphism

Informal description

Given a function $f$ between two linear orders $\alpha$ and $\beta$ that preserves the order structure, this definition reinterprets $f$ as a lattice homomorphism between the corresponding lattices. Specifically, it constructs a `LatticeHom` from $f$ where the lattice operations (supremum and infimum) are preserved.

OrderHomClass.coe_to_lattice_hom theorem

(f : F) : ⇑(toLatticeHom α β f) = f

Full source

@[simp]
theorem coe_to_lattice_hom (f : F) : ⇑(toLatticeHom α β f) = f :=
  rfl

Coercion of Order-Preserving Function to Lattice Homomorphism Preserves Function

Informal description

For any order-preserving function $f$ between two linear orders $\alpha$ and $\beta$, the underlying function of the lattice homomorphism constructed from $f$ is equal to $f$ itself.

OrderHomClass.to_lattice_hom_apply theorem

(f : F) (a : α) : toLatticeHom α β f a = f a

Full source

@[simp]
theorem to_lattice_hom_apply (f : F) (a : α) : toLatticeHom α β f a = f a :=
  rfl

Lattice Homomorphism Construction Preserves Function Application

Informal description

For any order-preserving function $f \colon \alpha \to \beta$ between two linear orders $\alpha$ and $\beta$, the application of the lattice homomorphism constructed from $f$ to an element $a \in \alpha$ is equal to $f(a)$, i.e., $\text{toLatticeHom}(f)(a) = f(a)$.

SupHom.dual definition

: SupHom α β ≃ InfHom αᵒᵈ βᵒᵈ

Full source

/-- Reinterpret a supremum homomorphism as an infimum homomorphism between the dual lattices. -/
@[simps]
protected def dual : SupHomSupHom α β ≃ InfHom αᵒᵈ βᵒᵈ where
  toFun f := ⟨f, f.map_sup'⟩
  invFun f := ⟨f, f.map_inf'⟩
  left_inv _ := rfl
  right_inv _ := rfl

Duality between supremum and infimum homomorphisms

Informal description

The equivalence between the type of supremum-preserving homomorphisms $\text{SupHom}(\alpha, \beta)$ and the type of infimum-preserving homomorphisms $\text{InfHom}(\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 supremum-preserving homomorphism $f \colon \alpha \to \beta$, the corresponding infimum-preserving homomorphism maps elements in $\alpha^\text{op}$ to $\beta^\text{op}$ by applying $f$. Conversely, given an infimum-preserving homomorphism $g \colon \alpha^\text{op} \to \beta^\text{op}$, the corresponding supremum-preserving homomorphism maps elements in $\alpha$ to $\beta$ by applying $g$.

SupHom.dual_id theorem

: SupHom.dual (SupHom.id α) = InfHom.id _

Full source

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

Duality Maps Identity Supremum Homomorphism to Identity Infimum Homomorphism

Informal description

The duality equivalence maps the identity supremum-preserving homomorphism on a lattice $\alpha$ to the identity infimum-preserving homomorphism on the order-dual lattice $\alpha^\text{op}$. That is, $\text{SupHom.dual}(\text{SupHom.id}_\alpha) = \text{InfHom.id}_{\alpha^\text{op}}$.

SupHom.dual_comp theorem

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

Full source

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

Duality Equivalence Preserves Composition of Supremum-Preserving Homomorphisms

Informal description

For any two supremum-preserving homomorphisms $f \colon \alpha \to \beta$ and $g \colon \beta \to \gamma$, the duality equivalence maps the composition $g \circ f$ to the composition of the duality equivalences of $g$ and $f$. That is, $$ \text{SupHom.dual}(g \circ f) = \text{SupHom.dual}(g) \circ \text{SupHom.dual}(f). $$

SupHom.symm_dual_id theorem

: SupHom.dual.symm (InfHom.id _) = SupHom.id α

Full source

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

Identity Homomorphism Preservation under Duality Inverse

Informal description

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

SupHom.symm_dual_comp theorem

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

Full source

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

Composition of Infimum-Preserving Homomorphisms under Duality Inverse

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be types equipped with order structures, and let $\alpha^\text{op}$, $\beta^\text{op}$, and $\gamma^\text{op}$ denote their order-dual lattices. For any infimum-preserving homomorphisms $f \colon \alpha^\text{op} \to \beta^\text{op}$ and $g \colon \beta^\text{op} \to \gamma^\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$ individually. That is, $$ \text{SupHom.dual.symm}(g \circ f) = (\text{SupHom.dual.symm} g) \circ (\text{SupHom.dual.symm} f). $$

InfHom.dual definition

: InfHom α β ≃ SupHom αᵒᵈ βᵒᵈ

Full source

/-- Reinterpret an infimum homomorphism as a supremum homomorphism between the dual lattices. -/
@[simps]
protected def dual : InfHomInfHom α β ≃ SupHom αᵒᵈ βᵒᵈ where
  toFun f := ⟨f, f.map_inf'⟩
  invFun f := ⟨f, f.map_sup'⟩
  left_inv _ := rfl
  right_inv _ := rfl

Duality between infimum and supremum homomorphisms

Informal description

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

InfHom.dual_id theorem

: InfHom.dual (InfHom.id α) = SupHom.id _

Full source

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

Duality of Identity Infimum-Preserving Homomorphism: $\text{InfHom.dual}(\text{id}) = \text{SupHom.id}$

Informal description

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

InfHom.dual_comp theorem

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

Full source

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

Duality of Composition of Infimum-Preserving Homomorphisms

Informal description

For any 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{InfHom.dual}(g \circ f) = \text{InfHom.dual}(g) \circ \text{InfHom.dual}(f)$.

InfHom.symm_dual_id theorem

: InfHom.dual.symm (SupHom.id _) = InfHom.id α

Full source

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

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

Informal description

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

InfHom.symm_dual_comp theorem

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

Full source

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

Inverse Duality Preserves Composition of Supremum Homomorphisms

Informal description

For any supremum-preserving homomorphisms $f \colon \alpha^\text{op} \to \beta^\text{op}$ and $g \colon \beta^\text{op} \to \gamma^\text{op}$, the inverse of the duality equivalence for infimum-preserving homomorphisms satisfies \[ \text{InfHom.dual.symm}(g \circ f) = \text{InfHom.dual.symm}(g) \circ \text{InfHom.dual.symm}(f). \]

LatticeHom.dual definition

: LatticeHom α β ≃ LatticeHom αᵒᵈ βᵒᵈ

Full source

/-- Reinterpret a lattice homomorphism as a lattice homomorphism between the dual lattices. -/
@[simps]
protected def dual : LatticeHomLatticeHom α β ≃ LatticeHom αᵒᵈ βᵒᵈ where
  toFun f := ⟨InfHom.dual f.toInfHom, f.map_sup'⟩
  invFun f := ⟨SupHom.dual.symm f.toInfHom, f.map_sup'⟩
  left_inv _ := rfl
  right_inv _ := rfl

Duality of lattice homomorphisms

Informal description

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

LatticeHom.dual_id theorem

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

Full source

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

Dual of Identity Lattice Homomorphism is Identity on Dual Lattice

Informal description

The dual of the identity lattice homomorphism on a lattice $\alpha$ is equal to the identity lattice homomorphism on the order dual $\alpha^\text{op}$.

LatticeHom.dual_comp theorem

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

Full source

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

Duality of Composition of Lattice Homomorphisms

Informal description

For any lattice homomorphisms $f \colon \alpha \to \beta$ and $g \colon \beta \to \gamma$, the dual of the composition $g \circ f$ is equal to the composition of the duals of $g$ and $f$. That is, the following diagram commutes: \[ (g \circ f)^\text{op} = g^\text{op} \circ f^\text{op}. \]

LatticeHom.symm_dual_id theorem

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

Full source

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

Inverse Duality of Identity Lattice Homomorphism

Informal description

The inverse of the duality equivalence for lattice homomorphisms, when applied to the identity homomorphism on the order dual of a lattice $\alpha$, yields the identity homomorphism on $\alpha$. In other words, if we take the identity lattice homomorphism on $\alpha^\text{op}$ and apply the inverse of the duality equivalence, we get back the identity homomorphism on $\alpha$.

LatticeHom.symm_dual_comp theorem

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

Full source

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

Inverse Dual Preserves Composition of Lattice Homomorphisms

Informal description

For any lattice homomorphisms $f \colon \alpha^\text{op} \to \beta^\text{op}$ and $g \colon \beta^\text{op} \to \gamma^\text{op}$, the inverse of the dual of their composition equals the composition of the inverses of their duals. That is, \[ (LatticeHom.dual.symm) (g \circ f) = (LatticeHom.dual.symm g) \circ (LatticeHom.dual.symm f). \]

LatticeHom.fst definition

: LatticeHom (α × β) α

Full source

/-- Natural projection homomorphism from `α × β` to `α`. -/
def fst : LatticeHom (α × β) α where
  toFun := Prod.fst
  map_sup' _ _ := rfl
  map_inf' _ _ := rfl

First projection lattice homomorphism

Informal description

The natural projection homomorphism from the product lattice $\alpha \times \beta$ to $\alpha$, which maps each pair $(x, y)$ to its first component $x$. This homomorphism preserves both the supremum ($\sqcup$) and infimum ($\sqcap$) operations.

LatticeHom.snd definition

: LatticeHom (α × β) β

Full source

/-- Natural projection homomorphism from `α × β` to `β`. -/
def snd : LatticeHom (α × β) β where
  toFun := Prod.snd
  map_sup' _ _ := rfl
  map_inf' _ _ := rfl

Second projection lattice homomorphism

Informal description

The natural projection homomorphism from the product lattice $\alpha \times \beta$ to $\beta$, which maps each pair $(x, y)$ to its second component $y$. This homomorphism preserves both the supremum ($\sqcup$) and infimum ($\sqcap$) operations.

LatticeHom.coe_fst theorem

: ⇑(fst (α := α) (β := β)) = Prod.fst

Full source

@[simp, norm_cast] lemma coe_fst : ⇑(fst (α := α) (β := β)) = Prod.fst := rfl

First Projection Lattice Homomorphism as Standard Projection

Informal description

The underlying function of the first projection lattice homomorphism from the product lattice $\alpha \times \beta$ to $\alpha$ is equal to the standard first projection function $\operatorname{fst} : \alpha \times \beta \to \alpha$, which maps each pair $(x, y)$ to $x$.

LatticeHom.coe_snd theorem

: ⇑(snd (α := α) (β := β)) = Prod.snd

Full source

@[simp, norm_cast] lemma coe_snd : ⇑(snd (α := α) (β := β)) = Prod.snd := rfl

Second Projection Lattice Homomorphism as Standard Projection

Informal description

The underlying function of the second projection lattice homomorphism from the product lattice $\alpha \times \beta$ to $\beta$ is equal to the standard second projection function $\operatorname{snd} : \alpha \times \beta \to \beta$, which maps each pair $(x, y)$ to $y$.

LatticeHom.fst_apply theorem

(x : α × β) : fst x = x.fst

Full source

lemma fst_apply (x : α × β) : fst x = x.fst := rfl

First Projection Lattice Homomorphism Evaluates to First Component

Informal description

For any element $x = (a, b)$ in the product lattice $\alpha \times \beta$, the first projection lattice homomorphism applied to $x$ equals the first component $a$ of $x$, i.e., $\operatorname{fst}(x) = a$.

LatticeHom.snd_apply theorem

(x : α × β) : snd x = x.snd

Full source

lemma snd_apply (x : α × β) : snd x = x.snd := rfl

Second Projection Lattice Homomorphism Evaluates to Second Component

Informal description

For any element $x = (a, b)$ in the product lattice $\alpha \times \beta$, the second projection lattice homomorphism applied to $x$ equals the second component $b$ of $x$, i.e., $\operatorname{snd}(x) = b$.

Pi.evalLatticeHom definition

(i : ι) : LatticeHom (∀ i, α i) (α i)

Full source

/-- Evaluation as a lattice homomorphism. -/
def evalLatticeHom (i : ι) : LatticeHom (∀ i, α i) (α i) where
  toFun := Function.eval i
  map_sup' _a _b := rfl
  map_inf' _a _b := rfl

Evaluation lattice homomorphism at index $i$

Informal description

For each index $i$ in the type $\iota$, the function $\operatorname{evalLatticeHom}_i$ is a lattice homomorphism from the product lattice $\prod_{i} \alpha_i$ to the lattice $\alpha_i$. Specifically, it evaluates a function $f$ in the product lattice at the index $i$, preserving both supremum and infimum operations.

Pi.coe_evalLatticeHom theorem

(i : ι) : ⇑(evalLatticeHom (α := α) i) = Function.eval i

Full source

@[simp, norm_cast]
lemma coe_evalLatticeHom (i : ι) : ⇑(evalLatticeHom (α := α) i) = Function.eval i := rfl

Evaluation Lattice Homomorphism as Function Evaluation

Informal description

For any index $i$ in the type $\iota$, the underlying function of the evaluation lattice homomorphism $\operatorname{evalLatticeHom}_i$ from the product lattice $\prod_{i} \alpha_i$ to $\alpha_i$ is equal to the standard evaluation function at $i$, i.e., $\operatorname{evalLatticeHom}_i(f) = f(i)$ for all $f \in \prod_{i} \alpha_i$.

Pi.evalLatticeHom_apply theorem

(i : ι) (f : ∀ i, α i) : evalLatticeHom i f = f i

Full source

lemma evalLatticeHom_apply (i : ι) (f : ∀ i, α i) : evalLatticeHom i f = f i := rfl

Evaluation of Lattice Homomorphism at Index $i$

Informal description

For any index $i$ in the type $\iota$ and any function $f$ in the product lattice $\prod_{i} \alpha_i$, the evaluation lattice homomorphism at index $i$ satisfies $\operatorname{evalLatticeHom}_i(f) = f(i)$.

Mathlib.Order.Hom.Lattice

Types of morphisms

Typeclasses