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 #

source
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
source
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
source
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
source
@[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
source
@[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
source
@[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
source
@[protected, instance]
def heyting_hom_class.to_bounded_lattice_hom_class {F : Type u_1} {α : Type u_2} {β : Type u_3} [heyting_algebra α] [heyting_algebra β] [heyting_hom_class F α β] :
bounded_lattice_hom_class F α β
Equations
source
@[protected, instance]
def coheyting_hom_class.to_bounded_lattice_hom_class {F : Type u_1} {α : Type u_2} {β : Type u_3} [coheyting_algebra α] [coheyting_algebra β] [coheyting_hom_class F α β] :
bounded_lattice_hom_class F α β
Equations
source
@[protected, instance]
def biheyting_hom_class.to_heyting_hom_class {F : Type u_1} {α : Type u_2} {β : Type u_3} [biheyting_algebra α] [biheyting_algebra β] [biheyting_hom_class F α β] :
heyting_hom_class F α β
Equations
source
@[protected, instance]
def biheyting_hom_class.to_coheyting_hom_class {F : Type u_1} {α : Type u_2} {β : Type u_3} [biheyting_algebra α] [biheyting_algebra β] [biheyting_hom_class F α β] :
coheyting_hom_class F α β
Equations
source
@[protected, instance]
def order_iso_class.to_heyting_hom_class {F : Type u_1} {α : Type u_2} {β : Type u_3} [heyting_algebra α] [heyting_algebra β] [order_iso_class F α β] :
heyting_hom_class F α β
Equations
source
@[protected, instance]
def order_iso_class.to_coheyting_hom_class {F : Type u_1} {α : Type u_2} {β : Type u_3} [coheyting_algebra α] [coheyting_algebra β] [order_iso_class F α β] :
coheyting_hom_class F α β
Equations
source
@[protected, instance]
def order_iso_class.to_biheyting_hom_class {F : Type u_1} {α : Type u_2} {β : Type u_3} [biheyting_algebra α] [biheyting_algebra β] [order_iso_class F α β] :
biheyting_hom_class F α β
Equations
source
@[reducible]
def bounded_lattice_hom_class.to_biheyting_hom_class {F : Type u_1} {α : Type u_2} {β : Type u_3} [boolean_algebra α] [boolean_algebra β] [bounded_lattice_hom_class F α β] :
biheyting_hom_class F α β

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

Equations
source
@[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)ᶜ
source
@[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
source
@[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
source
@[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
source
@[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 α β] :
has_coe_t F (heyting_hom α β)
Equations
source
@[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 α β] :
has_coe_t F (coheyting_hom α β)
Equations
source
@[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 α β] :
has_coe_t F (biheyting_hom α β)
Equations
source
@[protected, instance]
def heyting_hom.heyting_hom_class {α : Type u_2} {β : Type u_3} [heyting_algebra α] [heyting_algebra β] :
heyting_hom_class (heyting_hom α β) α β
Equations
source
@[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
source
@[simp]
theorem heyting_hom.to_fun_eq_coe {α : Type u_2} {β : Type u_3} [heyting_algebra α] [heyting_algebra β] {f : heyting_hom α β} :
f.to_lattice_hom.to_sup_hom.to_fun = ⇑f
source
@[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
source
@[protected]
def heyting_hom.copy {α : Type u_2} {β : Type u_3} [heyting_algebra α] [heyting_algebra β] (f : heyting_hom α β) (f' : α → β) (h : f' = ⇑f) :
heyting_hom α β

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

Equations
source
@[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'
source
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
source
@[protected]
def heyting_hom.id (α : Type u_2) [heyting_algebra α] :
heyting_hom α α

id as a heyting_hom.

Equations
source
@[simp]
theorem heyting_hom.coe_id (α : Type u_2) [heyting_algebra α] :
⇑(heyting_hom.id α) = id
source
@[simp]
theorem heyting_hom.id_apply {α : Type u_2} [heyting_algebra α] (a : α) :
⇑(heyting_hom.id α) a = a
source
@[protected, instance]
def heyting_hom.inhabited {α : Type u_2} [heyting_algebra α] :
inhabited (heyting_hom α α)
Equations
source
@[protected, instance]
def heyting_hom.partial_order {α : Type u_2} {β : Type u_3} [heyting_algebra α] [heyting_algebra β] :
partial_order (heyting_hom α β)
Equations
source
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 α β) :
heyting_hom α γ

Composition of heyting_homs as a heyting_hom.

Equations
source
@[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
source
@[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)
source
@[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)
source
@[simp]
theorem heyting_hom.comp_id {α : Type u_2} {β : Type u_3} [heyting_algebra α] [heyting_algebra β] (f : heyting_hom α β) :
f.comp (heyting_hom.id α) = f
source
@[simp]
theorem heyting_hom.id_comp {α : Type u_2} {β : Type u_3} [heyting_algebra α] [heyting_algebra β] (f : heyting_hom α β) :
(heyting_hom.id β).comp f = f
source
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₂
source
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₂
source
@[protected, instance]
def coheyting_hom.coheyting_hom_class {α : Type u_2} {β : Type u_3} [coheyting_algebra α] [coheyting_algebra β] :
coheyting_hom_class (coheyting_hom α β) α β
Equations
source
@[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
source
@[simp]
theorem coheyting_hom.to_fun_eq_coe {α : Type u_2} {β : Type u_3} [coheyting_algebra α] [coheyting_algebra β] {f : coheyting_hom α β} :
f.to_lattice_hom.to_sup_hom.to_fun = ⇑f
source
@[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
source
@[protected]
def coheyting_hom.copy {α : Type u_2} {β : Type u_3} [coheyting_algebra α] [coheyting_algebra β] (f : coheyting_hom α β) (f' : α → β) (h : f' = ⇑f) :
coheyting_hom α β

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

Equations
source
@[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'
source
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
source
@[protected]
def coheyting_hom.id (α : Type u_2) [coheyting_algebra α] :
coheyting_hom α α

id as a coheyting_hom.

Equations
source
@[simp]
theorem coheyting_hom.coe_id (α : Type u_2) [coheyting_algebra α] :
⇑(coheyting_hom.id α) = id
source
@[simp]
theorem coheyting_hom.id_apply {α : Type u_2} [coheyting_algebra α] (a : α) :
⇑(coheyting_hom.id α) a = a
source
@[protected, instance]
def coheyting_hom.inhabited {α : Type u_2} [coheyting_algebra α] :
inhabited (coheyting_hom α α)
Equations
source
@[protected, instance]
def coheyting_hom.partial_order {α : Type u_2} {β : Type u_3} [coheyting_algebra α] [coheyting_algebra β] :
partial_order (coheyting_hom α β)
Equations
source
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 α β) :
coheyting_hom α γ

Composition of coheyting_homs as a coheyting_hom.

Equations
source
@[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
source
@[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)
source
@[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)
source
@[simp]
theorem coheyting_hom.comp_id {α : Type u_2} {β : Type u_3} [coheyting_algebra α] [coheyting_algebra β] (f : coheyting_hom α β) :
f.comp (coheyting_hom.id α) = f
source
@[simp]
theorem coheyting_hom.id_comp {α : Type u_2} {β : Type u_3} [coheyting_algebra α] [coheyting_algebra β] (f : coheyting_hom α β) :
(coheyting_hom.id β).comp f = f
source
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₂
source
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₂
source
@[protected, instance]
def biheyting_hom.biheyting_hom_class {α : Type u_2} {β : Type u_3} [biheyting_algebra α] [biheyting_algebra β] :
biheyting_hom_class (biheyting_hom α β) α β
Equations
source
@[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
source
@[simp]
theorem biheyting_hom.to_fun_eq_coe {α : Type u_2} {β : Type u_3} [biheyting_algebra α] [biheyting_algebra β] {f : biheyting_hom α β} :
f.to_lattice_hom.to_sup_hom.to_fun = ⇑f
source
@[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
source
@[protected]
def biheyting_hom.copy {α : Type u_2} {β : Type u_3} [biheyting_algebra α] [biheyting_algebra β] (f : biheyting_hom α β) (f' : α → β) (h : f' = ⇑f) :
biheyting_hom α β

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

Equations
source
@[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'
source
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
source
@[protected]
def biheyting_hom.id (α : Type u_2) [biheyting_algebra α] :
biheyting_hom α α

id as a biheyting_hom.

Equations
source
@[simp]
theorem biheyting_hom.coe_id (α : Type u_2) [biheyting_algebra α] :
⇑(biheyting_hom.id α) = id
source
@[simp]
theorem biheyting_hom.id_apply {α : Type u_2} [biheyting_algebra α] (a : α) :
⇑(biheyting_hom.id α) a = a
source
@[protected, instance]
def biheyting_hom.inhabited {α : Type u_2} [biheyting_algebra α] :
inhabited (biheyting_hom α α)
Equations
source
@[protected, instance]
def biheyting_hom.partial_order {α : Type u_2} {β : Type u_3} [biheyting_algebra α] [biheyting_algebra β] :
partial_order (biheyting_hom α β)
Equations
source
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 α β) :
biheyting_hom α γ

Composition of biheyting_homs as a biheyting_hom.

Equations
source
@[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
source
@[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)
source
@[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)
source
@[simp]
theorem biheyting_hom.comp_id {α : Type u_2} {β : Type u_3} [biheyting_algebra α] [biheyting_algebra β] (f : biheyting_hom α β) :
f.comp (biheyting_hom.id α) = f
source
@[simp]
theorem biheyting_hom.id_comp {α : Type u_2} {β : Type u_3} [biheyting_algebra α] [biheyting_algebra β] (f : biheyting_hom α β) :
(biheyting_hom.id β).comp f = f
source
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₂
source
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₂