Homomorphisms of commutative rings
module commutative-algebra.homomorphisms-commutative-rings where
Imports
open import commutative-algebra.commutative-rings open import commutative-algebra.homomorphisms-commutative-semirings open import foundation.contractible-types open import foundation.dependent-pair-types open import foundation.equivalences open import foundation.identity-types open import foundation.propositions open import foundation.sets open import foundation.universe-levels open import group-theory.homomorphisms-abelian-groups open import group-theory.homomorphisms-monoids open import ring-theory.homomorphisms-rings
Idea
A homomorphism of commutative rings is a homomorphism between their underlying rings.
Definition
The predicate of being a ring homomorphism
module _ {l1 l2 : Level} (A : Commutative-Ring l1) (B : Commutative-Ring l2) where is-commutative-ring-homomorphism-hom-Ab-Prop : type-hom-Ab (ab-Commutative-Ring A) (ab-Commutative-Ring B) → Prop (l1 ⊔ l2) is-commutative-ring-homomorphism-hom-Ab-Prop = is-ring-homomorphism-hom-Ab-Prop ( ring-Commutative-Ring A) ( ring-Commutative-Ring B) is-commutative-ring-homomorphism-hom-Ab : type-hom-Ab (ab-Commutative-Ring A) (ab-Commutative-Ring B) → UU (l1 ⊔ l2) is-commutative-ring-homomorphism-hom-Ab = is-ring-homomorphism-hom-Ab ( ring-Commutative-Ring A) ( ring-Commutative-Ring B) is-prop-is-commutative-ring-homomorphism-hom-Ab : (f : type-hom-Ab (ab-Commutative-Ring A) (ab-Commutative-Ring B)) → is-prop (is-commutative-ring-homomorphism-hom-Ab f) is-prop-is-commutative-ring-homomorphism-hom-Ab = is-prop-is-ring-homomorphism-hom-Ab ( ring-Commutative-Ring A) ( ring-Commutative-Ring B)
module _ {l1 l2 : Level} (A : Commutative-Ring l1) (B : Commutative-Ring l2) where hom-Commutative-Ring : Set (l1 ⊔ l2) hom-Commutative-Ring = hom-Ring (ring-Commutative-Ring A) (ring-Commutative-Ring B) type-hom-Commutative-Ring : UU (l1 ⊔ l2) type-hom-Commutative-Ring = type-hom-Ring (ring-Commutative-Ring A) (ring-Commutative-Ring B) is-set-type-hom-Commutative-Ring : is-set type-hom-Commutative-Ring is-set-type-hom-Commutative-Ring = is-set-type-hom-Ring (ring-Commutative-Ring A) (ring-Commutative-Ring B) module _ (f : type-hom-Commutative-Ring) where hom-ab-hom-Commutative-Ring : type-hom-Ab (ab-Commutative-Ring A) (ab-Commutative-Ring B) hom-ab-hom-Commutative-Ring = hom-ab-hom-Ring (ring-Commutative-Ring A) (ring-Commutative-Ring B) f hom-multiplicative-monoid-hom-Commutative-Ring : type-hom-Monoid ( multiplicative-monoid-Commutative-Ring A) ( multiplicative-monoid-Commutative-Ring B) hom-multiplicative-monoid-hom-Commutative-Ring = hom-multiplicative-monoid-hom-Ring ( ring-Commutative-Ring A) ( ring-Commutative-Ring B) ( f) map-hom-Commutative-Ring : type-Commutative-Ring A → type-Commutative-Ring B map-hom-Commutative-Ring = map-hom-Ring ( ring-Commutative-Ring A) ( ring-Commutative-Ring B) ( f) preserves-add-hom-Commutative-Ring : preserves-add-Ab ( ab-Commutative-Ring A) ( ab-Commutative-Ring B) ( map-hom-Commutative-Ring) preserves-add-hom-Commutative-Ring = preserves-add-hom-Ring ( ring-Commutative-Ring A) ( ring-Commutative-Ring B) ( f) preserves-zero-hom-Commutative-Ring : preserves-zero-Ab ( ab-Commutative-Ring A) ( ab-Commutative-Ring B) ( map-hom-Commutative-Ring) preserves-zero-hom-Commutative-Ring = preserves-zero-hom-Ring ( ring-Commutative-Ring A) ( ring-Commutative-Ring B) ( f) preserves-neg-hom-Commutative-Ring : preserves-negatives-Ab ( ab-Commutative-Ring A) ( ab-Commutative-Ring B) ( map-hom-Commutative-Ring) preserves-neg-hom-Commutative-Ring = preserves-neg-hom-Ring ( ring-Commutative-Ring A) ( ring-Commutative-Ring B) ( f) preserves-mul-hom-Commutative-Ring : preserves-mul-hom-Ab ( ring-Commutative-Ring A) ( ring-Commutative-Ring B) ( hom-ab-hom-Commutative-Ring) preserves-mul-hom-Commutative-Ring = preserves-mul-hom-Ring ( ring-Commutative-Ring A) ( ring-Commutative-Ring B) ( f) preserves-unit-hom-Commutative-Ring : preserves-unit-hom-Ab ( ring-Commutative-Ring A) ( ring-Commutative-Ring B) ( hom-ab-hom-Commutative-Ring) preserves-unit-hom-Commutative-Ring = preserves-unit-hom-Ring ( ring-Commutative-Ring A) ( ring-Commutative-Ring B) ( f) is-commutative-ring-homomorphism-hom-Commutative-Ring : is-commutative-ring-homomorphism-hom-Ab A B hom-ab-hom-Commutative-Ring is-commutative-ring-homomorphism-hom-Commutative-Ring = is-ring-homomorphism-hom-Ring ( ring-Commutative-Ring A) ( ring-Commutative-Ring B) ( f) hom-commutative-semiring-hom-Commutative-Ring : type-hom-Commutative-Semiring ( commutative-semiring-Commutative-Ring A) ( commutative-semiring-Commutative-Ring B) hom-commutative-semiring-hom-Commutative-Ring = hom-semiring-hom-Ring ( ring-Commutative-Ring A) ( ring-Commutative-Ring B) ( f)
The identity homomorphism of commutative rings
module _ {l : Level} (A : Commutative-Ring l) where preserves-mul-id-hom-Commutative-Ring : preserves-mul-hom-Ab ( ring-Commutative-Ring A) ( ring-Commutative-Ring A) ( id-hom-Ab (ab-Commutative-Ring A)) preserves-mul-id-hom-Commutative-Ring = preserves-mul-id-hom-Ring (ring-Commutative-Ring A) preserves-unit-id-hom-Commutative-Ring : preserves-unit-hom-Ab ( ring-Commutative-Ring A) ( ring-Commutative-Ring A) ( id-hom-Ab (ab-Commutative-Ring A)) preserves-unit-id-hom-Commutative-Ring = preserves-unit-id-hom-Ring (ring-Commutative-Ring A) is-ring-homomorphism-id-hom-Commutative-Ring : is-ring-homomorphism-hom-Ab ( ring-Commutative-Ring A) ( ring-Commutative-Ring A) ( id-hom-Ab (ab-Commutative-Ring A)) is-ring-homomorphism-id-hom-Commutative-Ring = is-ring-homomorphism-id-hom-Ring (ring-Commutative-Ring A) id-hom-Commutative-Ring : type-hom-Commutative-Ring A A id-hom-Commutative-Ring = id-hom-Ring (ring-Commutative-Ring A)
Composition of commutative ring homomorphisms
module _ {l1 l2 l3 : Level} (A : Commutative-Ring l1) (B : Commutative-Ring l2) (C : Commutative-Ring l3) (g : type-hom-Commutative-Ring B C) (f : type-hom-Commutative-Ring A B) where hom-ab-comp-hom-Commutative-Ring : type-hom-Ab (ab-Commutative-Ring A) (ab-Commutative-Ring C) hom-ab-comp-hom-Commutative-Ring = hom-ab-comp-hom-Ring ( ring-Commutative-Ring A) ( ring-Commutative-Ring B) ( ring-Commutative-Ring C) ( g) ( f) hom-multiplicative-monoid-comp-hom-Commutative-Ring : type-hom-Monoid ( multiplicative-monoid-Commutative-Ring A) ( multiplicative-monoid-Commutative-Ring C) hom-multiplicative-monoid-comp-hom-Commutative-Ring = hom-multiplicative-monoid-comp-hom-Ring ( ring-Commutative-Ring A) ( ring-Commutative-Ring B) ( ring-Commutative-Ring C) ( g) ( f) preserves-mul-comp-hom-Commutative-Ring : preserves-mul-hom-Ab ( ring-Commutative-Ring A) ( ring-Commutative-Ring C) ( hom-ab-comp-hom-Commutative-Ring) preserves-mul-comp-hom-Commutative-Ring = preserves-mul-comp-hom-Ring ( ring-Commutative-Ring A) ( ring-Commutative-Ring B) ( ring-Commutative-Ring C) ( g) ( f) preserves-unit-comp-hom-Commutative-Ring : preserves-unit-hom-Ab ( ring-Commutative-Ring A) ( ring-Commutative-Ring C) ( hom-ab-comp-hom-Commutative-Ring) preserves-unit-comp-hom-Commutative-Ring = preserves-unit-comp-hom-Ring ( ring-Commutative-Ring A) ( ring-Commutative-Ring B) ( ring-Commutative-Ring C) ( g) ( f) is-commutative-ring-homomorphism-comp-hom-Commutative-Ring : is-commutative-ring-homomorphism-hom-Ab A C ( hom-ab-comp-hom-Commutative-Ring) is-commutative-ring-homomorphism-comp-hom-Commutative-Ring = is-ring-homomorphism-comp-hom-Ring ( ring-Commutative-Ring A) ( ring-Commutative-Ring B) ( ring-Commutative-Ring C) ( g) ( f) comp-hom-Commutative-Ring : type-hom-Commutative-Ring A C comp-hom-Commutative-Ring = comp-hom-Ring ( ring-Commutative-Ring A) ( ring-Commutative-Ring B) ( ring-Commutative-Ring C) ( g) ( f)
Homotopies of homomorphisms of commutative rings
module _ {l1 l2 : Level} (A : Commutative-Ring l1) (B : Commutative-Ring l2) where htpy-hom-Commutative-Ring : type-hom-Commutative-Ring A B → type-hom-Commutative-Ring A B → UU (l1 ⊔ l2) htpy-hom-Commutative-Ring = htpy-hom-Ring ( ring-Commutative-Ring A) ( ring-Commutative-Ring B) refl-htpy-hom-Commutative-Ring : (f : type-hom-Commutative-Ring A B) → htpy-hom-Commutative-Ring f f refl-htpy-hom-Commutative-Ring = refl-htpy-hom-Ring ( ring-Commutative-Ring A) ( ring-Commutative-Ring B)
Properties
Homotopies characterize identifications of homomorphisms of commutative rings
module _ {l1 l2 : Level} (A : Commutative-Ring l1) (B : Commutative-Ring l2) (f : type-hom-Commutative-Ring A B) where htpy-eq-hom-Commutative-Ring : (g : type-hom-Commutative-Ring A B) → (f ＝ g) → htpy-hom-Commutative-Ring A B f g htpy-eq-hom-Commutative-Ring = htpy-eq-hom-Ring ( ring-Commutative-Ring A) ( ring-Commutative-Ring B) ( f) is-contr-total-htpy-hom-Commutative-Ring : is-contr ( Σ (type-hom-Commutative-Ring A B) (htpy-hom-Commutative-Ring A B f)) is-contr-total-htpy-hom-Commutative-Ring = is-contr-total-htpy-hom-Ring ( ring-Commutative-Ring A) ( ring-Commutative-Ring B) ( f) is-equiv-htpy-eq-hom-Commutative-Ring : (g : type-hom-Commutative-Ring A B) → is-equiv (htpy-eq-hom-Commutative-Ring g) is-equiv-htpy-eq-hom-Commutative-Ring = is-equiv-htpy-eq-hom-Ring ( ring-Commutative-Ring A) ( ring-Commutative-Ring B) ( f) extensionality-hom-Commutative-Ring : (g : type-hom-Commutative-Ring A B) → (f ＝ g) ≃ htpy-hom-Commutative-Ring A B f g extensionality-hom-Commutative-Ring = extensionality-hom-Ring ( ring-Commutative-Ring A) ( ring-Commutative-Ring B) ( f) eq-htpy-hom-Commutative-Ring : (g : type-hom-Commutative-Ring A B) → htpy-hom-Commutative-Ring A B f g → f ＝ g eq-htpy-hom-Commutative-Ring = eq-htpy-hom-Ring ( ring-Commutative-Ring A) ( ring-Commutative-Ring B) ( f)
Associativity of composition of ring homomorphisms
module _ {l1 l2 l3 l4 : Level} (A : Commutative-Ring l1) (B : Commutative-Ring l2) (C : Commutative-Ring l3) (D : Commutative-Ring l4) (h : type-hom-Commutative-Ring C D) (g : type-hom-Commutative-Ring B C) (f : type-hom-Commutative-Ring A B) where associative-comp-hom-Commutative-Ring : ( comp-hom-Commutative-Ring A B D ( comp-hom-Commutative-Ring B C D h g) ( f)) ＝ ( comp-hom-Commutative-Ring A C D ( h) ( comp-hom-Commutative-Ring A B C g f)) associative-comp-hom-Commutative-Ring = associative-comp-hom-Ring ( ring-Commutative-Ring A) ( ring-Commutative-Ring B) ( ring-Commutative-Ring C) ( ring-Commutative-Ring D) ( h) ( g) ( f)
Unit laws for composition of homomorphisms of commutative rings
module _ {l1 l2 : Level} (A : Commutative-Ring l1) (B : Commutative-Ring l2) (f : type-hom-Commutative-Ring A B) where left-unit-law-comp-hom-Commutative-Ring : comp-hom-Commutative-Ring A B B (id-hom-Commutative-Ring B) f ＝ f left-unit-law-comp-hom-Commutative-Ring = left-unit-law-comp-hom-Ring ( ring-Commutative-Ring A) ( ring-Commutative-Ring B) ( f) right-unit-law-comp-hom-Commutative-Ring : comp-hom-Commutative-Ring A A B f (id-hom-Commutative-Ring A) ＝ f right-unit-law-comp-hom-Commutative-Ring = right-unit-law-comp-hom-Ring ( ring-Commutative-Ring A) ( ring-Commutative-Ring B) ( f)