mathlib3 documentation

order.heyting.hom

Heyting algebra morphisms #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

We use the fun_like 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 #

Typeclasses #

structure heyting_hom (α : Type u_6) (β : Type u_7) [heyting_algebra α] [heyting_algebra β] :
Type (max u_6 u_7)

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

Instances for heyting_hom
structure coheyting_hom (α : Type u_6) (β : Type u_7) [coheyting_algebra α] [coheyting_algebra β] :
Type (max u_6 u_7)

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

Instances for coheyting_hom
structure biheyting_hom (α : Type u_6) (β : Type u_7) [biheyting_algebra α] [biheyting_algebra β] :
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 biheyting_hom
@[class]
structure heyting_hom_class (F : Type u_6) (α : out_param (Type u_7)) (β : out_param (Type u_8)) [heyting_algebra α] [heyting_algebra β] :
Type (max u_6 u_7 u_8)

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

You should extend this class when you extend heyting_hom.

Instances of this typeclass
Instances of other typeclasses for heyting_hom_class
  • heyting_hom_class.has_sizeof_inst
@[class]
structure coheyting_hom_class (F : Type u_6) (α : out_param (Type u_7)) (β : out_param (Type u_8)) [coheyting_algebra α] [coheyting_algebra β] :
Type (max u_6 u_7 u_8)

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

You should extend this class when you extend coheyting_hom.

Instances of this typeclass
Instances of other typeclasses for coheyting_hom_class
  • coheyting_hom_class.has_sizeof_inst
@[class]
structure biheyting_hom_class (F : Type u_6) (α : out_param (Type u_7)) (β : out_param (Type u_8)) [biheyting_algebra α] [biheyting_algebra β] :
Type (max u_6 u_7 u_8)

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

You should extend this class when you extend biheyting_hom.

Instances of this typeclass
Instances of other typeclasses for biheyting_hom_class
  • biheyting_hom_class.has_sizeof_inst
@[reducible]

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

Equations
@[simp]
theorem map_compl {F : Type u_1} {α : Type u_2} {β : Type u_3} [heyting_algebra α] [heyting_algebra β] [heyting_hom_class F α β] (f : F) (a : α) :
f a = (f a)
@[simp]
theorem map_bihimp {F : Type u_1} {α : Type u_2} {β : Type u_3} [heyting_algebra α] [heyting_algebra β] [heyting_hom_class F α β] (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} [coheyting_algebra α] [coheyting_algebra β] [coheyting_hom_class F α β] (f : F) (a : α) :
f (a) = f a
@[simp]
theorem map_symm_diff {F : Type u_1} {α : Type u_2} {β : Type u_3} [coheyting_algebra α] [coheyting_algebra β] [coheyting_hom_class F α β] (f : F) (a b : α) :
f (a b) = f a f b
@[protected, instance]
def heyting_hom.has_coe_t {F : Type u_1} {α : Type u_2} {β : Type u_3} [heyting_algebra α] [heyting_algebra β] [heyting_hom_class F α β] :
Equations
@[protected, instance]
def coheyting_hom.has_coe_t {F : Type u_1} {α : Type u_2} {β : Type u_3} [coheyting_algebra α] [coheyting_algebra β] [coheyting_hom_class F α β] :
Equations
@[protected, instance]
def biheyting_hom.has_coe_t {F : Type u_1} {α : Type u_2} {β : Type u_3} [biheyting_algebra α] [biheyting_algebra β] [biheyting_hom_class F α β] :
Equations
@[protected, instance]
Equations
@[protected, instance]
def heyting_hom.has_coe_to_fun {α : Type u_2} {β : Type u_3} [heyting_algebra α] [heyting_algebra β] :
has_coe_to_fun (heyting_hom α β) (λ (_x : heyting_hom α β), α β)

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun directly.

Equations
@[simp]
@[ext]
theorem heyting_hom.ext {α : Type u_2} {β : Type u_3} [heyting_algebra α] [heyting_algebra β] {f g : heyting_hom α β} (h : (a : α), f a = g a) :
f = g
@[protected]
def heyting_hom.copy {α : Type u_2} {β : Type u_3} [heyting_algebra α] [heyting_algebra β] (f : heyting_hom α β) (f' : α β) (h : f' = f) :

Copy of a heyting_hom with a new to_fun equal to the old one. Useful to fix definitional equalities.

