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.

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) [HeytingAlgebra α] [HeytingAlgebra β] extends LatticeHom α β : 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.

structure CoheytingHom (α : Type u_6) (β : Type u_7) [CoheytingAlgebra α] [CoheytingAlgebra β] extends LatticeHom α β : 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.

structure BiheytingHom (α : Type u_6) (β : Type u_7) [BiheytingAlgebra α] [BiheytingAlgebra β] extends LatticeHom α β : 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.

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

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.

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

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.

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

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.

This section passes in some instances implicitly. See note [implicit instance arguments]

@[instance 100]

instance HeytingHomClass.toBoundedLatticeHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [HeytingAlgebra α] {x✝ : HeytingAlgebra β} [HeytingHomClass F α β] : BoundedLatticeHomClass F α β

@[instance 100]

instance CoheytingHomClass.toBoundedLatticeHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [CoheytingAlgebra α] {x✝ : CoheytingAlgebra β} [CoheytingHomClass F α β] : BoundedLatticeHomClass F α β

@[instance 100]

instance BiheytingHomClass.toHeytingHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [BiheytingAlgebra α] {x✝ : BiheytingAlgebra β} [BiheytingHomClass F α β] : HeytingHomClass F α β

@[instance 100]

instance BiheytingHomClass.toCoheytingHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [BiheytingAlgebra α] {x✝ : BiheytingAlgebra β} [BiheytingHomClass F α β] : CoheytingHomClass F α β

@[instance 100]

instance OrderIsoClass.toHeytingHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [HeytingAlgebra α] {x✝ : HeytingAlgebra β} [OrderIsoClass F α β] : HeytingHomClass F α β

@[instance 100]

instance OrderIsoClass.toCoheytingHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [CoheytingAlgebra α] {x✝ : CoheytingAlgebra β} [OrderIsoClass F α β] : CoheytingHomClass F α β

@[instance 100]

instance OrderIsoClass.toBiheytingHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [BiheytingAlgebra α] {x✝ : BiheytingAlgebra β} [OrderIsoClass F α β] : BiheytingHomClass F α β

instance BoundedLatticeHomClass.toBiheytingHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [BooleanAlgebra α] [BooleanAlgebra β] [BoundedLatticeHomClass F α β] : BiheytingHomClass F α β

@[simp]

