Homomorphisms of Heyting fields

Content created by Louis Wasserman.

Created on 2025-12-30.
Last modified on 2025-12-30.

module commutative-algebra.homomorphisms-heyting-fields where
Imports 
open import commutative-algebra.heyting-fields
open import commutative-algebra.homomorphisms-commutative-rings

open import foundation.universe-levels

Idea

A homomorphism of Heyting fields is a homomorphism between their underlying commutative rings.

Definition

module _
  {l1 l2 : Level}
  (F : Heyting-Field l1)
  (G : Heyting-Field l2)
  where

  hom-Heyting-Field : UU (l1 ⊔ l2)
  hom-Heyting-Field =
    hom-Commutative-Ring
      ( commutative-ring-Heyting-Field F)
      ( commutative-ring-Heyting-Field G)

Recent changes