# Documentation

Mathlib.Order.Heyting.Hom

# Heyting algebra morphisms #

A Heyting homomorphism between two Heyting algebras is a bounded lattice homomorphism that preserves Heyting implication.

We use the FunLike design, so each type of morphisms has a companion typeclass which is meant to be satisfied by itself and all stricter types.

## Types of morphisms #

• HeytingHom: Heyting homomorphisms.
• CoheytingHom: Co-Heyting homomorphisms.
• BiheytingHom: Bi-Heyting homomorphisms.

## Typeclasses #

• HeytingHomClass
• CoheytingHomClass
• BiheytingHomClass
structure HeytingHom (α : Type u_6) (β : Type u_7) [] [] extends :
Type (max u_6 u_7)

The type of Heyting homomorphisms from α to β. Bounded lattice homomorphisms that preserve Heyting implication.

Instances For
structure CoheytingHom (α : Type u_6) (β : Type u_7) [] [] extends :
Type (max u_6 u_7)

The type of co-Heyting homomorphisms from α to β. Bounded lattice homomorphisms that preserve difference.

Instances For
structure BiheytingHom (α : Type u_6) (β : Type u_7) [] [] extends :
Type (max u_6 u_7)

The type of bi-Heyting homomorphisms from α to β. Bounded lattice homomorphisms that preserve Heyting implication and difference.

Instances For
class HeytingHomClass (F : Type u_6) (α : outParam (Type u_7)) (β : outParam (Type u_8)) [] [] extends :
Type (max (max u_6 u_7) u_8)
• coe : Fαβ
• coe_injective' : Function.Injective FunLike.coe
• map_sup : ∀ (f : F) (a b : α), f (a b) = f a f b
• map_inf : ∀ (f : F) (a b : α), f (a b) = f a f b
• map_bot : ∀ (f : F), f =

The proposition that a Heyting homomorphism preserves the bottom element.

• map_himp : ∀ (f : F) (a b : α), f (a b) = f a f b

The proposition that a Heyting homomorphism preserves the Heyting implication.

HeytingHomClass F α β states that F is a type of Heyting homomorphisms.

You should extend this class when you extend HeytingHom.

Instances
class CoheytingHomClass (F : Type u_6) (α : outParam (Type u_7)) (β : outParam (Type u_8)) [] [] extends :
Type (max (max u_6 u_7) u_8)
• coe : Fαβ
• coe_injective' : Function.Injective FunLike.coe
• map_sup : ∀ (f : F) (a b : α), f (a b) = f a f b
• map_inf : ∀ (f : F) (a b : α), f (a b) = f a f b
• map_top : ∀ (f : F), f =

The proposition that a co-Heyting homomorphism preserves the top element.

• map_sdiff : ∀ (f : F) (a b : α), f (a \ b) = f a \ f b

The proposition that a co-Heyting homomorphism preserves the difference operation.

CoheytingHomClass F α β states that F is a type of co-Heyting homomorphisms.

You should extend this class when you extend CoheytingHom.

Instances
class BiheytingHomClass (F : Type u_6) (α : outParam (Type u_7)) (β : outParam (Type u_8)) [] [] extends :
Type (max (max u_6 u_7) u_8)
• coe : Fαβ
• coe_injective' : Function.Injective FunLike.coe
• map_sup : ∀ (f : F) (a b : α), f (a b) = f a f b
• map_inf : ∀ (f : F) (a b : α), f (a b) = f a f b
• map_himp : ∀ (f : F) (a b : α), f (a b) = f a f b

The proposition that a bi-Heyting homomorphism preserves the Heyting implication.

• map_sdiff : ∀ (f : F) (a b : α), f (a \ b) = f a \ f b

The proposition that a bi-Heyting homomorphism preserves the difference operation.

BiheytingHomClass F α β states that F is a type of bi-Heyting homomorphisms.

You should extend this class when you extend BiheytingHom.

