# Heyting algebra morphisms #

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

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

## Typeclasses #

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.

• toFun : αβ
• map_sup' : ∀ (a b : α), self.toFun (a b) = self.toFun a self.toFun b
• map_inf' : ∀ (a b : α), self.toFun (a b) = self.toFun a self.toFun b
• map_bot' : self.toFun =

The proposition that a Heyting homomorphism preserves the bottom element.

• map_himp' : ∀ (a b : α), self.toFun (a b) = self.toFun a self.toFun b

The proposition that a Heyting homomorphism preserves the Heyting implication.

Instances For
theorem HeytingHom.map_bot' {α : Type u_6} {β : Type u_7} [] [] (self : ) :
self.toFun =

The proposition that a Heyting homomorphism preserves the bottom element.

theorem HeytingHom.map_himp' {α : Type u_6} {β : Type u_7} [] [] (self : ) (a : α) (b : α) :
self.toFun (a b) = self.toFun a self.toFun b

The proposition that a Heyting homomorphism preserves the Heyting implication.

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.

• toFun : αβ
• map_sup' : ∀ (a b : α), self.toFun (a b) = self.toFun a self.toFun b
• map_inf' : ∀ (a b : α), self.toFun (a b) = self.toFun a self.toFun b
• map_top' : self.toFun =

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

• map_sdiff' : ∀ (a b : α), self.toFun (a \ b) = self.toFun a \ self.toFun b

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

Instances For
theorem CoheytingHom.map_top' {α : Type u_6} {β : Type u_7} [] [] (self : ) :
self.toFun =

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

theorem CoheytingHom.map_sdiff' {α : Type u_6} {β : Type u_7} [] [] (self : ) (a : α) (b : α) :
self.toFun (a \ b) = self.toFun a \ self.toFun b

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

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.

• toFun : αβ
• map_sup' : ∀ (a b : α), self.toFun (a b) = self.toFun a self.toFun b
• map_inf' : ∀ (a b : α), self.toFun (a b) = self.toFun a self.toFun b
• map_himp' : ∀ (a b : α), self.toFun (a b) = self.toFun a self.toFun b

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

• map_sdiff' : ∀ (a b : α), self.toFun (a \ b) = self.toFun a \ self.toFun b

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

Instances For
theorem BiheytingHom.map_himp' {α : Type u_6} {β : Type u_7} [] [] (self : ) (a : α) (b : α) :
self.toFun (a b) = self.toFun a self.toFun b

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

theorem BiheytingHom.map_sdiff' {α : Type u_6} {β : Type u_7} [] [] (self : ) (a : α) (b : α) :
self.toFun (a \ b) = self.toFun a \ self.toFun b

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

class HeytingHomClass (F : Type u_6) (α : Type u_7) (β : Type u_8) [] [] [FunLike F α β] extends :

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

You should extend this class when you extend HeytingHom.

• 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.

Instances
theorem HeytingHomClass.map_bot {F : Type u_6} {α : Type u_7} {β : Type u_8} [] [] [FunLike F α β] [self : ] (f : F) :

The proposition that a Heyting homomorphism preserves the bottom element.

@[simp]
theorem HeytingHomClass.map_himp {F : Type u_6} {α : Type u_7} {β : Type u_8} [] [] [FunLike F α β] [self : ] (f : F) (a : α) (b : α) :
f (a b) = f a f b

The proposition that a Heyting homomorphism preserves the Heyting implication.

class CoheytingHomClass (F : Type u_6) (α : Type u_7) (β : Type u_8) [] [] [FunLike F α β] extends :

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

You should extend this class when you extend CoheytingHom.

• 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.

Instances
theorem CoheytingHomClass.map_top {F : Type u_6} {α : Type u_7} {β : Type u_8} [] [] [FunLike F α β] [self : ] (f : F) :

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