Equations
@[simp]
theorem heyting_hom.coe_copy {α : Type u_2} {β : Type u_3} [heyting_algebra α] [heyting_algebra β] (f : heyting_hom α β) (f' : α β) (h : f' = f) :
(f.copy f' h) = f'
theorem heyting_hom.copy_eq {α : Type u_2} {β : Type u_3} [heyting_algebra α] [heyting_algebra β] (f : heyting_hom α β) (f' : α β) (h : f' = f) :
f.copy f' h = f
@[simp]
theorem heyting_hom.coe_id (α : Type u_2) [heyting_algebra α] :
@[simp]
theorem heyting_hom.id_apply {α : Type u_2} [heyting_algebra α] (a : α) :
@[protected, instance]
Equations
@[protected, instance]
Equations
def heyting_hom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [heyting_algebra α] [heyting_algebra β] [heyting_algebra γ] (f : heyting_hom β γ) (g : heyting_hom α β) :

Composition of heyting_homs as a heyting_hom.

Equations
@[simp]
theorem heyting_hom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [heyting_algebra α] [heyting_algebra β] [heyting_algebra γ] (f : heyting_hom β γ) (g : heyting_hom α β) :
(f.comp g) = f g
@[simp]
theorem heyting_hom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [heyting_algebra α] [heyting_algebra β] [heyting_algebra γ] (f : heyting_hom β γ) (g : heyting_hom α β) (a : α) :
(f.comp g) a = f (g a)
@[simp]
theorem heyting_hom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [heyting_algebra α] [heyting_algebra β] [heyting_algebra γ] [heyting_algebra δ] (f : heyting_hom γ δ) (g : heyting_hom β γ) (h : heyting_hom α β) :
(f.comp g).comp h = f.comp (g.comp h)
@[simp]
theorem heyting_hom.comp_id {α : Type u_2} {β : Type u_3} [heyting_algebra α] [heyting_algebra β] (f : heyting_hom α β) :
@[simp]
theorem heyting_hom.id_comp {α : Type u_2} {β : Type u_3} [heyting_algebra α] [heyting_algebra β] (f : heyting_hom α β) :
theorem heyting_hom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [heyting_algebra α] [heyting_algebra β] [heyting_algebra γ] {f : heyting_hom α β} {g₁ g₂ : heyting_hom β γ} (hf : function.surjective f) :
g₁.comp f = g₂.comp f g₁ = g₂
theorem heyting_hom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [heyting_algebra α] [heyting_algebra β] [heyting_algebra γ] {f₁ f₂ : heyting_hom α β} {g : heyting_hom β γ} (hg : function.injective g) :
g.comp f₁ = g.comp f₂ f₁ = f₂
@[protected, instance]
def coheyting_hom.has_coe_to_fun {α : Type u_2} {β : Type u_3} [coheyting_algebra α] [coheyting_algebra β] :
has_coe_to_fun (coheyting_hom α β) (λ (_x : coheyting_hom α β), α β)

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun directly.

Equations
@[ext]
theorem coheyting_hom.ext {α : Type u_2} {β : Type u_3} [coheyting_algebra α] [coheyting_algebra β] {f g : coheyting_hom α β} (h : (a : α), f a = g a) :
f = g
@[protected]
def coheyting_hom.copy {α : Type u_2} {β : Type u_3} [coheyting_algebra α] [coheyting_algebra β] (f : coheyting_hom α β) (f' : α β) (h : f' = f) :

Copy of a coheyting_hom with a new to_fun equal to the old one. Useful to fix definitional equalities.

Equations
@[simp]
theorem coheyting_hom.coe_copy {α : Type u_2} {β : Type u_3} [coheyting_algebra α] [coheyting_algebra β] (f : coheyting_hom α β) (f' : α β) (h : f' = f) :
(f.copy f' h) = f'
theorem coheyting_hom.copy_eq {α : Type u_2} {β : Type u_3} [coheyting_algebra α] [coheyting_algebra β] (f : coheyting_hom α β) (f' : α β) (h : f' = f) :
f.copy f' h = f
@[simp]
@[simp]
theorem coheyting_hom.id_apply {α : Type u_2} [coheyting_algebra α] (a : α) :
@[protected, instance]
Equations
@[protected, instance]
Equations
def coheyting_hom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [coheyting_algebra α] [coheyting_algebra β] [coheyting_algebra γ] (f : coheyting_hom β γ) (g : coheyting_hom α β) :

Composition of coheyting_homs as a coheyting_hom.

Equations
@[simp]
theorem coheyting_hom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [coheyting_algebra α] [coheyting_algebra β] [coheyting_algebra γ] (f : coheyting_hom β γ) (g : coheyting_hom α β) :
(f.comp g) = f g
@[simp]
theorem coheyting_hom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [coheyting_algebra α] [coheyting_algebra β] [coheyting_algebra γ] (f : coheyting_hom β γ) (g : coheyting_hom α β) (a : α) :
(f.comp g) a = f (g a)
@[simp]
theorem coheyting_hom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [coheyting_algebra α] [coheyting_algebra β] [coheyting_algebra γ] [coheyting_algebra δ] (f : coheyting_hom γ δ) (g : coheyting_hom β γ) (h : coheyting_hom α β) :
(f.comp g).comp h = f.comp (g.comp h)
@[simp]
theorem coheyting_hom.comp_id {α : Type u_2} {β : Type u_3} [coheyting_algebra α] [coheyting_algebra β] (f : coheyting_hom α β) :
@[simp]
theorem coheyting_hom.id_comp {α : Type u_2} {β : Type u_3} [coheyting_algebra α] [coheyting_algebra β] (f : coheyting_hom α β) :
theorem coheyting_hom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [coheyting_algebra α] [coheyting_algebra β] [coheyting_algebra γ] {f : coheyting_hom α β} {g₁ g₂ : coheyting_hom β γ} (hf : function.surjective f) :
g₁.comp f = g₂.comp f g₁ = g₂
theorem coheyting_hom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [coheyting_algebra α] [coheyting_algebra β] [coheyting_algebra γ] {f₁ f₂ : coheyting_hom α β} {g : coheyting_hom β γ} (hg : function.injective g) :
g.comp f₁ = g.comp f₂ f₁ = f₂
@[protected, instance]
def biheyting_hom.has_coe_to_fun {α : Type u_2} {β : Type u_3} [biheyting_algebra α] [biheyting_algebra β] :
has_coe_to_fun (biheyting_hom α β) (λ (_x : biheyting_hom α β), α β)

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun directly.

Equations
@[ext]
theorem biheyting_hom.ext {α : Type u_2} {β : Type u_3} [biheyting_algebra α] [biheyting_algebra β] {f g : biheyting_hom α β} (h : (a : α), f a = g a) :
f = g
@[protected]
def biheyting_hom.copy {α : Type u_2} {β : Type u_3} [biheyting_algebra α] [biheyting_algebra β] (f : biheyting_hom α β) (f' : α β) (h : f' = f) :

Copy of a biheyting_hom with a new to_fun equal to the old one. Useful to fix definitional equalities.

Equations
@[simp]
theorem biheyting_hom.coe_copy {α : Type u_2} {β : Type u_3} [biheyting_algebra α] [biheyting_algebra β] (f : biheyting_hom α β) (f' : α β) (h : f' = f) :
(f.copy f' h) = f'
theorem biheyting_hom.copy_eq {α : Type u_2} {β : Type u_3} [biheyting_algebra α] [biheyting_algebra β] (f : biheyting_hom α β) (f' : α β) (h : f' = f) :
f.copy f' h = f
@[simp]
@[simp]
theorem biheyting_hom.id_apply {α : Type u_2} [biheyting_algebra α] (a : α) :
@[protected, instance]
Equations
@[protected, instance]
Equations
def biheyting_hom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [biheyting_algebra α] [biheyting_algebra β] [biheyting_algebra γ] (f : biheyting_hom β γ) (g : biheyting_hom α β) :

Composition of biheyting_homs as a biheyting_hom.

Equations
@[simp]
theorem biheyting_hom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [biheyting_algebra α] [biheyting_algebra β] [biheyting_algebra γ] (f : biheyting_hom β γ) (g : biheyting_hom α β) :
(f.comp g) = f g
@[simp]
theorem biheyting_hom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [biheyting_algebra α] [biheyting_algebra β] [biheyting_algebra γ] (f : biheyting_hom β γ) (g : biheyting_hom α β) (a : α) :
(f.comp g) a = f (g a)
@[simp]
theorem biheyting_hom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [biheyting_algebra α] [biheyting_algebra β] [biheyting_algebra γ] [biheyting_algebra δ] (f : biheyting_hom γ δ) (g : biheyting_hom β γ) (h : biheyting_hom α β) :
(f.comp g).comp h = f.comp (g.comp h)
@[simp]
theorem biheyting_hom.comp_id {α : Type u_2} {β : Type u_3} [biheyting_algebra α] [biheyting_algebra β] (f : biheyting_hom α β) :
@[simp]
theorem biheyting_hom.id_comp {α : Type u_2} {β : Type u_3} [biheyting_algebra α] [biheyting_algebra β] (f : biheyting_hom α β) :
theorem biheyting_hom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [biheyting_algebra α] [biheyting_algebra β] [biheyting_algebra γ] {f : biheyting_hom α β} {g₁ g₂ : biheyting_hom β γ} (hf : function.surjective f) :
g₁.comp f = g₂.comp f g₁ = g₂
theorem biheyting_hom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [biheyting_algebra α] [biheyting_algebra β] [biheyting_algebra γ] {f₁ f₂ : biheyting_hom α β} {g : biheyting_hom β γ} (hg : function.injective g) :
g.comp f₁ = g.comp f₂ f₁ = f₂