feat(order/hom/heyting): Heyting homomorphisms (#15308)

Define the type of Heyting homomorphisms, maps between Heyting algebras that preserve Heyting implication.

src/algebra/ring/boolean_ring.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bryan Gin-ge Chen, Yaël Dillies
 -/
 import algebra.punit_instances
-import order.hom.lattice
+import order.heyting.hom
 import tactic.abel
 import tactic.ring
 
@@ -359,7 +359,7 @@ from `α` to `β` considered as Boolean rings. -/
 { to_fun := to_boolring ∘ f ∘ of_boolring,
   map_zero' := f.map_bot',
   map_one' := f.map_top',
-  map_add' := map_symm_diff f,
+  map_add' := map_symm_diff' f,
   map_mul' := f.map_inf' }
 
 @[simp] lemma bounded_lattice_hom.as_boolring_id :

src/data/fun_like/equiv.lean

@@ -175,6 +175,22 @@ function.injective.of_comp_iff' f (equiv_like.bijective e)
   function.bijective (f ∘ e) ↔ function.bijective f :=
 (equiv_like.bijective e).of_comp_iff f
 
+/-- This lemma is only supposed to be used in the generic context, when working with instances
+of classes extending `equiv_like`.
+For concrete isomorphism types such as `equiv`, you should use `equiv.symm_apply_apply`
+or its equivalent.
+
+TODO: define a generic form of `equiv.symm`. -/
+@[simp] lemma inv_apply_apply (e : E) (a : α) : equiv_like.inv e (e a) = a := left_inv _ _
+
+/-- This lemma is only supposed to be used in the generic context, when working with instances
+of classes extending `equiv_like`.
+For concrete isomorphism types such as `equiv`, you should use `equiv.apply_symm_apply`
+or its equivalent.
+
+TODO: define a generic form of `equiv.symm`. -/
+@[simp] lemma apply_inv_apply (e : E) (b : β) : e (equiv_like.inv e b) = b := right_inv _ _
+
 omit iE
 include iF
 

src/order/heyting/basic.lean

@@ -61,7 +61,7 @@ variables {ι α β : Type*}
 
 /-- Syntax typeclass for Heyting negation `￢`.
 
-The difference between `has_hnot` and `has_compl` is that the former belongs to Heyting algebras,
+The difference between `has_compl` and `has_hnot` is that the former belongs to Heyting algebras,
 while the latter belongs to co-Heyting algebras. They are both pseudo-complements, but `compl`
 underestimates while `hnot` overestimates. In boolean algebras, they are equal. See `hnot_eq_compl`.
 -/