@[simp]
theorem CoheytingHomClass.map_sdiff {F : Type u_6} {α : Type u_7} {β : Type u_8} [] [] [FunLike F α β] [self : ] (f : F) (a : α) (b : α) :
f (a \ b) = f a \ f b

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

class BiheytingHomClass (F : Type u_6) (α : Type u_7) (β : Type u_8) [] [] [FunLike F α β] extends :

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

You should extend this class when you extend BiheytingHom.

• 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.

Instances
theorem BiheytingHomClass.map_himp {F : Type u_6} {α : Type u_7} {β : Type u_8} [] [] [FunLike F α β] [self : ] (f : F) (a : α) (b : α) :
f (a b) = f a f b

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

theorem BiheytingHomClass.map_sdiff {F : Type u_6} {α : Type u_7} {β : Type u_8} [] [] [FunLike F α β] [self : ] (f : F) (a : α) (b : α) :
f (a \ b) = f a \ f b

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

@[instance 100]
instance HeytingHomClass.toBoundedLatticeHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [] :
∀ {x : } [inst : ],
Equations
• =
@[instance 100]
instance CoheytingHomClass.toBoundedLatticeHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [] :
∀ {x : } [inst : ],
Equations
• =
@[instance 100]
instance BiheytingHomClass.toHeytingHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [] :
∀ {x : } [inst : ],
Equations
• =
@[instance 100]
instance BiheytingHomClass.toCoheytingHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [] :
∀ {x : } [inst : ],
Equations
• =
@[instance 100]
instance OrderIsoClass.toHeytingHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [] :
∀ {x : } [inst : ],
Equations
• =
@[instance 100]
instance OrderIsoClass.toCoheytingHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [] :
∀ {x : } [inst : ],
Equations
• =
@[instance 100]
instance OrderIsoClass.toBiheytingHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [] :
∀ {x : } [inst : ],
Equations
• =
theorem BoundedLatticeHomClass.toBiheytingHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [] [] [] :

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