Instances
instance HeytingHomClass.toBoundedLatticeHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [] :
{x : } → [inst : ] →
instance CoheytingHomClass.toBoundedLatticeHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [] :
{x : } → [inst : ] →
instance BiheytingHomClass.toHeytingHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [] :
{x : } → [inst : ] →
instance BiheytingHomClass.toCoheytingHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [] :
{x : } → [inst : ] →
instance OrderIsoClass.toHeytingHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [] :
{x : } → [inst : ] →
instance OrderIsoClass.toCoheytingHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [] :
{x : } → [inst : ] →
instance OrderIsoClass.toBiheytingHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [] :
{x : } → [inst : ] →
@[reducible]
def BoundedLatticeHomClass.toBiheytingHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [] :

This can't be an instance because of typeclass loops.

Instances For
@[simp]
theorem map_compl {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [] (f : F) (a : α) :
f a = (f a)
@[simp]
theorem map_bihimp {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [] (f : F) (a : α) (b : α) :
f (a b) = f a f b
@[simp]
theorem map_hnot {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [] (f : F) (a : α) :
f (a) = f a
@[simp]
theorem map_symmDiff {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [] (f : F) (a : α) (b : α) :
f (a b) = f a f b
instance instCoeTCHeytingHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [] :
CoeTC F ()
instance instCoeTCCoheytingHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [] :
CoeTC F ()
instance instCoeTCBiheytingHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [] :
CoeTC F ()
instance HeytingHom.instHeytingHomClass {α : Type u_2} {β : Type u_3} [] [] :
theorem HeytingHom.toFun_eq_coe {α : Type u_2} {β : Type u_3} [] [] {f : } :
f.toFun = f
@[simp]
theorem HeytingHom.toFun_eq_coe_aux {α : Type u_2} {β : Type u_3} [] [] {f : } :
f.toLatticeHom = f
theorem HeytingHom.ext {α : Type u_2} {β : Type u_3} [] [] {f : } {g : } (h : ∀ (a : α), f a = g a) :
f = g
def HeytingHom.copy {α : Type u_2} {β : Type u_3} [] [] (f : ) (f' : αβ) (h : f' = f) :

Copy of a HeytingHom with a new toFun equal to the old one. Useful to fix definitional equalities.

Instances For
@[simp]
theorem HeytingHom.coe_copy {α : Type u_2} {β : Type u_3} [] [] (f : ) (f' : αβ) (h : f' = f) :
↑(HeytingHom.copy f f' h) = f'
theorem HeytingHom.copy_eq {α : Type u_2} {β : Type u_3} [] [] (f : ) (f' : αβ) (h : f' = f) :
def HeytingHom.id (α : Type u_2) [] :

id as a HeytingHom.

Instances For
@[simp]
theorem HeytingHom.coe_id (α : Type u_2) [] :
↑() = id
@[simp]
theorem HeytingHom.id_apply {α : Type u_2} [] (a : α) :
↑() a = a
instance HeytingHom.instPartialOrderHeytingHom {α : Type u_2} {β : Type u_3} [] [] :
def HeytingHom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] (f : ) (g : ) :

Composition of HeytingHoms as a HeytingHom.

Instances For
@[simp]
theorem HeytingHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] (f : ) (g : ) :
↑() = f g
@[simp]
theorem HeytingHom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] (f : ) (g : ) (a : α) :
↑() a = f (g a)
@[simp]
theorem HeytingHom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [] [] [] [] (f : ) (g : ) (h : ) :
=
@[simp]
theorem HeytingHom.comp_id {α : Type u_2} {β : Type u_3} [] [] (f : ) :
= f
@[simp]
theorem HeytingHom.id_comp {α : Type u_2} {β : Type u_3} [] [] (f : ) :
= f
@[simp]
theorem HeytingHom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] {f : } {g₁ : } {g₂ : } (hf : ) :
= g₁ = g₂
@[simp]
theorem HeytingHom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] {f₁ : } {f₂ : } {g : } (hg : ) :
= f₁ = f₂
theorem CoheytingHom.toFun_eq_coe {α : Type u_2} {β : Type u_3} [] [] {f : } :
f.toFun = f
@[simp]
theorem CoheytingHom.toFun_eq_coe_aux {α : Type u_2} {β : Type u_3} [] [] {f : } :
f.toLatticeHom = f
theorem CoheytingHom.ext {α : Type u_2} {β : Type u_3} [] [] {f : } {g : } (h : ∀ (a : α), f a = g a) :
f = g
def CoheytingHom.copy {α : Type u_2} {β : Type u_3} [] [] (f : ) (f' : αβ) (h : f' = f) :

