Mathlib.Order.Hom.CompleteLattice

sSupHom structure

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

Full source

/-- The type of `⨆`-preserving functions from `α` to `β`. -/
structure sSupHom (α β : Type*) [SupSet α] [SupSet β] where
  /-- The underlying function of a sSupHom. -/
  toFun : α → β
  /-- The proposition that a `sSupHom` commutes with arbitrary suprema/joins. -/
  map_sSup' (s : Set α) : toFun (sSup s) = sSup (toFun '' s)

Supremum-preserving function

Informal description

The structure representing functions between types `α` and `β` (equipped with supremum operations) that preserve arbitrary suprema (joins). Specifically, a function `f : α → β` is a `sSupHom` if for any subset `s ⊆ α`, we have `f (⨆ s) = ⨆ (f '' s)`.

sInfHom structure

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

Full source

/-- The type of `⨅`-preserving functions from `α` to `β`. -/
structure sInfHom (α β : Type*) [InfSet α] [InfSet β] where
  /-- The underlying function of an `sInfHom`. -/
  toFun : α → β
  /-- The proposition that a `sInfHom` commutes with arbitrary infima/meets -/
  map_sInf' (s : Set α) : toFun (sInf s) = sInf (toFun '' s)

Infimum-preserving homomorphism

Informal description

The structure representing functions between types `α` and `β` equipped with infimum operations that preserve arbitrary infima (i.e., functions `f : α → β` such that for any family of elements `{aᵢ}` in `α`, `f (⨅ aᵢ) = ⨅ (f aᵢ)`).

FrameHom structure

(α β : Type*) [CompleteLattice α] [CompleteLattice β] extends
  InfTopHom α β

Full source

/-- The type of frame homomorphisms from `α` to `β`. They preserve finite meets and arbitrary joins.
-/
structure FrameHom (α β : Type*) [CompleteLattice α] [CompleteLattice β] extends
  InfTopHom α β where
  /-- The proposition that frame homomorphisms commute with arbitrary suprema/joins. -/
  map_sSup' (s : Set α) : toFun (sSup s) = sSup (toFun '' s)

Frame Homomorphism

Informal description

The structure representing frame homomorphisms between complete lattices $\alpha$ and $\beta$. A frame homomorphism is a map that preserves arbitrary suprema (joins), finite infima (meets), and the top element.

CompleteLatticeHom structure

(α β : Type*) [CompleteLattice α] [CompleteLattice β] extends
  sInfHom α β

Full source

/-- The type of complete lattice homomorphisms from `α` to `β`. -/
structure CompleteLatticeHom (α β : Type*) [CompleteLattice α] [CompleteLattice β] extends
  sInfHom α β where
  /-- The proposition that complete lattice homomorphism commutes with arbitrary suprema/joins. -/
  map_sSup' (s : Set α) : toFun (sSup s) = sSup (toFun '' s)

Complete lattice homomorphism

Informal description

A complete lattice homomorphism from a complete lattice $\alpha$ to a complete lattice $\beta$ is a function that preserves arbitrary suprema (joins) and infima (meets). More precisely, a complete lattice homomorphism $f : \alpha \to \beta$ satisfies: - $f(\bigsqcup S) = \bigsqcup f(S)$ for any subset $S \subseteq \alpha$ - $f(\bigsqcap S) = \bigsqcap f(S)$ for any subset $S \subseteq \alpha$ where $\bigsqcup$ and $\bigsqcap$ denote the supremum and infimum operations respectively.

sSupHomClass structure

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

Full source

/-- `sSupHomClass F α β` states that `F` is a type of `⨆`-preserving morphisms.

You should extend this class when you extend `sSupHom`. -/
class sSupHomClass (F α β : Type*) [SupSet α] [SupSet β] [FunLike F α β] : Prop where
  /-- The proposition that members of `sSupHomClass`s commute with arbitrary suprema/joins. -/
  map_sSup (f : F) (s : Set α) : f (sSup s) = sSup (f '' s)

Class of supremum-preserving functions

Informal description

The class `sSupHomClass F α β` states that `F` is a type of functions between types `α` and `β` equipped with supremum operations, where each function in `F` preserves arbitrary suprema (joins). More precisely, for any `f : F` and any subset `S ⊆ α`, we have `f(⨆ S) = ⨆ f(S)`.

sInfHomClass structure

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

Full source

/-- `sInfHomClass F α β` states that `F` is a type of `⨅`-preserving morphisms.

You should extend this class when you extend `sInfHom`. -/
class sInfHomClass (F α β : Type*) [InfSet α] [InfSet β] [FunLike F α β] : Prop where
  /-- The proposition that members of `sInfHomClass`s commute with arbitrary infima/meets. -/
  map_sInf (f : F) (s : Set α) : f (sInf s) = sInf (f '' s)

Class of infimum-preserving functions

Informal description

The class `sInfHomClass F α β` states that `F` is a type of functions between types `α` and `β` equipped with infimum operations, where each function in `F` preserves arbitrary infima (meets). More precisely, for any `f : F` and any subset `S ⊆ α`, we have `f(⨅ S) = ⨅ f(S)`.

FrameHomClass structure

(F α β : Type*) [CompleteLattice α] [CompleteLattice β] [FunLike F α β] : Prop
  extends InfTopHomClass F α β

Full source

/-- `FrameHomClass F α β` states that `F` is a type of frame morphisms. They preserve `⊓` and `⨆`.

You should extend this class when you extend `FrameHom`. -/
class FrameHomClass (F α β : Type*) [CompleteLattice α] [CompleteLattice β] [FunLike F α β] : Prop
  extends InfTopHomClass F α β where
  /-- The proposition that members of `FrameHomClass` commute with arbitrary suprema/joins. -/
  map_sSup (f : F) (s : Set α) : f (sSup s) = sSup (f '' s)

Frame Homomorphism Class

Informal description

The class `FrameHomClass F α β` states that `F` is a type of frame homomorphisms between complete lattices `α` and `β`. These are functions that preserve arbitrary suprema (joins), finite infima (meets), and the top element. More precisely, for any `f : F`, the function `f` satisfies: 1. Preservation of arbitrary suprema: $f(\bigsqcup S) = \bigsqcup f(S)$ for any subset $S \subseteq \alpha$ 2. Preservation of finite infima: $f(a \sqcap b) = f(a) \sqcap f(b)$ for any $a, b \in \alpha$ 3. Preservation of top element: $f(\top) = \top$

CompleteLatticeHomClass structure

(F α β : Type*) [CompleteLattice α] [CompleteLattice β]
    [FunLike F α β] : Prop
  extends sInfHomClass F α β

Full source

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

You should extend this class when you extend `CompleteLatticeHom`. -/
class CompleteLatticeHomClass (F α β : Type*) [CompleteLattice α] [CompleteLattice β]
    [FunLike F α β] : Prop
  extends sInfHomClass F α β where
  /-- The proposition that members of `CompleteLatticeHomClass` commute with arbitrary
  suprema/joins. -/
  map_sSup (f : F) (s : Set α) : f (sSup s) = sSup (f '' s)

Complete Lattice Homomorphism Class

Informal description

The class `CompleteLatticeHomClass F α β` states that `F` is a type of complete lattice homomorphisms between complete lattices `α` and `β`. These are functions that preserve arbitrary suprema (joins) and infima (meets). More precisely, for any `f : F`, the function `f` preserves all suprema (i.e., `f (⨆ i, g i) = ⨆ i, f (g i)` for any family `g`) and all infima (i.e., `f (⨅ i, g i) = ⨅ i, f (g i)` for any family `g`).

map_iSup theorem

[SupSet α] [SupSet β] [sSupHomClass F α β] (f : F) (g : ι → α) : f (⨆ i, g i) = ⨆ i, f (g i)

Full source

@[simp] theorem map_iSup [SupSet α] [SupSet β] [sSupHomClass F α β] (f : F) (g : ι → α) :
    f (⨆ i, g i) = ⨆ i, f (g i) := by simp [iSup, ← Set.range_comp, Function.comp_def]

Preservation of Suprema by Supremum-Preserving Functions

Informal description

Let $\alpha$ and $\beta$ be types equipped with supremum operations, and let $F$ be a type of functions from $\alpha$ to $\beta$ that preserves arbitrary suprema. For any function $f \in F$ and any family of elements $(g_i)_{i \in \iota}$ in $\alpha$, we have: \[ f\left(\bigsqcup_{i} g_i\right) = \bigsqcup_{i} f(g_i). \]

map_iSup₂ theorem

 [SupSet α] [SupSet β] [sSupHomClass F α β] (f : F) (g : ∀ i, κ i → α) : f (⨆ (i) (j), g i j) = ⨆ (i) (j), f (g i j)

Full source

theorem map_iSup₂ [SupSet α] [SupSet β] [sSupHomClass F α β] (f : F) (g : ∀ i, κ i → α) :
    f (⨆ (i) (j), g i j) = ⨆ (i) (j), f (g i j) := by simp_rw [map_iSup]

Preservation of Double Suprema by Supremum-Preserving Functions

Informal description

Let $\alpha$ and $\beta$ be types equipped with supremum operations, and let $F$ be a type of functions from $\alpha$ to $\beta$ that preserves arbitrary suprema. For any function $f \in F$ and any doubly-indexed family of elements $(g_{i,j})_{i \in \iota, j \in \kappa_i}$ in $\alpha$, we have: \[ f\left(\bigsqcup_{i,j} g_{i,j}\right) = \bigsqcup_{i,j} f(g_{i,j}). \]

map_iInf theorem

[InfSet α] [InfSet β] [sInfHomClass F α β] (f : F) (g : ι → α) : f (⨅ i, g i) = ⨅ i, f (g i)

Full source

@[simp] theorem map_iInf [InfSet α] [InfSet β] [sInfHomClass F α β] (f : F) (g : ι → α) :
    f (⨅ i, g i) = ⨅ i, f (g i) := by simp [iInf, ← Set.range_comp, Function.comp_def]