@[simp]
theorem map_compl {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [] [] [] (f : F) (a : α) :
f a = (f a)
@[simp]
theorem map_bihimp {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [] [] [] (f : F) (a : α) (b : α) :
f (bihimp a b) = bihimp (f a) (f b)
@[simp]
theorem map_hnot {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [] [] [] (f : F) (a : α) :
f (a) = f a
@[simp]
theorem map_symmDiff {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [] [] [] (f : F) (a : α) (b : α) :
f (symmDiff a b) = symmDiff (f a) (f b)
instance instCoeTCHeytingHomOfHeytingHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [] [] [] :
CoeTC F ()
Equations
• instCoeTCHeytingHomOfHeytingHomClass = { coe := fun (f : F) => { toFun := f, map_sup' := , map_inf' := , map_bot' := , map_himp' := } }
instance instCoeTCCoheytingHomOfCoheytingHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [] [] [] :
CoeTC F ()
Equations
• instCoeTCCoheytingHomOfCoheytingHomClass = { coe := fun (f : F) => { toFun := f, map_sup' := , map_inf' := , map_top' := , map_sdiff' := } }
instance instCoeTCBiheytingHomOfBiheytingHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [] [] [] :
CoeTC F ()
Equations
• instCoeTCBiheytingHomOfBiheytingHomClass = { coe := fun (f : F) => { toFun := f, map_sup' := , map_inf' := , map_himp' := , map_sdiff' := } }
instance HeytingHom.instFunLike {α : Type u_2} {β : Type u_3} [] [] :
FunLike () α β
Equations
• HeytingHom.instFunLike = { coe := fun (f : ) => f.toFun, coe_injective' := }
instance HeytingHom.instHeytingHomClass {α : Type u_2} {β : Type u_3} [] [] :
Equations
• =
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.

Equations
• f.copy f' h = { toFun := f', map_sup' := , map_inf' := , map_bot' := , map_himp' := }
Instances For
@[simp]
theorem HeytingHom.coe_copy {α : Type u_2} {β : Type u_3} [] [] (f : ) (f' : αβ) (h : f' = f) :
(f.copy f' h) = f'
theorem HeytingHom.copy_eq {α : Type u_2} {β : Type u_3} [] [] (f : ) (f' : αβ) (h : f' = f) :
f.copy f' h = f
def HeytingHom.id (α : Type u_2) [] :

id as a HeytingHom.

Equations
• = let __src := ; { toLatticeHom := , map_bot' := , map_himp' := }
Instances For
@[simp]
theorem HeytingHom.coe_id (α : Type u_2) [] :
() = id
@[simp]
theorem HeytingHom.id_apply {α : Type u_2} [] (a : α) :
() a = a
instance HeytingHom.instInhabited {α : Type u_2} [] :
Equations
• HeytingHom.instInhabited = { default := }
instance HeytingHom.instPartialOrder {α : Type u_2} {β : Type u_3} [] [] :
Equations
def HeytingHom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] (f : ) (g : ) :

Composition of HeytingHoms as a HeytingHom.

Equations
• f.comp g = let __src := f.comp g.toLatticeHom; { toFun := f g, map_sup' := , map_inf' := , map_bot' := , map_himp' := }
Instances For
@[simp]
theorem HeytingHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] (f : ) (g : ) :
(f.comp g) = f g
@[simp]
theorem HeytingHom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] (f : ) (g : ) (a : α) :
(f.comp g) a = f (g a)
@[simp]
theorem HeytingHom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [] [] [] [] (f : ) (g : ) (h : ) :
(f.comp g).comp h = f.comp (g.comp h)
@[simp]
theorem HeytingHom.comp_id {α : Type u_2} {β : Type u_3} [] [] (f : ) :
f.comp () = f
@[simp]
theorem HeytingHom.id_comp {α : Type u_2} {β : Type u_3} [] [] (f : ) :
().comp f = f
@[simp]
theorem HeytingHom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] {f : } {g₁ : } {g₂ : } (hf : ) :
g₁.comp f = g₂.comp f g₁ = g₂
@[simp]
theorem HeytingHom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] {f₁ : } {f₂ : } {g : } (hg : ) :
g.comp f₁ = g.comp f₂ f₁ = f₂
instance CoheytingHom.instFunLike {α : Type u_2} {β : Type u_3} [] [] :
FunLike () α β
Equations
• CoheytingHom.instFunLike = { coe := fun (f : ) => f.toFun, coe_injective' := }
instance CoheytingHom.instCoheytingHomClass {α : Type u_2} {β : Type u_3} [] [] :
Equations
• =
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.

Equations
• f.copy f' h = { toFun := f', map_sup' := , map_inf' := , map_top' := , map_sdiff' := }
Instances For
@[simp]
theorem CoheytingHom.coe_copy {α : Type u_2} {β : Type u_3} [] [] (f : ) (f' : αβ) (h : f' = f) :
(f.copy f' h) = f'
theorem CoheytingHom.copy_eq {α : Type u_2} {β : Type u_3} [] [] (f : ) (f' : αβ) (h : f' = f) :
f.copy f' h = f
def CoheytingHom.id (α : Type u_2) [] :

id as a CoheytingHom.

Equations
• = let __src := ; { toLatticeHom := , map_top' := , map_sdiff' := }
Instances For
@[simp]
theorem CoheytingHom.coe_id (α : Type u_2) [] :
() = id
@[simp]
theorem CoheytingHom.id_apply {α : Type u_2} [] (a : α) :
() a = a
instance CoheytingHom.instInhabited {α : Type u_2} [] :
Equations
• CoheytingHom.instInhabited = { default := }
instance CoheytingHom.instPartialOrder {α : Type u_2} {β : Type u_3} [] [] :
Equations
def CoheytingHom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] (f : ) (g : ) :

Composition of CoheytingHoms as a CoheytingHom.

