Heyting Algebra - Quotients

Quotients

Let H be a Heyting algebra, and let F ⊆ H. We call F a filter on H if it satisfies the following properties:

The intersection of any set of filters on H is again a filter. Therefore, given any subset S of H there is a smallest filter containing S. We call it the filter generated by S. If S is empty, F = {1}. Otherwise, F is equal to the set of x in H such that there exist y₁, y₂, …, y_n ∈ S with y₁ ∧ y₂ ∧ … ∧ y_n ≤ x.

If H is a Heyting algebra and F is a filter on H, we define a relation ∼ on H as follows: we write x ∼ y whenever x → y and y → x both belong to F. Then ∼ is an equivalence relation; we write H/F for the quotient set. There is a unique Heyting algebra structure on H/F such that the canonical surjection p_F : H → H/F becomes a Heyting algebra morphism. We call the Heyting algebra H/F the quotient of H by F.

Let S be a subset of a Heyting algebra H and let F be the filter generated by S. Then H/F satisfies the following universal property:

• Given any morphism of Heyting algebras ƒ : H → H′ satisfying ƒ(y) = 1 for every y ∈ S, ƒ factors uniquely through the canonical surjection p_F : H → H/F. That is, there is a unique morphism ƒ′ : H/F → H′ satisfying ƒ′p_F = ƒ. The morphism ƒ′ is said to be induced by ƒ.

Let f : H₁ → H₂ be a morphism of Heyting algebras. The kernel of ƒ, written ker ƒ, is the set ƒ−1. It is a filter on H₁. (Care should be taken because this definition, if applied to a morphism of Boolean algebras, is dual to what would be called the kernel of the morphism viewed as a morphism of rings.) By the foregoing, ƒ induces a morphism ƒ′ : H₁/(ker ƒ) → H₂. It is an isomorphism of H₁/(ker ƒ) onto the subalgebra ƒ of H₂.