Preservation of Infima by Infimum-Preserving Functions

Informal description

Let $\alpha$ and $\beta$ be complete lattices (or more generally, types equipped with infimum operations), and let $F$ be a type of functions from $\alpha$ to $\beta$ that preserves arbitrary infima. For any function $f \in F$ and any family of elements $(g_i)_{i \in \iota}$ in $\alpha$, we have: \[ f\left(\bigsqcap_{i} g_i\right) = \bigsqcap_{i} f(g_i). \]

map_iInf₂ theorem

 [InfSet α] [InfSet β] [sInfHomClass F α β] (f : F) (g : ∀ i, κ i → α) : f (⨅ (i) (j), g i j) = ⨅ (i) (j), f (g i j)

Full source

theorem map_iInf₂ [InfSet α] [InfSet β] [sInfHomClass F α β] (f : F) (g : ∀ i, κ i → α) :
    f (⨅ (i) (j), g i j) = ⨅ (i) (j), f (g i j) := by simp_rw [map_iInf]

Preservation of Doubly-Indexed Infima by Infimum-Preserving Functions

Informal description

Let $\alpha$ and $\beta$ be complete lattices (or more generally, types equipped with infimum operations), and let $F$ be a type of functions from $\alpha$ to $\beta$ that preserves arbitrary infima. For any function $f \in F$ and any doubly-indexed family of elements $(g_{i,j})_{i \in \iota, j \in \kappa_i}$ in $\alpha$, we have: \[ f\left(\bigsqcap_{i,j} g_{i,j}\right) = \bigsqcap_{i,j} f(g_{i,j}). \]

sSupHomClass.toSupBotHomClass instance

[CompleteLattice α] [CompleteLattice β] [sSupHomClass F α β] : SupBotHomClass F α β

Full source

instance (priority := 100) sSupHomClass.toSupBotHomClass [CompleteLattice α]
    [CompleteLattice β] [sSupHomClass F α β] : SupBotHomClass F α β :=
  {  ‹sSupHomClass F α β› with
    map_sup := fun f a b => by
      rw [← sSup_pair, map_sSup]
      simp only [Set.image_pair, sSup_insert, sSup_singleton]
    map_bot := fun f => by
      rw [← sSup_empty, map_sSup, Set.image_empty, sSup_empty] }

Supremum-Preserving Functions Preserve Finite Suprema and Bottom Element

Informal description

For any complete lattices $\alpha$ and $\beta$, every function $f \in F$ that preserves arbitrary suprema (i.e., $f(\bigsqcup S) = \bigsqcup f(S)$ for any $S \subseteq \alpha$) also preserves finite suprema and the bottom element. In other words, the class of supremum-preserving functions is a subclass of the class of functions that preserve finite suprema and the bottom element.

sInfHomClass.toInfTopHomClass instance

[CompleteLattice α] [CompleteLattice β] [sInfHomClass F α β] : InfTopHomClass F α β

Full source

instance (priority := 100) sInfHomClass.toInfTopHomClass [CompleteLattice α]
    [CompleteLattice β] [sInfHomClass F α β] : InfTopHomClass F α β :=
  { ‹sInfHomClass F α β› with
    map_inf := fun f a b => by
      rw [← sInf_pair, map_sInf, Set.image_pair]
      simp only [Set.image_pair, sInf_insert, sInf_singleton]
    map_top := fun f => by
      rw [← sInf_empty, map_sInf, Set.image_empty, sInf_empty] }

Infimum-Preserving Functions Preserve Finite Infima and Top Element

Informal description

For any complete lattices $\alpha$ and $\beta$, every function $f \in F$ that preserves arbitrary infima (i.e., $f(\bigsqcap S) = \bigsqcap f(S)$ for any $S \subseteq \alpha$) also preserves finite infima and the top element. In other words, the class of infimum-preserving functions is a subclass of the class of functions that preserve finite infima and the top element.

FrameHomClass.tosSupHomClass instance

[CompleteLattice α] [CompleteLattice β] [FrameHomClass F α β] : sSupHomClass F α β

Full source

instance (priority := 100) FrameHomClass.tosSupHomClass [CompleteLattice α]
    [CompleteLattice β] [FrameHomClass F α β] : sSupHomClass F α β :=
  { ‹FrameHomClass F α β› with }

Frame Homomorphisms Preserve Arbitrary Suprema

Informal description

For any complete lattices $\alpha$ and $\beta$, every frame homomorphism between $\alpha$ and $\beta$ preserves arbitrary suprema. That is, if $f$ is a frame homomorphism, then for any subset $S \subseteq \alpha$, we have $f(\bigsqcup S) = \bigsqcup f(S)$.

FrameHomClass.toBoundedLatticeHomClass instance

[CompleteLattice α] [CompleteLattice β] [FrameHomClass F α β] : BoundedLatticeHomClass F α β

Full source

instance (priority := 100) FrameHomClass.toBoundedLatticeHomClass [CompleteLattice α]
    [CompleteLattice β] [FrameHomClass F α β] : BoundedLatticeHomClass F α β :=
  { ‹FrameHomClass F α β›, sSupHomClass.toSupBotHomClass with }

Frame Homomorphisms are Bounded Lattice Homomorphisms

Informal description

For any complete lattices $\alpha$ and $\beta$, every frame homomorphism between $\alpha$ and $\beta$ is also a bounded lattice homomorphism. That is, a function that preserves arbitrary suprema, finite infima, and the top element also preserves finite suprema, finite infima, the top element, and the bottom element.

CompleteLatticeHomClass.toFrameHomClass instance

[CompleteLattice α] [CompleteLattice β] [CompleteLatticeHomClass F α β] : FrameHomClass F α β

Full source

instance (priority := 100) CompleteLatticeHomClass.toFrameHomClass [CompleteLattice α]
    [CompleteLattice β] [CompleteLatticeHomClass F α β] : FrameHomClass F α β :=
  { ‹CompleteLatticeHomClass F α β›, sInfHomClass.toInfTopHomClass with }

Complete Lattice Homomorphisms are Frame Homomorphisms

Informal description

For any complete lattices $\alpha$ and $\beta$, every complete lattice homomorphism between $\alpha$ and $\beta$ is also a frame homomorphism. That is, any function that preserves arbitrary suprema and infima also preserves finite infima and the top element.

CompleteLatticeHomClass.toBoundedLatticeHomClass instance

[CompleteLattice α] [CompleteLattice β] [CompleteLatticeHomClass F α β] : BoundedLatticeHomClass F α β

Full source

instance (priority := 100) CompleteLatticeHomClass.toBoundedLatticeHomClass [CompleteLattice α]
    [CompleteLattice β] [CompleteLatticeHomClass F α β] : BoundedLatticeHomClass F α β :=
  { sSupHomClass.toSupBotHomClass, sInfHomClass.toInfTopHomClass with }

Complete Lattice Homomorphisms are Bounded Lattice Homomorphisms

Informal description

For any complete lattices $\alpha$ and $\beta$, every complete lattice homomorphism between $\alpha$ and $\beta$ is also a bounded lattice homomorphism. That is, any function that preserves arbitrary suprema and infima also preserves finite suprema, finite infima, the top element, and the bottom element.

OrderIsoClass.tosSupHomClass instance

[CompleteLattice α] [CompleteLattice β] [OrderIsoClass F α β] : sSupHomClass F α β

Full source

instance (priority := 100) OrderIsoClass.tosSupHomClass [CompleteLattice α]
    [CompleteLattice β] [OrderIsoClass F α β] : sSupHomClass F α β :=
  { show OrderHomClass F α β from inferInstance with
    map_sSup := fun f s =>
      eq_of_forall_ge_iff fun c => by
        simp only [← le_map_inv_iff, sSup_le_iff, Set.forall_mem_image] }

Order Isomorphisms Preserve Suprema

Informal description

For any complete lattices $\alpha$ and $\beta$, every order isomorphism between $\alpha$ and $\beta$ preserves arbitrary suprema.

OrderIsoClass.tosInfHomClass instance

[CompleteLattice α] [CompleteLattice β] [OrderIsoClass F α β] : sInfHomClass F α β

Full source

instance (priority := 100) OrderIsoClass.tosInfHomClass [CompleteLattice α]
    [CompleteLattice β] [OrderIsoClass F α β] : sInfHomClass F α β :=
  { show OrderHomClass F α β from inferInstance with
    map_sInf := fun f s =>
      eq_of_forall_le_iff fun c => by
        simp only [← map_inv_le_iff, le_sInf_iff, Set.forall_mem_image] }

Order Isomorphisms Preserve Infima

Informal description

For any complete lattices $\alpha$ and $\beta$, and any type $F$ that is an instance of `OrderIsoClass` (representing order isomorphisms between $\alpha$ and $\beta$), $F$ is also an instance of `sInfHomClass`. This means that every order isomorphism in $F$ preserves arbitrary infima (meets).

OrderIsoClass.toCompleteLatticeHomClass instance

[CompleteLattice α] [CompleteLattice β] [OrderIsoClass F α β] : CompleteLatticeHomClass F α β

Full source

instance (priority := 100) OrderIsoClass.toCompleteLatticeHomClass [CompleteLattice α]
    [CompleteLattice β] [OrderIsoClass F α β] : CompleteLatticeHomClass F α β :=
  { OrderIsoClass.tosSupHomClass, OrderIsoClass.tosInfHomClass with }

Order Isomorphisms are Complete Lattice Homomorphisms

Informal description

For any complete lattices $\alpha$ and $\beta$, every order isomorphism between $\alpha$ and $\beta$ is also a complete lattice homomorphism. That is, it preserves arbitrary suprema and infima.

OrderIso.toCompleteLatticeHom definition

[CompleteLattice α] [CompleteLattice β] (f : OrderIso α β) : CompleteLatticeHom α β