Copy of a CoheytingHom with a new toFun equal to the old one. Useful to fix definitional equalities.

Instances For
@[simp]
theorem CoheytingHom.coe_copy {α : Type u_2} {β : Type u_3} [] [] (f : ) (f' : αβ) (h : f' = f) :
↑() = f'
theorem CoheytingHom.copy_eq {α : Type u_2} {β : Type u_3} [] [] (f : ) (f' : αβ) (h : f' = f) :
= f
def CoheytingHom.id (α : Type u_2) [] :

id as a CoheytingHom.

Instances For
@[simp]
theorem CoheytingHom.coe_id (α : Type u_2) [] :
↑() = id
@[simp]
theorem CoheytingHom.id_apply {α : Type u_2} [] (a : α) :
↑() a = a
def CoheytingHom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] (f : ) (g : ) :

Composition of CoheytingHoms as a CoheytingHom.

Instances For
@[simp]
theorem CoheytingHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] (f : ) (g : ) :
↑() = f g
@[simp]
theorem CoheytingHom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] (f : ) (g : ) (a : α) :
↑() a = f (g a)
@[simp]
theorem CoheytingHom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [] [] [] [] (f : ) (g : ) (h : ) :
=
@[simp]
theorem CoheytingHom.comp_id {α : Type u_2} {β : Type u_3} [] [] (f : ) :
@[simp]
theorem CoheytingHom.id_comp {α : Type u_2} {β : Type u_3} [] [] (f : ) :
@[simp]
theorem CoheytingHom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] {f : } {g₁ : } {g₂ : } (hf : ) :
= g₁ = g₂
@[simp]
theorem CoheytingHom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] {f₁ : } {f₂ : } {g : } (hg : ) :
= f₁ = f₂
theorem BiheytingHom.toFun_eq_coe {α : Type u_2} {β : Type u_3} [] [] {f : } :
f.toFun = f
@[simp]
theorem BiheytingHom.toFun_eq_coe_aux {α : Type u_2} {β : Type u_3} [] [] {f : } :
f.toLatticeHom = f
theorem BiheytingHom.ext {α : Type u_2} {β : Type u_3} [] [] {f : } {g : } (h : ∀ (a : α), f a = g a) :
f = g
def BiheytingHom.copy {α : Type u_2} {β : Type u_3} [] [] (f : ) (f' : αβ) (h : f' = f) :

Copy of a BiheytingHom with a new toFun equal to the old one. Useful to fix definitional equalities.

Instances For
@[simp]
theorem BiheytingHom.coe_copy {α : Type u_2} {β : Type u_3} [] [] (f : ) (f' : αβ) (h : f' = f) :
↑() = f'
theorem BiheytingHom.copy_eq {α : Type u_2} {β : Type u_3} [] [] (f : ) (f' : αβ) (h : f' = f) :
= f
def BiheytingHom.id (α : Type u_2) [] :

id as a BiheytingHom.

Instances For
@[simp]
theorem BiheytingHom.coe_id (α : Type u_2) [] :
↑() = id
@[simp]
theorem BiheytingHom.id_apply {α : Type u_2} [] (a : α) :
↑() a = a
def BiheytingHom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] (f : ) (g : ) :

Composition of BiheytingHoms as a BiheytingHom.

Instances For
@[simp]
theorem BiheytingHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] (f : ) (g : ) :
↑() = f g
@[simp]
theorem BiheytingHom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] (f : ) (g : ) (a : α) :
↑() a = f (g a)
@[simp]
theorem BiheytingHom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [] [] [] [] (f : ) (g : ) (h : ) :
=
@[simp]
theorem BiheytingHom.comp_id {α : Type u_2} {β : Type u_3} [] [] (f : ) :
@[simp]
theorem BiheytingHom.id_comp {α : Type u_2} {β : Type u_3} [] [] (f : ) :
@[simp]
theorem BiheytingHom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] {f : } {g₁ : } {g₂ : } (hf : ) :
= g₁ = g₂
@[simp]
theorem BiheytingHom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] {f₁ : } {f₂ : } {g : } (hg : ) :
= f₁ = f₂