theorem map_compl {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [HeytingAlgebra α] [HeytingAlgebra β] [HeytingHomClass F α β] (f : F) (a : α) : f aᶜ = (f a)ᶜ

@[simp]

theorem map_bihimp {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [HeytingAlgebra α] [HeytingAlgebra β] [HeytingHomClass 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 α β] [CoheytingAlgebra α] [CoheytingAlgebra β] [CoheytingHomClass F α β] (f : F) (a : α) : f (￢a) = ￢f a

@[simp]

theorem map_symmDiff {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [CoheytingAlgebra α] [CoheytingAlgebra β] [CoheytingHomClass 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 α β] [HeytingAlgebra α] [HeytingAlgebra β] [HeytingHomClass F α β] : CoeTC F (HeytingHom α β)

instance instCoeTCCoheytingHomOfCoheytingHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [CoheytingAlgebra α] [CoheytingAlgebra β] [CoheytingHomClass F α β] : CoeTC F (CoheytingHom α β)

instance instCoeTCBiheytingHomOfBiheytingHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [BiheytingAlgebra α] [BiheytingAlgebra β] [BiheytingHomClass F α β] : CoeTC F (BiheytingHom α β)

instance HeytingHom.instFunLike {α : Type u_2} {β : Type u_3} [HeytingAlgebra α] [HeytingAlgebra β] : FunLike (HeytingHom α β) α β

instance HeytingHom.instHeytingHomClass {α : Type u_2} {β : Type u_3} [HeytingAlgebra α] [HeytingAlgebra β] : HeytingHomClass (HeytingHom α β) α β

theorem HeytingHom.toFun_eq_coe {α : Type u_2} {β : Type u_3} [HeytingAlgebra α] [HeytingAlgebra β] {f : HeytingHom α β} : f.toFun = ⇑f

@[simp]

theorem HeytingHom.toFun_eq_coe_aux {α : Type u_2} {β : Type u_3} [HeytingAlgebra α] [HeytingAlgebra β] {f : HeytingHom α β} : ⇑f.toLatticeHom = ⇑f

theorem HeytingHom.ext {α : Type u_2} {β : Type u_3} [HeytingAlgebra α] [HeytingAlgebra β] {f g : HeytingHom α β} (h : ∀ (a : α), f a = g a) : f = g

theorem HeytingHom.ext_iff {α : Type u_2} {β : Type u_3} [HeytingAlgebra α] [HeytingAlgebra β] {f g : HeytingHom α β} : f = g ↔ ∀ (a : α), f a = g a

def HeytingHom.copy {α : Type u_2} {β : Type u_3} [HeytingAlgebra α] [HeytingAlgebra β] (f : HeytingHom α β) (f' : α → β) (h : f' = ⇑f) : HeytingHom α β

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

@[simp]

theorem HeytingHom.coe_copy {α : Type u_2} {β : Type u_3} [HeytingAlgebra α] [HeytingAlgebra β] (f : HeytingHom α β) (f' : α → β) (h : f' = ⇑f) : ⇑(f.copy f' h) = f'

theorem HeytingHom.copy_eq {α : Type u_2} {β : Type u_3} [HeytingAlgebra α] [HeytingAlgebra β] (f : HeytingHom α β) (f' : α → β) (h : f' = ⇑f) : f.copy f' h = f

def HeytingHom.id (α : Type u_2) [HeytingAlgebra α] : HeytingHom α α

id as a HeytingHom.

@[simp]

theorem HeytingHom.coe_id (α : Type u_2) [HeytingAlgebra α] : ⇑(HeytingHom.id α) = id

@[simp]

theorem HeytingHom.id_apply {α : Type u_2} [HeytingAlgebra α] (a : α) : (HeytingHom.id α) a = a

instance HeytingHom.instInhabited {α : Type u_2} [HeytingAlgebra α] : Inhabited (HeytingHom α α)

instance HeytingHom.instPartialOrder {α : Type u_2} {β : Type u_3} [HeytingAlgebra α] [HeytingAlgebra β] : PartialOrder (HeytingHom α β)

def HeytingHom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [HeytingAlgebra α] [HeytingAlgebra β] [HeytingAlgebra γ] (f : HeytingHom β γ) (g : HeytingHom α β) : HeytingHom α γ

Composition of HeytingHoms as a HeytingHom.

@[simp]

theorem HeytingHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [HeytingAlgebra α] [HeytingAlgebra β] [HeytingAlgebra γ] (f : HeytingHom β γ) (g : HeytingHom α β) : ⇑(f.comp g) = ⇑f ∘ ⇑g

@[simp]

theorem HeytingHom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [HeytingAlgebra α] [HeytingAlgebra β] [HeytingAlgebra γ] (f : HeytingHom β γ) (g : HeytingHom α β) (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} [HeytingAlgebra α] [HeytingAlgebra β] [HeytingAlgebra γ] [HeytingAlgebra δ] (f : HeytingHom γ δ) (g : HeytingHom β γ) (h : HeytingHom α β) : (f.comp g).comp h = f.comp (g.comp h)

@[simp]

theorem HeytingHom.comp_id {α : Type u_2} {β : Type u_3} [HeytingAlgebra α] [HeytingAlgebra β] (f : HeytingHom α β) : f.comp (HeytingHom.id α) = f

@[simp]

theorem HeytingHom.id_comp {α : Type u_2} {β : Type u_3} [HeytingAlgebra α] [HeytingAlgebra β] (f : HeytingHom α β) : (HeytingHom.id β).comp f = f

@[simp]

theorem HeytingHom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [HeytingAlgebra α] [HeytingAlgebra β] [HeytingAlgebra γ] {f : HeytingHom α β} {g₁ g₂ : HeytingHom β γ} (hf : Function.Surjective ⇑f) : g₁.comp f = g₂.comp f ↔ g₁ = g₂

@[simp]

theorem HeytingHom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [HeytingAlgebra α] [HeytingAlgebra β] [HeytingAlgebra γ] {f₁ f₂ : HeytingHom α β} {g : HeytingHom β γ} (hg : Function.Injective ⇑g) : g.comp f₁ = g.comp f₂ ↔ f₁ = f₂

instance CoheytingHom.instFunLike {α : Type u_2} {β : Type u_3} [CoheytingAlgebra α] [CoheytingAlgebra β] : FunLike (CoheytingHom α β) α β

instance CoheytingHom.instCoheytingHomClass {α : Type u_2} {β : Type u_3} [CoheytingAlgebra α] [CoheytingAlgebra β] : CoheytingHomClass (CoheytingHom α β) α β

theorem CoheytingHom.toFun_eq_coe {α : Type u_2} {β : Type u_3} [CoheytingAlgebra α] [CoheytingAlgebra β] {f : CoheytingHom α β} : f.toFun = ⇑f

@[simp]

theorem CoheytingHom.toFun_eq_coe_aux {α : Type u_2} {β : Type u_3} [CoheytingAlgebra α] [CoheytingAlgebra β] {f : CoheytingHom α β} : ⇑f.toLatticeHom = ⇑f

theorem CoheytingHom.ext {α : Type u_2} {β : Type u_3} [CoheytingAlgebra α] [CoheytingAlgebra β] {f g : CoheytingHom α β} (h : ∀ (a : α), f a = g a) : f = g

theorem CoheytingHom.ext_iff {α : Type u_2} {β : Type u_3} [CoheytingAlgebra α] [CoheytingAlgebra β] {f g : CoheytingHom α β} : f = g ↔ ∀ (a : α), f a = g a

def CoheytingHom.copy {α : Type u_2} {β : Type u_3} [CoheytingAlgebra α] [CoheytingAlgebra β] (f : CoheytingHom α β) (f' : α → β) (h : f' = ⇑f) : CoheytingHom α β

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

@[simp]

theorem CoheytingHom.coe_copy {α : Type u_2} {β : Type u_3} [CoheytingAlgebra α] [CoheytingAlgebra β] (f : CoheytingHom α β) (f' : α → β) (h : f' = ⇑f) : ⇑(f.copy f' h) = f'

theorem CoheytingHom.copy_eq {α : Type u_2} {β : Type u_3} [CoheytingAlgebra α] [CoheytingAlgebra β] (f : CoheytingHom α β) (f' : α → β) (h : f' = ⇑f) : f.copy f' h = f

def CoheytingHom.id (α : Type u_2) [CoheytingAlgebra α] : CoheytingHom α α

id as a CoheytingHom.

@[simp]

theorem CoheytingHom.coe_id (α : Type u_2) [CoheytingAlgebra α] : ⇑(CoheytingHom.id α) = id

@[simp]

theorem CoheytingHom.id_apply {α : Type u_2} [CoheytingAlgebra α] (a : α) : (CoheytingHom.id α) a = a

instance CoheytingHom.instInhabited {α : Type u_2} [CoheytingAlgebra α] : Inhabited (CoheytingHom α α)

instance CoheytingHom.instPartialOrder {α : Type u_2} {β : Type u_3} [CoheytingAlgebra α] [CoheytingAlgebra β] : PartialOrder (CoheytingHom α β)

def CoheytingHom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CoheytingAlgebra α] [CoheytingAlgebra β] [CoheytingAlgebra γ] (f : CoheytingHom β γ) (g : CoheytingHom α β) : CoheytingHom α γ

Composition of CoheytingHoms as a CoheytingHom.

@[simp]

theorem CoheytingHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CoheytingAlgebra α] [CoheytingAlgebra β] [CoheytingAlgebra γ] (f : CoheytingHom β γ) (g : CoheytingHom α β) : ⇑(f.comp g) = ⇑f ∘ ⇑g

@[simp]

theorem CoheytingHom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CoheytingAlgebra α] [CoheytingAlgebra β] [CoheytingAlgebra γ] (f : CoheytingHom β γ) (g : CoheytingHom α β) (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} [CoheytingAlgebra α] [CoheytingAlgebra β] [CoheytingAlgebra γ] [CoheytingAlgebra δ] (f : CoheytingHom γ δ) (g : CoheytingHom β γ) (h : CoheytingHom α β) : (f.comp g).comp h = f.comp (g.comp h)

@[simp]

theorem CoheytingHom.comp_id {α : Type u_2} {β : Type u_3} [CoheytingAlgebra α] [CoheytingAlgebra β] (f : CoheytingHom α β) : f.comp (CoheytingHom.id α) = f

@[simp]

theorem CoheytingHom.id_comp {α : Type u_2} {β : Type u_3} [CoheytingAlgebra α] [CoheytingAlgebra β] (f : CoheytingHom α β) : (CoheytingHom.id β).comp f = f

@[simp]

theorem CoheytingHom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CoheytingAlgebra α] [CoheytingAlgebra β] [CoheytingAlgebra γ] {f : CoheytingHom α β} {g₁ g₂ : CoheytingHom β γ} (hf : Function.Surjective ⇑f) : g₁.comp f = g₂.comp f ↔ g₁ = g₂

@[simp]

theorem CoheytingHom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CoheytingAlgebra α] [CoheytingAlgebra β] [CoheytingAlgebra γ] {f₁ f₂ : CoheytingHom α β} {g : CoheytingHom β γ} (hg : Function.Injective ⇑g) : g.comp f₁ = g.comp f₂ ↔ f₁ = f₂