Full source

/-- Reinterpret an order isomorphism as a morphism of complete lattices. -/
@[simps] def OrderIso.toCompleteLatticeHom [CompleteLattice α] [CompleteLattice β]
    (f : OrderIso α β) : CompleteLatticeHom α β where
  toFun := f
  map_sInf' := sInfHomClass.map_sInf f
  map_sSup' := sSupHomClass.map_sSup f

Order isomorphism as complete lattice homomorphism

Informal description

Given an order isomorphism $f$ between two complete lattices $\alpha$ and $\beta$, this definition reinterprets $f$ as a complete lattice homomorphism. Specifically, the homomorphism preserves arbitrary suprema and infima, meaning: - $f(\bigsqcup S) = \bigsqcup f(S)$ for any subset $S \subseteq \alpha$ - $f(\bigsqcap S) = \bigsqcap f(S)$ for any subset $S \subseteq \alpha$ where $\bigsqcup$ and $\bigsqcap$ denote the supremum and infimum operations respectively.

instCoeTCSSupHomOfSSupHomClass instance

[SupSet α] [SupSet β] [sSupHomClass F α β] : CoeTC F (sSupHom α β)

Full source

instance [SupSet α] [SupSet β] [sSupHomClass F α β] : CoeTC F (sSupHom α β) :=
  ⟨fun f => ⟨f, map_sSup f⟩⟩

Canonical View of Supremum-Preserving Homomorphisms

Informal description

For any types $\alpha$ and $\beta$ equipped with supremum operations, and any type $F$ of supremum-preserving functions from $\alpha$ to $\beta$, there is a canonical way to view elements of $F$ as supremum-preserving homomorphisms in $\text{sSupHom}(\alpha, \beta)$. This means that any function $f \in F$ can be treated as a homomorphism that preserves arbitrary suprema.

instCoeTCSInfHomOfSInfHomClass instance

[InfSet α] [InfSet β] [sInfHomClass F α β] : CoeTC F (sInfHom α β)

Full source

instance [InfSet α] [InfSet β] [sInfHomClass F α β] : CoeTC F (sInfHom α β) :=
  ⟨fun f => ⟨f, map_sInf f⟩⟩

Canonical View of Infimum-Preserving Homomorphisms

Informal description

For any types $\alpha$ and $\beta$ equipped with infimum operations, and any type $F$ of infimum-preserving functions from $\alpha$ to $\beta$, there is a canonical way to view elements of $F$ as infimum-preserving homomorphisms in $\mathrm{sInfHom}(\alpha, \beta)$. This means that any function $f \in F$ can be treated as a homomorphism that preserves arbitrary infima.

instCoeTCFrameHomOfFrameHomClass instance

[CompleteLattice α] [CompleteLattice β] [FrameHomClass F α β] : CoeTC F (FrameHom α β)

Full source

instance [CompleteLattice α] [CompleteLattice β] [FrameHomClass F α β] : CoeTC F (FrameHom α β) :=
  ⟨fun f => ⟨f, map_sSup f⟩⟩

Canonical View of Frame Homomorphisms

Informal description

For any complete lattices $\alpha$ and $\beta$, and any type $F$ of frame homomorphisms from $\alpha$ to $\beta$, there is a canonical way to view elements of $F$ as frame homomorphisms in $\text{FrameHom}(\alpha, \beta)$. This means that any function $f \in F$ can be treated as a frame homomorphism that preserves arbitrary suprema, finite infima, and the top element.

instCoeTCCompleteLatticeHomOfCompleteLatticeHomClass instance

[CompleteLattice α] [CompleteLattice β] [CompleteLatticeHomClass F α β] : CoeTC F (CompleteLatticeHom α β)

Full source

instance [CompleteLattice α] [CompleteLattice β] [CompleteLatticeHomClass F α β] :
    CoeTC F (CompleteLatticeHom α β) :=
  ⟨fun f => ⟨f, map_sSup f⟩⟩

Canonical View of Complete Lattice Homomorphisms

Informal description

For any complete lattices $\alpha$ and $\beta$, and any type $F$ of complete lattice homomorphisms from $\alpha$ to $\beta$, there is a canonical way to view elements of $F$ as complete lattice homomorphisms in $\text{CompleteLatticeHom}(\alpha, \beta)$. This means that any function $f \in F$ can be treated as a complete lattice homomorphism that preserves arbitrary suprema and infima.

sSupHom.instFunLike instance

: FunLike (sSupHom α β) α β

Full source

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

Function-Like Structure for Supremum-Preserving Maps

Informal description

For any types $\alpha$ and $\beta$ equipped with supremum operations, the type of supremum-preserving functions $\alpha \to \beta$ can be treated as a function-like type, meaning each such function can be coerced to an ordinary function from $\alpha$ to $\beta$.

sSupHom.instSSupHomClass instance

: sSupHomClass (sSupHom α β) α β

Full source

instance : sSupHomClass (sSupHom α β) α β where
  map_sSup := sSupHom.map_sSup'

Class of Supremum-Preserving Functions

Informal description

For any types $\alpha$ and $\beta$ equipped with supremum operations, the type of supremum-preserving functions $\alpha \to \beta$ forms a class of functions that preserve arbitrary suprema. That is, for any $f$ in this class and any subset $S \subseteq \alpha$, we have $f(\bigsqcup S) = \bigsqcup f(S)$.

sSupHom.toFun_eq_coe theorem

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

Full source

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

Underlying function equals coercion for supremum-preserving maps

Informal description

For any supremum-preserving function $f$ between complete lattices $\alpha$ and $\beta$, the underlying function of $f$ (accessed via `f.toFun`) is equal to the function obtained by coercing $f$ to a function (denoted by $f$ itself).

sSupHom.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 Function Equals Original Function

Informal description

For any function $f \colon \alpha \to \beta$ that preserves arbitrary suprema (i.e., satisfies $f(\bigsqcup S) = \bigsqcup f(S)$ for all $S \subseteq \alpha$), the coercion of the constructed `sSupHom` term `mk f hf` to a function equals $f$ itself.

sSupHom.ext theorem

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

Full source

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

Extensionality of Supremum-Preserving Functions

Informal description

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

sSupHom.copy definition

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

Full source

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

Copy of a supremum-preserving function

Informal description

Given a supremum-preserving function $f \colon \alpha \to \beta$ and a function $f' \colon \alpha \to \beta$ that is definitionally equal to $f$, the function `sSupHom.copy` constructs a new supremum-preserving function with $f'$ as its underlying function. This is useful for maintaining definitional equalities when working with such functions.

sSupHom.coe_copy theorem

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

Full source

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

Coefficient of Copied Supremum-Preserving Function Equals Implementation

Informal description

For any supremum-preserving function $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 implementation is equal to $f'$.

sSupHom.copy_eq theorem

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

Full source

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

Copy of Supremum-Preserving Function Equals Original

Informal description

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

sSupHom.id definition

: sSupHom α α

Full source

/-- `id` as a `sSupHom`. -/
protected def id : sSupHom α α :=
  ⟨id, fun s => by rw [id, Set.image_id]⟩

Identity as a supremum-preserving function

Informal description

The identity function on a type $\alpha$ equipped with a supremum operation, viewed as a supremum-preserving function. Specifically, it maps any element $x \in \alpha$ to itself and preserves arbitrary suprema: for any subset $s \subseteq \alpha$, we have $\text{id}(\bigvee s) = \bigvee (\text{id} '' s)$.

sSupHom.instInhabited instance

: Inhabited (sSupHom α α)

Full source

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

Inhabitedness of Supremum-Preserving Functions

Informal description

For any type $\alpha$ equipped with a supremum operation, the type of supremum-preserving functions from $\alpha$ to itself is inhabited (i.e., contains at least one element, namely the identity function).

sSupHom.coe_id theorem

: ⇑(sSupHom.id α) = id

Full source

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

Identity Supremum-Preserving Homomorphism as Identity Function

Informal description

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

sSupHom.id_apply theorem

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

Full source

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

Identity Supremum-Preserving Function Evaluation

Informal description

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

sSupHom.comp definition

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

Full source

/-- Composition of `sSupHom`s as a `sSupHom`. -/
def comp (f : sSupHom β γ) (g : sSupHom α β) : sSupHom α γ where
  toFun := f ∘ g
  map_sSup' s := by rw [comp_apply, map_sSup, map_sSup, Set.image_image]; simp only [Function.comp]

Composition of supremum-preserving functions

Informal description

The composition of two supremum-preserving functions $ f \colon \beta \to \gamma $ and $ g \colon \alpha \to \beta $ is again a supremum-preserving function $ \alpha \to \gamma $. Specifically, for any subset $ s \subseteq \alpha $, we have $ (f \circ g)(\bigsqcup s) = \bigsqcup (f \circ g)(s) $.

sSupHom.coe_comp theorem

(f : sSupHom β γ) (g : sSupHom α β) : ⇑(f.comp g) = f ∘ g

Full source

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

Composition of Supremum-Preserving Functions as Pointwise Composition

Informal description

For any two supremum-preserving functions $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)(x) = f(g(x))$ for all $x \in \alpha$.

sSupHom.comp_apply theorem

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

Full source

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

Application of Composition of Supremum-Preserving Functions

Informal description

For any two supremum-preserving functions $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$ equals the application of $f$ to $g(a)$, i.e., $(f \circ g)(a) = f(g(a))$.

sSupHom.comp_assoc theorem

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

Full source

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

Associativity of Composition for Supremum-Preserving Functions

Informal description

For any three supremum-preserving functions $f \colon \gamma \to \delta$, $g \colon \beta \to \gamma$, and $h \colon \alpha \to \beta$, the composition of these functions satisfies the associativity property: $$(f \circ g) \circ h = f \circ (g \circ h).$$

sSupHom.comp_id theorem

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

Full source

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

Right Identity Law for Supremum-Preserving Function Composition