Equations
• f.comp g = let __src := f.comp g.toLatticeHom; { toFun := f g, map_sup' := , map_inf' := , map_top' := , map_sdiff' := }
Instances For
@[simp]
theorem CoheytingHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] (f : ) (g : ) :
(f.comp g) = f g
@[simp]
theorem CoheytingHom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] (f : ) (g : ) (a : α) :
(f.comp g) a = f (g a)
@[simp]
theorem CoheytingHom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [] [] [] [] (f : ) (g : ) (h : ) :
(f.comp g).comp h = f.comp (g.comp h)
@[simp]
theorem CoheytingHom.comp_id {α : Type u_2} {β : Type u_3} [] [] (f : ) :
f.comp () = f
@[simp]
theorem CoheytingHom.id_comp {α : Type u_2} {β : Type u_3} [] [] (f : ) :
().comp f = f
@[simp]
theorem CoheytingHom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] {f : } {g₁ : } {g₂ : } (hf : ) :
g₁.comp f = g₂.comp f g₁ = g₂
@[simp]
theorem CoheytingHom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] {f₁ : } {f₂ : } {g : } (hg : ) :
g.comp f₁ = g.comp f₂ f₁ = f₂
instance BiheytingHom.instFunLike {α : Type u_2} {β : Type u_3} [] [] :
FunLike () α β
Equations
• BiheytingHom.instFunLike = { coe := fun (f : ) => f.toFun, coe_injective' := }
instance BiheytingHom.instBiheytingHomClass {α : Type u_2} {β : Type u_3} [] [] :
Equations
• =
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.

Equations
• f.copy f' h = { toFun := f', map_sup' := , map_inf' := , map_himp' := , map_sdiff' := }
Instances For
@[simp]
theorem BiheytingHom.coe_copy {α : Type u_2} {β : Type u_3} [] [] (f : ) (f' : αβ) (h : f' = f) :
(f.copy f' h) = f'
theorem BiheytingHom.copy_eq {α : Type u_2} {β : Type u_3} [] [] (f : ) (f' : αβ) (h : f' = f) :
f.copy f' h = f
def BiheytingHom.id (α : Type u_2) [] :

id as a BiheytingHom.

Equations
• = let __src := ; let __src := ; { toLatticeHom := , map_himp' := , map_sdiff' := }
Instances For
@[simp]
theorem BiheytingHom.coe_id (α : Type u_2) [] :
() = id
@[simp]
theorem BiheytingHom.id_apply {α : Type u_2} [] (a : α) :
() a = a
instance BiheytingHom.instInhabited {α : Type u_2} [] :
Equations
• BiheytingHom.instInhabited = { default := }
instance BiheytingHom.instPartialOrder {α : Type u_2} {β : Type u_3} [] [] :
Equations
def BiheytingHom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] (f : ) (g : ) :

Composition of BiheytingHoms as a BiheytingHom.

Equations
• f.comp g = let __src := f.comp g.toLatticeHom; { toFun := f g, map_sup' := , map_inf' := , map_himp' := , map_sdiff' := }
Instances For
@[simp]
theorem BiheytingHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] (f : ) (g : ) :
(f.comp g) = f g
@[simp]
theorem BiheytingHom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] (f : ) (g : ) (a : α) :
(f.comp g) a = f (g a)
@[simp]
theorem BiheytingHom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [] [] [] [] (f : ) (g : ) (h : ) :
(f.comp g).comp h = f.comp (g.comp h)
@[simp]
theorem BiheytingHom.comp_id {α : Type u_2} {β : Type u_3} [] [] (f : ) :
f.comp () = f
@[simp]
theorem BiheytingHom.id_comp {α : Type u_2} {β : Type u_3} [] [] (f : ) :
().comp f = f
@[simp]
theorem BiheytingHom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] {f : } {g₁ : } {g₂ : } (hf : ) :
g₁.comp f = g₂.comp f g₁ = g₂
@[simp]
theorem BiheytingHom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] {f₁ : } {f₂ : } {g : } (hg : ) :
g.comp f₁ = g.comp f₂ f₁ = f₂