instance BiheytingHom.instFunLike {α : Type u_2} {β : Type u_3} [BiheytingAlgebra α] [BiheytingAlgebra β] : FunLike (BiheytingHom α β) α β

instance BiheytingHom.instBiheytingHomClass {α : Type u_2} {β : Type u_3} [BiheytingAlgebra α] [BiheytingAlgebra β] : BiheytingHomClass (BiheytingHom α β) α β

theorem BiheytingHom.toFun_eq_coe {α : Type u_2} {β : Type u_3} [BiheytingAlgebra α] [BiheytingAlgebra β] {f : BiheytingHom α β} : f.toFun = ⇑f

@[simp]

theorem BiheytingHom.toFun_eq_coe_aux {α : Type u_2} {β : Type u_3} [BiheytingAlgebra α] [BiheytingAlgebra β] {f : BiheytingHom α β} : ⇑f.toLatticeHom = ⇑f

theorem BiheytingHom.ext {α : Type u_2} {β : Type u_3} [BiheytingAlgebra α] [BiheytingAlgebra β] {f g : BiheytingHom α β} (h : ∀ (a : α), f a = g a) : f = g

theorem BiheytingHom.ext_iff {α : Type u_2} {β : Type u_3} [BiheytingAlgebra α] [BiheytingAlgebra β] {f g : BiheytingHom α β} : f = g ↔ ∀ (a : α), f a = g a