Informal description

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

sSupHom.id_comp theorem

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

Full source

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

Left Identity Property of Composition for Supremum-Preserving Functions

Informal description

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

sSupHom.cancel_right theorem

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

Full source

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

Right Cancellation Property for Composition of Supremum-Preserving Functions

Informal description

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

sSupHom.cancel_left theorem

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

Full source

@[simp]
theorem cancel_left {g : sSupHom β γ} {f₁ f₂ : sSupHom α β} (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 Supremum-Preserving Functions

Informal description

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

sSupHom.instPartialOrder instance

: PartialOrder (sSupHom α β)

Full source

instance : PartialOrder (sSupHom α β) :=
  PartialOrder.lift _ DFunLike.coe_injective

Pointwise Order on Supremum-Preserving Functions

Informal description

For any types $\alpha$ and $\beta$ equipped with supremum operations, the type of supremum-preserving functions $\alpha \to \beta$ forms a partial order under the pointwise order. That is, for two such functions $f$ and $g$, we define $f \leq g$ if $f(a) \leq g(a)$ for all $a \in \alpha$.

sSupHom.instBot instance

: Bot (sSupHom α β)

Full source

instance : Bot (sSupHom α β) :=
  ⟨⟨fun _ => ⊥, fun s => by
      obtain rfl | hs := s.eq_empty_or_nonempty
      · rw [Set.image_empty, sSup_empty]
      · rw [hs.image_const, sSup_singleton]⟩⟩

Bottom Element in the Pointwise Order of Supremum-Preserving Functions

Informal description

For any types $\alpha$ and $\beta$ equipped with supremum operations, the type of supremum-preserving functions $\alpha \to \beta$ has a bottom element with respect to the pointwise order.

sSupHom.instOrderBot instance

: OrderBot (sSupHom α β)

Full source

instance : OrderBot (sSupHom α β) where
  bot := ⊥
  bot_le := fun _ _ ↦ CompleteLattice.bot_le _

Pointwise Order with Bottom Element on Supremum-Preserving Functions

Informal description

For any types $\alpha$ and $\beta$ equipped with supremum operations, the type of supremum-preserving functions $\alpha \to \beta$ forms an order with a bottom element under the pointwise order. The bottom element is the constant function that maps every element of $\alpha$ to the bottom element of $\beta$.

sSupHom.coe_bot theorem

: ⇑(⊥ : sSupHom α β) = ⊥

Full source

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

Bottom Supremum-Preserving Function is Constant Bottom Function

Informal description

The bottom element of the type of supremum-preserving functions from $\alpha$ to $\beta$ (with respect to the pointwise order) is equal to the constant bottom function, i.e., $\bot = \lambda a, \bot$.

sSupHom.bot_apply theorem

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

Full source

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

Bottom Element Evaluation in Supremum-Preserving Functions

Informal description

For any element $a$ in a type $\alpha$ equipped with a supremum operation, the bottom element of the pointwise order on supremum-preserving functions from $\alpha$ to $\beta$ (also equipped with a supremum operation) satisfies $(\bot)(a) = \bot$.

sInfHom.instFunLike instance

: FunLike (sInfHom α β) α β

Full source

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

Function-Like Structure for Infimum-Preserving Homomorphisms

Informal description

For any types $\alpha$ and $\beta$ equipped with infimum operations, the type of infimum-preserving homomorphisms $\alpha \to \beta$ has a function-like structure, meaning each homomorphism can be treated as a function from $\alpha$ to $\beta$.

sInfHom.instSInfHomClass instance

: sInfHomClass (sInfHom α β) α β

Full source

instance : sInfHomClass (sInfHom α β) α β where
  map_sInf := sInfHom.map_sInf'

Infimum-Preserving Homomorphism Class for Infimum-Preserving Homomorphisms

Informal description

For any types $\alpha$ and $\beta$ equipped with infimum operations, the type of infimum-preserving homomorphisms $\alpha \to \beta$ forms a class of functions that preserve arbitrary infima. That is, for any $f$ in this class and any subset $S \subseteq \alpha$, we have $f(\bigsqcap S) = \bigsqcap f(S)$.

sInfHom.toFun_eq_coe theorem

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

Full source

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

Underlying Function Equals Coercion for Infimum-Preserving Homomorphisms

Informal description

For any infimum-preserving homomorphism $f$ between types $\alpha$ and $\beta$ equipped with infimum operations, the underlying function of $f$ is equal to the coercion of $f$.

sInfHom.coe_mk theorem

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

Full source

@[simp] 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 : \alpha \to \beta$ that preserves arbitrary infima (i.e., $f(\bigsqcap a_i) = \bigsqcap f(a_i)$ for any family $\{a_i\}$ in $\alpha$), the coercion of the infimum-preserving homomorphism constructed from $f$ and its proof $hf$ is equal to $f$ itself. In other words, $\uparrow(\text{mk } f hf) = f$.

sInfHom.ext theorem

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

Full source

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

Extensionality for Infimum-Preserving Homomorphisms

Informal description

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

sInfHom.copy definition

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

Full source

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

Copy of an infimum-preserving homomorphism with a new function

Informal description

Given an infimum-preserving homomorphism $f : \alpha \to \beta$ and a function $f' : \alpha \to \beta$ that is definitionally equal to $f$, the function `sInfHom.copy` constructs a new infimum-preserving homomorphism with the underlying function $f'$ and the same infimum-preserving property as $f$. This is useful for fixing definitional equalities while maintaining the structure of an infimum-preserving homomorphism.

sInfHom.coe_copy theorem

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

Full source

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

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

Informal description

Let $f : \alpha \to \beta$ be an infimum-preserving homomorphism between complete lattices, and let $f' : \alpha \to \beta$ be a function such that $f' = f$. Then the underlying function of the copy of $f$ with $f'$ is equal to $f'$.

sInfHom.copy_eq theorem

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

Full source

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

Copy of Infimum-Preserving Homomorphism Equals Original

Informal description

Let $f : \alpha \to \beta$ be an infimum-preserving homomorphism between complete lattices, and let $f' : \alpha \to \beta$ be a function such that $f' = f$. Then the copy of $f$ with underlying function $f'$ is equal to $f$ itself.

sInfHom.id definition

: sInfHom α α

Full source

/-- `id` as an `sInfHom`. -/
protected def id : sInfHom α α :=
  ⟨id, fun s => by rw [id, Set.image_id]⟩

Identity infimum-preserving homomorphism

Informal description

The identity function on a type $\alpha$ equipped with an infimum operation, viewed as an infimum-preserving homomorphism. Specifically, it satisfies $f(\bigsqcap a_i) = \bigsqcap f(a_i)$ for any family of elements $\{a_i\}$ in $\alpha$.

sInfHom.instInhabited instance

: Inhabited (sInfHom α α)

Full source

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

Inhabitedness 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 (i.e., contains at least one element).

sInfHom.coe_id theorem

: ⇑(sInfHom.id α) = id

Full source

@[simp, norm_cast]
theorem coe_id : ⇑(sInfHom.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 = \text{id}$.

sInfHom.id_apply theorem

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

Full source

@[simp]
theorem id_apply (a : α) : sInfHom.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$, i.e., $\text{id}(a) = a$.

sInfHom.comp definition

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

Full source

/-- Composition of `sInfHom`s as a `sInfHom`. -/
def comp (f : sInfHom β γ) (g : sInfHom α β) : sInfHom α γ where
  toFun := f ∘ g
  map_sInf' s := by rw [comp_apply, map_sInf, map_sInf, Set.image_image]; simp only [Function.comp]

Composition of infimum-preserving homomorphisms

Informal description

The composition of two infimum-preserving homomorphisms $ f : \beta \to \gamma $ and $ g : \alpha \to \beta $ is an infimum-preserving homomorphism $ \alpha \to \gamma $, defined by the function composition $ f \circ g $. This composition preserves arbitrary infima, meaning that for any family of elements $ \{a_i\} $ in $ \alpha $, $ (f \circ g)(\bigwedge a_i) = \bigwedge (f \circ g)(a_i) $.

sInfHom.coe_comp theorem

(f : sInfHom β γ) (g : sInfHom α β) : ⇑(f.comp g) = f ∘ g

Full source

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

Composition of Infimum-Preserving Homomorphisms as Function Composition

Informal description

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

sInfHom.comp_apply theorem

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

Full source

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

Composition of Infimum-Preserving Homomorphisms Evaluates as Function Composition

Informal description

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

sInfHom.comp_assoc theorem

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

Full source

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

Associativity of Composition for Infimum-Preserving Homomorphisms

Informal description

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

sInfHom.comp_id theorem

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

Full source

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

Right Identity Law for Infimum-Preserving Homomorphisms

Informal description

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

sInfHom.id_comp theorem

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

Full source

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

Right Identity Law for Infimum-Preserving Homomorphisms

Informal description

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

sInfHom.cancel_right theorem

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

Full source

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

Right Cancellation Property for Infimum-Preserving Homomorphisms via Surjective Maps

Informal description

Let $f \colon \alpha \to \beta$ be a surjective infimum-preserving homomorphism between complete lattices, and let $g_1, g_2 \colon \beta \to \gamma$ be 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$.

sInfHom.cancel_left theorem

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

Full source

@[simp]
theorem cancel_left {g : sInfHom β γ} {f₁ f₂ : sInfHom α β} (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 Infimum-Preserving Homomorphisms

Informal description

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

sInfHom.instPartialOrder instance

: PartialOrder (sInfHom α β)

Full source

instance : PartialOrder (sInfHom α β) :=
  PartialOrder.lift _ DFunLike.coe_injective

Partial Order on Infimum-Preserving Homomorphisms

Informal description

For any types $\alpha$ and $\beta$ equipped with infimum operations, the set of infimum-preserving homomorphisms from $\alpha$ to $\beta$ forms a partial order under the pointwise ordering. That is, for $f, g \in \mathrm{sInfHom}(\alpha, \beta)$, we define $f \leq g$ if $f(a) \leq g(a)$ for all $a \in \alpha$.

sInfHom.instTop instance

: Top (sInfHom α β)

Full source

instance : Top (sInfHom α β) :=
  ⟨⟨fun _ => ⊤, fun s => by
      obtain rfl | hs := s.eq_empty_or_nonempty
      · rw [Set.image_empty, sInf_empty]
      · rw [hs.image_const, sInf_singleton]⟩⟩

Greatest Element in Infimum-Preserving Homomorphisms

Informal description

For any types $\alpha$ and $\beta$ equipped with infimum operations, the type of infimum-preserving homomorphisms from $\alpha$ to $\beta$ has a greatest element with respect to the pointwise order.

sInfHom.instOrderTop instance

: OrderTop (sInfHom α β)

Full source

instance : OrderTop (sInfHom α β) where
  top := ⊤
  le_top := fun _ _ => CompleteLattice.le_top _

Pointwise Order on Infimum-Preserving Homomorphisms with Top Element

Informal description

For any types $\alpha$ and $\beta$ equipped with infimum operations, the type of infimum-preserving homomorphisms from $\alpha$ to $\beta$ is an order with a top element under the pointwise order.

sInfHom.coe_top theorem

: ⇑(⊤ : sInfHom α β) = ⊤

Full source

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

Greatest Infimum-Preserving Homomorphism as Constant Top Function

Informal description

The greatest element in the type of infimum-preserving homomorphisms from $\alpha$ to $\beta$, when viewed as a function, is equal to the constant function that returns the greatest element $\top$ of $\beta$.

sInfHom.top_apply theorem

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

Full source

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

Greatest Infimum-Preserving Homomorphism Evaluates to Top

Informal description

For any element $a$ in a type $\alpha$ equipped with an infimum operation, the application of the greatest infimum-preserving homomorphism $\top : \alpha \to \beta$ to $a$ yields the greatest element $\top$ in $\beta$.

FrameHom.instFunLike instance

: FunLike (FrameHom α β) α β

Full source

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

Function-Like Structure of Frame Homomorphisms

Informal description

For any complete lattices $\alpha$ and $\beta$, the type of frame homomorphisms from $\alpha$ to $\beta$ can be treated as a function-like type, where each homomorphism can be coerced to a function from $\alpha$ to $\beta$.

FrameHom.instFrameHomClass instance

: FrameHomClass (FrameHom α β) α β

Full source

instance : FrameHomClass (FrameHom α β) α β where
  map_sSup f := f.map_sSup'
  map_inf f := f.map_inf'
  map_top f := f.map_top'

Frame Homomorphism Class for Frame Homomorphisms

Informal description

For any complete lattices $\alpha$ and $\beta$, the type of frame homomorphisms from $\alpha$ to $\beta$ forms a `FrameHomClass`. This means that every frame homomorphism preserves arbitrary suprema, finite infima, and the top element.

FrameHom.toLatticeHom definition

(f : FrameHom α β) : LatticeHom α β

Full source

/-- Reinterpret a `FrameHom` as a `LatticeHom`. -/
def toLatticeHom (f : FrameHom α β) : LatticeHom α β :=
  f

Frame homomorphism as lattice homomorphism

Informal description

Given a frame homomorphism $f$ between complete lattices $\alpha$ and $\beta$, this function reinterprets $f$ as a lattice homomorphism between $\alpha$ and $\beta$.

FrameHom.toFun_eq_coe theorem

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

Full source

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

Frame Homomorphism Function Coincidence

Informal description

For any frame homomorphism $f$ between complete lattices $\alpha$ and $\beta$, the underlying function $f.\mathrm{toFun}$ is equal to $f$ itself.

FrameHom.coe_toInfTopHom theorem

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

Full source

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

Frame Homomorphism Coincides with Underlying Inf-Top Homomorphism

Informal description

For any frame homomorphism $f$ between complete lattices $\alpha$ and $\beta$, the underlying function of $f$ as an infimum-top homomorphism is equal to $f$ itself.

FrameHom.coe_toLatticeHom theorem

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

Full source

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

Frame Homomorphism Coincides with Underlying Lattice Homomorphism

Informal description

For any frame homomorphism $f$ between complete lattices $\alpha$ and $\beta$, the underlying function of $f$ as a lattice homomorphism is equal to $f$ itself.

FrameHom.coe_mk theorem

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

Full source

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

Frame Homomorphism Construction Preserves Underlying Function

Informal description

Given an infimum-top homomorphism $f$ between complete lattices $\alpha$ and $\beta$, and a proof $hf$ that $f$ preserves arbitrary suprema, the underlying function of the frame homomorphism constructed from $f$ and $hf$ is equal to $f$ itself.

FrameHom.ext theorem

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

Full source

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

Extensionality of Frame Homomorphisms

Informal description

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

FrameHom.copy definition

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

Full source

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

Copy of a frame homomorphism with a new underlying function

Informal description

Given a frame homomorphism $f \colon \alpha \to \beta$ between complete lattices and a function $f' \colon \alpha \to \beta$ that is definitionally equal to $f$, the function `FrameHom.copy` constructs a new frame homomorphism with $f'$ as its underlying function while preserving the frame homomorphism structure. This is useful for maintaining definitional equalities when working with such homomorphisms.

FrameHom.coe_copy theorem

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

Full source

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

Underlying function equality for copied frame homomorphism

Informal description

Let $f \colon \alpha \to \beta$ be a frame homomorphism between complete 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 frame homomorphism $f.copy\ f'\ h$ is equal to $f'$.

FrameHom.copy_eq theorem

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

Full source

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

Copy of Frame Homomorphism Equals Original

Informal description

Given a frame homomorphism $f \colon \alpha \to \beta$ between complete lattices and a function $f' \colon \alpha \to \beta$ such that $f' = f$, the copy of $f$ with underlying function $f'$ is equal to $f$ itself.

FrameHom.id definition

: FrameHom α α

Full source

/-- `id` as a `FrameHom`. -/
protected def id : FrameHom α α :=
  { sSupHom.id α with toInfTopHom := InfTopHom.id α }

Identity frame homomorphism

Informal description

The identity function on a complete lattice $\alpha$, viewed as a frame homomorphism. It preserves arbitrary suprema, finite infima, and the top element.

FrameHom.instInhabited instance

: Inhabited (FrameHom α α)

Full source

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

Inhabited Type of Frame Homomorphisms on a Complete Lattice

Informal description

For any complete lattice $\alpha$, the type of frame homomorphisms from $\alpha$ to itself is inhabited.

FrameHom.coe_id theorem

: ⇑(FrameHom.id α) = id

Full source

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

Identity Frame Homomorphism Coercion Equals Identity Function

Informal description

The coercion of the identity frame homomorphism on a complete lattice $\alpha$ is equal to the identity function on $\alpha$, i.e., $\text{id}_{\text{FrameHom}(\alpha)} = \text{id}_{\alpha}$.

FrameHom.id_apply theorem

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

Full source

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

Identity Frame Homomorphism Acts as Identity Function

Informal description

For any element $a$ in a complete lattice $\alpha$, the identity frame homomorphism evaluated at $a$ is equal to $a$ itself, i.e., $\text{id}(a) = a$.

FrameHom.comp definition

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

Full source

/-- Composition of `FrameHom`s as a `FrameHom`. -/
def comp (f : FrameHom β γ) (g : FrameHom α β) : FrameHom α γ :=
  { (f : sSupHom β γ).comp (g : sSupHom α β) with
    toInfTopHom := f.toInfTopHom.comp g.toInfTopHom }

Composition of frame homomorphisms

Informal description

The composition of two frame homomorphisms $ f \colon \beta \to \gamma $ and $ g \colon \alpha \to \beta $ is again a frame homomorphism $ \alpha \to \gamma $. This means the composition preserves arbitrary suprema, finite infima, and the top element.

FrameHom.coe_comp theorem

(f : FrameHom β γ) (g : FrameHom α β) : ⇑(f.comp g) = f ∘ g

Full source

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

Composition of Frame Homomorphisms as Function Composition

Informal description

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

FrameHom.comp_apply theorem

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

Full source

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

Application of Composition of Frame Homomorphisms

Informal description

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

FrameHom.comp_assoc theorem

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

Full source

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

Associativity of Composition of Frame Homomorphisms

Informal description

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

FrameHom.comp_id theorem

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

Full source

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

Right Identity Law for Frame Homomorphism Composition

Informal description

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

FrameHom.id_comp theorem

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

Full source

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

Identity Frame Homomorphism Left Composition Law

Informal description

For any frame homomorphism $f \colon \alpha \to \beta$ between complete lattices $\alpha$ and $\beta$, the composition of the identity frame homomorphism on $\beta$ with $f$ is equal to $f$.

FrameHom.cancel_right theorem

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

Full source

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

Right Cancellation Property for Composition of Frame Homomorphisms under Surjectivity

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be complete lattices. Given two frame homomorphisms $g_1, g_2 \colon \beta \to \gamma$ and a surjective frame homomorphism $f \colon \alpha \to \beta$, the compositions $g_1 \circ f$ and $g_2 \circ f$ are equal if and only if $g_1 = g_2$.

FrameHom.cancel_left theorem

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

Full source

@[simp]
theorem cancel_left {g : FrameHom β γ} {f₁ f₂ : FrameHom α β} (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 Frame Homomorphisms under Injectivity

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be complete lattices. Given a frame homomorphism $g \colon \beta \to \gamma$ and two frame homomorphisms $f_1, f_2 \colon \alpha \to \beta$, if $g$ is injective, then the compositions $g \circ f_1$ and $g \circ f_2$ are equal if and only if $f_1 = f_2$.

FrameHom.instPartialOrder instance

: PartialOrder (FrameHom α β)

Full source

instance : PartialOrder (FrameHom α β) :=
  PartialOrder.lift _ DFunLike.coe_injective

Partial Order on Frame Homomorphisms

Informal description

For any complete lattices $\alpha$ and $\beta$, the type of frame homomorphisms from $\alpha$ to $\beta$ is equipped with a partial order structure, where the order is defined pointwise.

CompleteLatticeHom.instFunLike instance

: FunLike (CompleteLatticeHom α β) α β

Full source

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

Function-Like Structure for Complete Lattice Homomorphisms

Informal description

For any complete lattices $\alpha$ and $\beta$, the type of complete lattice homomorphisms from $\alpha$ to $\beta$ has a function-like structure, meaning each homomorphism can be treated as a function from $\alpha$ to $\beta$.

CompleteLatticeHom.instCompleteLatticeHomClass instance

: CompleteLatticeHomClass (CompleteLatticeHom α β) α β

Full source

instance : CompleteLatticeHomClass (CompleteLatticeHom α β) α β where
  map_sSup f := f.map_sSup'
  map_sInf f := f.map_sInf'

Complete Lattice Homomorphism Class Instance

Informal description

For any complete lattices $\alpha$ and $\beta$, the type of complete lattice homomorphisms from $\alpha$ to $\beta$ forms a `CompleteLatticeHomClass`. This means every complete lattice homomorphism preserves arbitrary suprema (joins) and infima (meets), satisfying: - $f(\bigsqcup S) = \bigsqcup f(S)$ for any subset $S \subseteq \alpha$ - $f(\bigsqcap S) = \bigsqcap f(S)$ for any subset $S \subseteq \alpha$ where $\bigsqcup$ and $\bigsqcap$ denote the supremum and infimum operations respectively.

CompleteLatticeHom.tosSupHom definition

(f : CompleteLatticeHom α β) : sSupHom α β

Full source

/-- Reinterpret a `CompleteLatticeHom` as a `sSupHom`. -/
def tosSupHom (f : CompleteLatticeHom α β) : sSupHom α β :=
  f

Complete lattice homomorphism as supremum-preserving function

Informal description

Given a complete lattice homomorphism $f$ from a complete lattice $\alpha$ to a complete lattice $\beta$, the function $f$ can be reinterpreted as a supremum-preserving function (a `sSupHom`) between $\alpha$ and $\beta$. This means $f$ preserves arbitrary suprema (joins) in addition to its existing properties as a complete lattice homomorphism.

CompleteLatticeHom.toBoundedLatticeHom definition

(f : CompleteLatticeHom α β) : BoundedLatticeHom α β

Full source

/-- Reinterpret a `CompleteLatticeHom` as a `BoundedLatticeHom`. -/
def toBoundedLatticeHom (f : CompleteLatticeHom α β) : BoundedLatticeHom α β :=
  f

Complete lattice homomorphism as bounded lattice homomorphism

Informal description

Given a complete lattice homomorphism $f$ from a complete lattice $\alpha$ to a complete lattice $\beta$, we can reinterpret $f$ as a bounded lattice homomorphism between $\alpha$ and $\beta$. This means $f$ preserves finite meets (including the top element) and finite joins (including the bottom element), in addition to its existing properties as a complete lattice homomorphism.

CompleteLatticeHom.toFun_eq_coe theorem

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

Full source

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

Underlying Function of Complete Lattice Homomorphism Coincides with Itself

Informal description

For any complete lattice homomorphism $f$ from a complete lattice $\alpha$ to a complete lattice $\beta$, the underlying function of $f$ is equal to $f$ itself when viewed as a function.

CompleteLatticeHom.coe_tosInfHom theorem

(f : CompleteLatticeHom α β) : ⇑f.tosInfHom = f

Full source

@[simp] lemma coe_tosInfHom (f : CompleteLatticeHom α β) : ⇑f.tosInfHom = f := rfl

Coercion of Infimum-Preserving Component of Complete Lattice Homomorphism

Informal description

For any complete lattice homomorphism $f$ from a complete lattice $\alpha$ to a complete lattice $\beta$, the underlying function of the infimum-preserving homomorphism associated with $f$ is equal to $f$ itself. In other words, the coercion of $f.\mathrm{to\_sInfHom}$ to a function coincides with $f$.

CompleteLatticeHom.coe_tosSupHom theorem

(f : CompleteLatticeHom α β) : ⇑f.tosSupHom = f

Full source

@[simp] lemma coe_tosSupHom (f : CompleteLatticeHom α β) : ⇑f.tosSupHom = f := rfl

Coercion of Supremum-Preserving Component of Complete Lattice Homomorphism

Informal description

For any complete lattice homomorphism $f$ from a complete lattice $\alpha$ to a complete lattice $\beta$, the underlying function of the supremum-preserving homomorphism associated with $f$ is equal to $f$ itself. In other words, the coercion of $f.\mathrm{to\_sSupHom}$ to a function coincides with $f$.

CompleteLatticeHom.coe_toBoundedLatticeHom theorem

(f : CompleteLatticeHom α β) : ⇑f.toBoundedLatticeHom = f

Full source

@[simp] lemma coe_toBoundedLatticeHom (f : CompleteLatticeHom α β) : ⇑f.toBoundedLatticeHom = f :=
rfl

Coercion of Bounded Lattice Homomorphism Component of Complete Lattice Homomorphism

Informal description

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

CompleteLatticeHom.coe_mk theorem

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

Full source

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

Underlying Function of Constructed Complete Lattice Homomorphism

Informal description

Let $f : \alpha \to \beta$ be an infimum-preserving homomorphism between complete lattices, and let $hf$ be a proof that $f$ preserves arbitrary suprema. Then the underlying function of the complete lattice homomorphism constructed from $f$ and $hf$ is equal to $f$ itself.

CompleteLatticeHom.ext theorem

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

Full source

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

Extensionality of Complete Lattice Homomorphisms

Informal description

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

CompleteLatticeHom.copy definition

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

Full source

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

Copy of a complete lattice homomorphism with a new function

Informal description

Given a complete lattice homomorphism $f \colon \alpha \to \beta$ and a function $f' \colon \alpha \to \beta$ that is definitionally equal to $f$, the function `CompleteLatticeHom.copy` constructs a new complete lattice homomorphism with $f'$ as its underlying function while preserving all the homomorphism properties of $f$. This is useful for maintaining definitional equalities when working with such homomorphisms.

CompleteLatticeHom.coe_copy theorem

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

Full source

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

Underlying function of copied complete lattice homomorphism equals copied function

Informal description

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

CompleteLatticeHom.copy_eq theorem

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

Full source

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

Copy of Complete Lattice Homomorphism Equals Original

Informal description

Given a complete 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. In other words, if $f'$ is definitionally equal to $f$, then $\text{copy}(f, f', h) = f$ where $h$ is the proof that $f' = f$.

CompleteLatticeHom.id definition

: CompleteLatticeHom α α

Full source

/-- `id` as a `CompleteLatticeHom`. -/
protected def id : CompleteLatticeHom α α :=
  { sSupHom.id α, sInfHom.id α with toFun := id }

Identity complete lattice homomorphism

Informal description

The identity function on a complete lattice $\alpha$, viewed as a complete lattice homomorphism. It preserves both arbitrary suprema and infima, satisfying: - $\text{id}(\bigsqcup S) = \bigsqcup \text{id}(S)$ for any subset $S \subseteq \alpha$ - $\text{id}(\bigsqcap S) = \bigsqcap \text{id}(S)$ for any subset $S \subseteq \alpha$

CompleteLatticeHom.instInhabited instance

: Inhabited (CompleteLatticeHom α α)

Full source

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

Inhabitedness of Complete Lattice Homomorphisms

Informal description

For any complete lattice $\alpha$, the type of complete lattice homomorphisms from $\alpha$ to itself is inhabited. In particular, the identity function is a complete lattice homomorphism.

CompleteLatticeHom.coe_id theorem

: ⇑(CompleteLatticeHom.id α) = id

Full source

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

Identity Complete Lattice Homomorphism as Identity Function

Informal description

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

CompleteLatticeHom.id_apply theorem

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

Full source

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

Identity Complete Lattice Homomorphism Acts as Identity Function

Informal description

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

CompleteLatticeHom.comp definition

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

Full source

/-- Composition of `CompleteLatticeHom`s as a `CompleteLatticeHom`. -/
def comp (f : CompleteLatticeHom β γ) (g : CompleteLatticeHom α β) : CompleteLatticeHom α γ :=
  { f.tosSupHom.comp g.tosSupHom with tosInfHom := f.tosInfHom.comp g.tosInfHom }

Composition of complete lattice homomorphisms

Informal description

The composition of two complete lattice homomorphisms $ f \colon \beta \to \gamma $ and $ g \colon \alpha \to \beta $ is again a complete lattice homomorphism $ \alpha \to \gamma $. Specifically, for any subset $ S \subseteq \alpha $, the composition satisfies: - $(f \circ g)(\bigsqcup S) = \bigsqcup (f \circ g)(S)$ - $(f \circ g)(\bigsqcap S) = \bigsqcap (f \circ g)(S)$ where $\bigsqcup$ and $\bigsqcap$ denote the supremum and infimum operations respectively.

CompleteLatticeHom.coe_comp theorem

(f : CompleteLatticeHom β γ) (g : CompleteLatticeHom α β) : ⇑(f.comp g) = f ∘ g

Full source

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

Composition of Complete Lattice Homomorphisms Preserves Function Application

Informal description

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

CompleteLatticeHom.comp_apply theorem

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

Full source

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

Application of Composition of Complete Lattice Homomorphisms

Informal description

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

CompleteLatticeHom.comp_assoc theorem

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

Full source

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

Associativity of Composition for Complete Lattice Homomorphisms

Informal description

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

CompleteLatticeHom.comp_id theorem

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

Full source

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

Right Identity Law for Complete Lattice Homomorphism Composition

Informal description

For any complete lattice homomorphism $f \colon \alpha \to \beta$, the composition of $f$ with the identity homomorphism on $\alpha$ equals $f$. In other words, $f \circ \text{id}_\alpha = f$.

CompleteLatticeHom.id_comp theorem

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

Full source

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

Left identity law for complete lattice homomorphisms

Informal description

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

CompleteLatticeHom.cancel_right theorem

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

Full source

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

Right Cancellation Property for Composition of Complete Lattice Homomorphisms

Informal description

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

CompleteLatticeHom.cancel_left theorem

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

Full source

@[simp]
theorem cancel_left {g : CompleteLatticeHom β γ} {f₁ f₂ : CompleteLatticeHom α β}
    (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 Complete Lattice Homomorphisms

Informal description

Let $g \colon \beta \to \gamma$ be an injective complete lattice homomorphism between complete lattices $\beta$ and $\gamma$, and let $f_1, f_2 \colon \alpha \to \beta$ be complete lattice homomorphisms from a complete 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$.

sSupHom.dual definition

: sSupHom α β ≃ sInfHom αᵒᵈ βᵒᵈ

Full source

/-- Reinterpret a `⨆`-homomorphism as an `⨅`-homomorphism between the dual orders. -/
@[simps]
protected def dual : sSupHomsSupHom α β ≃ sInfHom αᵒᵈ βᵒᵈ where
  toFun f := ⟨toDual ∘ f ∘ ofDual, f.map_sSup'⟩
  invFun f := ⟨ofDual ∘ f ∘ toDual, f.map_sInf'⟩
  left_inv _ := sSupHom.ext fun _ => rfl
  right_inv _ := sInfHom.ext fun _ => rfl

Duality between supremum and infimum preserving homomorphisms

Informal description

The equivalence between the type of supremum-preserving homomorphisms from $\alpha$ to $\beta$ and the type of infimum-preserving homomorphisms between their order duals $\alpha^\text{op}$ and $\beta^\text{op}$. Concretely, given a supremum-preserving homomorphism $f: \alpha \to \beta$, its dual is the infimum-preserving homomorphism $f^\text{op}: \alpha^\text{op} \to \beta^\text{op}$ defined by $f^\text{op}(x) = f(x)^\text{op}$, and vice versa. This correspondence is bijective and preserves composition of homomorphisms.

sSupHom.dual_id theorem

: sSupHom.dual (sSupHom.id α) = sInfHom.id _

Full source

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

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

Informal description

The dual of the identity supremum-preserving homomorphism on a complete lattice $\alpha$ is the identity infimum-preserving homomorphism on the order dual of $\alpha$. That is, $(id_\alpha)^\text{op} = id_{\alpha^\text{op}}$.

sSupHom.dual_comp theorem

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

Full source

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

Duality of Composition for Supremum-Preserving Homomorphisms

Informal description

For any two supremum-preserving homomorphisms $g \colon \beta \to \gamma$ and $f \colon \alpha \to \beta$, the dual of their composition is equal to the composition of their duals. That is, $(g \circ f)^\text{op} = g^\text{op} \circ f^\text{op}$, where $^\text{op}$ denotes the order dual homomorphism.

sSupHom.symm_dual_id theorem

: sSupHom.dual.symm (sInfHom.id _) = sSupHom.id α

Full source

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

Inverse Duality of Identity Infimum-Preserving Homomorphism Yields Identity Supremum-Preserving Homomorphism

Informal description

The inverse of the duality equivalence applied to the identity infimum-preserving homomorphism on the order dual of a complete lattice $\alpha$ is equal to the identity supremum-preserving homomorphism on $\alpha$. That is, $(id_{\alpha^\text{op}})^\vee = id_\alpha$, where $^\vee$ denotes the inverse of the duality equivalence.

sSupHom.symm_dual_comp theorem

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

Full source

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

Inverse Duality Preserves Composition of Infimum-Preserving Homomorphisms

Informal description

Let $\alpha, \beta, \gamma$ be types equipped with complete lattice structures, and let $\alpha^\text{op}, \beta^\text{op}, \gamma^\text{op}$ denote their order duals. For any infimum-preserving 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$ individually. In other words, $(g \circ f)^\vee = g^\vee \circ f^\vee$, where $^\vee$ denotes the inverse of the duality equivalence between infimum-preserving and supremum-preserving homomorphisms.

sInfHom.dual definition

: sInfHom α β ≃ sSupHom αᵒᵈ βᵒᵈ

Full source

/-- Reinterpret an `⨅`-homomorphism as a `⨆`-homomorphism between the dual orders. -/
@[simps]
protected def dual : sInfHomsInfHom α β ≃ sSupHom αᵒᵈ βᵒᵈ where
  toFun f :=
    { toFun := toDualtoDual ∘ f ∘ ofDual
      map_sSup' := fun _ => congr_arg toDual (map_sInf f _) }
  invFun f :=
    { toFun := ofDualofDual ∘ f ∘ toDual
      map_sInf' := fun _ => congr_arg ofDual (map_sSup f _) }
  left_inv _ := sInfHom.ext fun _ => rfl
  right_inv _ := sSupHom.ext fun _ => rfl

Duality between infimum-preserving and supremum-preserving homomorphisms

Informal description

The equivalence between the type of infimum-preserving homomorphisms from $\alpha$ to $\beta$ and the type of supremum-preserving homomorphisms from the order dual of $\alpha$ to the order dual of $\beta$. Specifically, given an infimum-preserving homomorphism $f : \alpha \to \beta$, the corresponding supremum-preserving homomorphism is obtained by composing $f$ with the order duality maps, and vice versa.

sInfHom.dual_id theorem

: sInfHom.dual (sInfHom.id α) = sSupHom.id _

Full source

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

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

Informal description

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

sInfHom.dual_comp theorem

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

Full source

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

Duality of Composition of Infimum-Preserving Homomorphisms: $\text{dual}(g \circ f) = \text{dual}(g) \circ \text{dual}(f)$

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be complete lattices, and let $f \colon \alpha \to \beta$ and $g \colon \beta \to \gamma$ be infimum-preserving homomorphisms. Then, the dual of the composition $g \circ f$ is equal to the composition of the duals of $g$ and $f$, i.e., \[ \text{dual}(g \circ f) = \text{dual}(g) \circ \text{dual}(f), \] where $\text{dual}(g \circ f)$ is a supremum-preserving homomorphism between the order duals of $\alpha$ and $\gamma$, and $\text{dual}(g) \circ \text{dual}(f)$ is the composition of the supremum-preserving homomorphisms between the order duals of $\beta$ and $\gamma$, and $\alpha$ and $\beta$, respectively.

sInfHom.symm_dual_id theorem

: sInfHom.dual.symm (sSupHom.id _) = sInfHom.id α

Full source

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

Inverse Duality of Identity Homomorphism: $\text{sInfHom.dual.symm}(\text{sSupHom.id}_{\alpha^\text{op}}) = \text{sInfHom.id}_\alpha$

Informal description

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

sInfHom.symm_dual_comp theorem

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

Full source

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

Inverse Duality Preserves Composition of Supremum-Preserving Homomorphisms

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be types equipped with complete lattice structures, and let $f : \alpha^\text{op} \to \beta^\text{op}$ and $g : \beta^\text{op} \to \gamma^\text{op}$ be supremum-preserving homomorphisms between their order duals. Then, 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. In other words, the following equality holds: \[ \text{sInfHom.dual.symm}(g \circ f) = (\text{sInfHom.dual.symm } g) \circ (\text{sInfHom.dual.symm } f). \]

CompleteLatticeHom.dual definition

: CompleteLatticeHom α β ≃ CompleteLatticeHom αᵒᵈ βᵒᵈ

Full source

/-- Reinterpret a complete lattice homomorphism as a complete lattice homomorphism between the dual
lattices. -/
@[simps!]
protected def dual : CompleteLatticeHomCompleteLatticeHom α β ≃ CompleteLatticeHom αᵒᵈ βᵒᵈ where
  toFun f := ⟨sSupHom.dual f.tosSupHom, fun s ↦ f.map_sInf' s⟩
  invFun f := ⟨sSupHom.dual f.tosSupHom, fun s ↦ f.map_sInf' s⟩
  left_inv _ := ext fun _ => rfl
  right_inv _ := ext fun _ => rfl

Duality of complete lattice homomorphisms

Informal description

The equivalence between the type of complete lattice homomorphisms from $\alpha$ to $\beta$ and the type of complete lattice homomorphisms between their order duals $\alpha^\text{op}$ and $\beta^\text{op}$. Concretely, given a complete lattice homomorphism $f: \alpha \to \beta$, its dual is the complete lattice homomorphism $f^\text{op}: \alpha^\text{op} \to \beta^\text{op}$ defined by $f^\text{op}(x) = f(x)^\text{op}$, and vice versa. This correspondence is bijective and preserves composition of homomorphisms.

CompleteLatticeHom.dual_id theorem

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

Full source

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

Dual of Identity Complete Lattice Homomorphism is Identity on Order Dual

Informal description

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

CompleteLatticeHom.dual_comp theorem

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

Full source

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

Duality of Composition of Complete Lattice Homomorphisms: $(g \circ f)^\text{op} = g^\text{op} \circ f^\text{op}$

Informal description

For any complete lattice homomorphisms $f \colon \alpha \to \beta$ and $g \colon \beta \to \gamma$, the dual of their composition equals the composition of their duals. That is, $$(g \circ f)^\text{op} = g^\text{op} \circ f^\text{op},$$ where $(-)^\text{op}$ denotes the dual homomorphism between the order dual lattices.

CompleteLatticeHom.symm_dual_id theorem

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

Full source

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

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

Informal description

The inverse of the duality equivalence applied to the identity complete lattice homomorphism on the order dual lattice $\alpha^\text{op}$ is equal to the identity complete lattice homomorphism on $\alpha$.

CompleteLatticeHom.symm_dual_comp theorem

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

Full source

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

Inverse Duality of Composition of Complete Lattice Homomorphisms: $(g \circ f)^\text{op}^{-1} = g^\text{op}^{-1} \circ f^\text{op}^{-1}$

Informal description

For any complete 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, $$(g \circ f)^\text{op}^{-1} = g^\text{op}^{-1} \circ f^\text{op}^{-1},$$ where $(-)^\text{op}$ denotes the dual homomorphism between the order dual lattices and $(-)^{-1}$ denotes the inverse equivalence.

CompleteLatticeHom.setPreimage definition

(f : α → β) : CompleteLatticeHom (Set β) (Set α)

Full source

/-- `Set.preimage` as a complete lattice homomorphism.

See also `sSupHom.setImage`. -/
def setPreimage (f : α → β) : CompleteLatticeHom (Set β) (Set α) where
  toFun := preimage f
  map_sSup' s := preimage_sUnion.trans <| by simp only [Set.sSup_eq_sUnion, Set.sUnion_image]
  map_sInf' s := preimage_sInter.trans <| by simp only [Set.sInf_eq_sInter, Set.sInter_image]

Preimage as a complete lattice homomorphism

Informal description

For any function $ f : \alpha \to \beta $, the preimage function $ \text{preimage}\, f : \text{Set}\, \beta \to \text{Set}\, \alpha $ is a complete lattice homomorphism. Specifically, it preserves arbitrary suprema and infima, satisfying: - $ (\text{preimage}\, f)(\bigcup S) = \bigcup_{s \in S} (\text{preimage}\, f)(s) $ for any family of sets $ S \subseteq \text{Set}\, \beta $ - $ (\text{preimage}\, f)(\bigcap S) = \bigcap_{s \in S} (\text{preimage}\, f)(s) $ for any family of sets $ S \subseteq \text{Set}\, \beta $

CompleteLatticeHom.coe_setPreimage theorem

(f : α → β) : ⇑(setPreimage f) = preimage f

Full source

@[simp]
theorem coe_setPreimage (f : α → β) : ⇑(setPreimage f) = preimage f :=
  rfl

Preimage Function as Underlying Map of Complete Lattice Homomorphism

Informal description

For any function $f : \alpha \to \beta$, the underlying function of the complete lattice homomorphism `setPreimage f` is equal to the preimage function $\text{preimage}\, f : \text{Set}\, \beta \to \text{Set}\, \alpha$.

CompleteLatticeHom.setPreimage_apply theorem

(f : α → β) (s : Set β) : setPreimage f s = s.preimage f

Full source

@[simp]
theorem setPreimage_apply (f : α → β) (s : Set β) : setPreimage f s = s.preimage f :=
  rfl

Preimage Application as Complete Lattice Homomorphism

Informal description

For any function $f : \alpha \to \beta$ and any subset $s \subseteq \beta$, the application of the complete lattice homomorphism `setPreimage f` to $s$ is equal to the preimage of $s$ under $f$, i.e., $f^{-1}(s) = \{x \in \alpha \mid f(x) \in s\}$.

CompleteLatticeHom.setPreimage_id theorem

: setPreimage (id : α → α) = CompleteLatticeHom.id _

Full source

@[simp]
theorem setPreimage_id : setPreimage (id : α → α) = CompleteLatticeHom.id _ :=
  rfl

Preimage of Identity Function as Identity Homomorphism

Informal description

For any type $\alpha$, the complete lattice homomorphism induced by the preimage of the identity function $\text{id} : \alpha \to \alpha$ is equal to the identity complete lattice homomorphism on $\text{Set}\, \alpha$.

CompleteLatticeHom.setPreimage_comp theorem

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

Full source

theorem setPreimage_comp (g : β → γ) (f : α → β) :
    setPreimage (g ∘ f) = (setPreimage f).comp (setPreimage g) :=
  rfl

Composition Law for Preimage Complete Lattice Homomorphisms

Informal description

For any functions $g \colon \beta \to \gamma$ and $f \colon \alpha \to \beta$, the complete lattice homomorphism induced by the preimage of the composition $g \circ f$ is equal to the composition of the complete lattice homomorphisms induced by the preimages of $f$ and $g$ respectively. In symbols: $$ \text{preimage}\, (g \circ f) = (\text{preimage}\, f) \circ (\text{preimage}\, g). $$

Set.image_sSup theorem

{f : α → β} (s : Set (Set α)) : f '' sSup s = sSup (image f '' s)

Full source

theorem Set.image_sSup {f : α → β} (s : Set (Set α)) : f '' sSup s = sSup (imageimage f '' s) :=
  Set.image_sUnion

Image of Supremum Equals Supremum of Images

Informal description

For any function $f \colon \alpha \to \beta$ and any set $s$ of subsets of $\alpha$, the image of the supremum of $s$ under $f$ is equal to the supremum of the images of the sets in $s$ under $f$. In symbols: $$ f \left( \bigcup_{A \in s} A \right) = \bigcup_{A \in s} f(A). $$

sSupHom.setImage definition

(f : α → β) : sSupHom (Set α) (Set β)

Full source

/-- Using `Set.image`, a function between types yields a `sSupHom` between their lattices of
subsets.

See also `CompleteLatticeHom.setPreimage`. -/
@[simps]
def sSupHom.setImage (f : α → β) : sSupHom (Set α) (Set β) where
  toFun := image f
  map_sSup' := Set.image_sSup

Image function as a supremum-preserving homomorphism

Informal description

Given a function $f \colon \alpha \to \beta$, the function `sSupHom.setImage` maps a subset $S \subseteq \alpha$ to its image $f(S) \subseteq \beta$, and this operation preserves arbitrary suprema (unions). Specifically, for any collection of subsets $\{S_i\}_{i \in I}$ of $\alpha$, we have: $$ f\left( \bigcup_{i \in I} S_i \right) = \bigcup_{i \in I} f(S_i). $$

Equiv.toOrderIsoSet definition

(e : α ≃ β) : Set α ≃o Set β

Full source

/-- An equivalence of types yields an order isomorphism between their lattices of subsets. -/
@[simps]
def Equiv.toOrderIsoSet (e : α ≃ β) : SetSet α ≃o Set β where
  toFun s := e '' s
  invFun s := e.symm '' s
  left_inv s := by simp only [← image_comp, Equiv.symm_comp_self, id, image_id']
  right_inv s := by simp only [← image_comp, Equiv.self_comp_symm, id, image_id']
  map_rel_iff' :=
    ⟨fun h => by simpa using @monotone_image _ _ e.symm _ _ h, fun h => monotone_image h⟩

Order isomorphism between power sets induced by a bijection

Informal description

Given a bijection $e \colon \alpha \simeq \beta$, the function `Equiv.toOrderIsoSet` constructs an order isomorphism between the power sets $\mathcal{P}(\alpha)$ and $\mathcal{P}(\beta)$. Specifically, it maps a subset $s \subseteq \alpha$ to its image $e(s) \subseteq \beta$, and the inverse maps a subset $t \subseteq \beta$ to its preimage $e^{-1}(t) \subseteq \alpha$. This isomorphism preserves the subset ordering in both directions, meaning $s_1 \subseteq s_2$ if and only if $e(s_1) \subseteq e(s_2)$ for any subsets $s_1, s_2 \subseteq \alpha$.

supsSupHom definition

: sSupHom (α × α) α

Full source

/-- The map `(a, b) ↦ a ⊔ b` as a `sSupHom`. -/
def supsSupHom : sSupHom (α × α) α where
  toFun x := x.1 ⊔ x.2
  map_sSup' s := by simp_rw [Prod.fst_sSup, Prod.snd_sSup, sSup_image, iSup_sup_eq]

Supremum homomorphism of pairs

Informal description

The function that maps a pair $(a, b)$ to their supremum $a \sqcup b$, viewed as a supremum-preserving homomorphism. Specifically, this is a bundled function between the product lattice $\alpha \times \alpha$ and $\alpha$ that preserves arbitrary suprema.

infsInfHom definition

: sInfHom (α × α) α

Full source

/-- The map `(a, b) ↦ a ⊓ b` as an `sInfHom`. -/
def infsInfHom : sInfHom (α × α) α where
  toFun x := x.1 ⊓ x.2
  map_sInf' s := by simp_rw [Prod.fst_sInf, Prod.snd_sInf, sInf_image, iInf_inf_eq]

Infimum homomorphism of pairs

Informal description

The function that maps a pair $(a, b)$ to their infimum $a \sqcap b$, viewed as an infimum-preserving homomorphism. Specifically, this is a bundled function between the product lattice $\alpha \times \alpha$ and $\alpha$ that preserves arbitrary infima.

supsSupHom_apply theorem

: supsSupHom x = x.1 ⊔ x.2

Full source

@[simp, norm_cast]
theorem supsSupHom_apply : supsSupHom x = x.1 ⊔ x.2 :=
  rfl

Application of Supremum Homomorphism to Pairs: $f(a, b) = a \sqcup b$

Informal description

For any pair $x = (a, b)$ in the product lattice $\alpha \times \alpha$, the application of the supremum-preserving homomorphism `supsSupHom` to $x$ yields the supremum $a \sqcup b$ in $\alpha$.

infsInfHom_apply theorem

: infsInfHom x = x.1 ⊓ x.2

Full source

@[simp, norm_cast]
theorem infsInfHom_apply : infsInfHom x = x.1 ⊓ x.2 :=
  rfl

Application of Infimum Homomorphism to Pairs: $f(a, b) = a \sqcap b$

Informal description

For any element $x = (a, b)$ in the product lattice $\alpha \times \alpha$, the infimum-preserving homomorphism `infsInfHom` maps $x$ to the infimum $a \sqcap b$ in $\alpha$.

Mathlib.Order.Hom.CompleteLattice

Types of morphisms

Typeclasses

Concrete homs

TODO