def BiheytingHom.copy {α : Type u_2} {β : Type u_3} [BiheytingAlgebra α] [BiheytingAlgebra β] (f : BiheytingHom α β) (f' : α → β) (h : f' = ⇑f) : BiheytingHom α β

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

@[simp]

theorem BiheytingHom.coe_copy {α : Type u_2} {β : Type u_3} [BiheytingAlgebra α] [BiheytingAlgebra β] (f : BiheytingHom α β) (f' : α → β) (h : f' = ⇑f) : ⇑(f.copy f' h) = f'

theorem BiheytingHom.copy_eq {α : Type u_2} {β : Type u_3} [BiheytingAlgebra α] [BiheytingAlgebra β] (f : BiheytingHom α β) (f' : α → β) (h : f' = ⇑f) : f.copy f' h = f

def BiheytingHom.id (α : Type u_2) [BiheytingAlgebra α] : BiheytingHom α α

id as a BiheytingHom.

@[simp]

theorem BiheytingHom.coe_id (α : Type u_2) [BiheytingAlgebra α] : ⇑(BiheytingHom.id α) = id

@[simp]

theorem BiheytingHom.id_apply {α : Type u_2} [BiheytingAlgebra α] (a : α) : (BiheytingHom.id α) a = a

instance BiheytingHom.instInhabited {α : Type u_2} [BiheytingAlgebra α] : Inhabited (BiheytingHom α α)

instance BiheytingHom.instPartialOrder {α : Type u_2} {β : Type u_3} [BiheytingAlgebra α] [BiheytingAlgebra β] : PartialOrder (BiheytingHom α β)

def BiheytingHom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [BiheytingAlgebra α] [BiheytingAlgebra β] [BiheytingAlgebra γ] (f : BiheytingHom β γ) (g : BiheytingHom α β) : BiheytingHom α γ

Composition of BiheytingHoms as a BiheytingHom.

@[simp]

theorem BiheytingHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [BiheytingAlgebra α] [BiheytingAlgebra β] [BiheytingAlgebra γ] (f : BiheytingHom β γ) (g : BiheytingHom α β) : ⇑(f.comp g) = ⇑f ∘ ⇑g

@[simp]

theorem BiheytingHom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [BiheytingAlgebra α] [BiheytingAlgebra β] [BiheytingAlgebra γ] (f : BiheytingHom β γ) (g : BiheytingHom α β) (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} [BiheytingAlgebra α] [BiheytingAlgebra β] [BiheytingAlgebra γ] [BiheytingAlgebra δ] (f : BiheytingHom γ δ) (g : BiheytingHom β γ) (h : BiheytingHom α β) : (f.comp g).comp h = f.comp (g.comp h)

@[simp]

theorem BiheytingHom.comp_id {α : Type u_2} {β : Type u_3} [BiheytingAlgebra α] [BiheytingAlgebra β] (f : BiheytingHom α β) : f.comp (BiheytingHom.id α) = f

@[simp]

theorem BiheytingHom.id_comp {α : Type u_2} {β : Type u_3} [BiheytingAlgebra α] [BiheytingAlgebra β] (f : BiheytingHom α β) : (BiheytingHom.id β).comp f = f

@[simp]

theorem BiheytingHom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [BiheytingAlgebra α] [BiheytingAlgebra β] [BiheytingAlgebra γ] {f : BiheytingHom α β} {g₁ g₂ : BiheytingHom β γ} (hf : Function.Surjective ⇑f) : g₁.comp f = g₂.comp f ↔ g₁ = g₂

@[simp]

theorem BiheytingHom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [BiheytingAlgebra α] [BiheytingAlgebra β] [BiheytingAlgebra γ] {f₁ f₂ : BiheytingHom α β} {g : BiheytingHom β γ} (hg : Function.Injective ⇑g) : g.comp f₁ = g.comp f₂ ↔ f₁ = f₂