{-# OPTIONS --safe #-} module Cubical.Algebra.Ring.Kernel where open import Cubical.Foundations.Prelude open import Cubical.Foundations.Equiv open import Cubical.Foundations.Structure open import Cubical.Foundations.HLevels open import Cubical.Foundations.Powerset open import Cubical.Algebra.Ring.Base open import Cubical.Algebra.Ring.Properties open import Cubical.Algebra.Ring.Ideal private variable ℓ : Level module _ {R S : Ring ℓ} (f′ : RingHom R S) where open IsRingHom (f′ .snd) open RingStr ⦃...⦄ open isIdeal open RingTheory private instance _ = R _ = S _ = snd R _ = snd S f = fst f′ kernel : fst R → hProp ℓ kernel x = (f x ≡ 0r) , is-set _ _ kernelIsIdeal : isIdeal R kernel +-closed kernelIsIdeal = λ fx≡0 fy≡0 → f (_ + _) ≡⟨ pres+ _ _ ⟩ f _ + f _ ≡⟨ cong (λ u → u + f _) fx≡0 ⟩ 0r + f _ ≡⟨ cong (λ u → 0r + u) fy≡0 ⟩ 0r + 0r ≡⟨ 0Idempotent S ⟩ 0r ∎ -closed kernelIsIdeal = λ fx≡0 → f (- _) ≡⟨ pres- _ ⟩ - f _ ≡⟨ cong -_ fx≡0 ⟩ - 0r ≡⟨ 0Selfinverse S ⟩ 0r ∎ 0r-closed kernelIsIdeal = f 0r ≡⟨ pres0 ⟩ 0r ∎ ·-closedLeft kernelIsIdeal = λ r fx≡0 → f (r · _) ≡⟨ pres· _ _ ⟩ f r · f (_) ≡⟨ cong (λ u → f r · u) fx≡0 ⟩ f r · 0r ≡⟨ 0RightAnnihilates S _ ⟩ 0r ∎ ·-closedRight kernelIsIdeal = λ r fx≡0 → f (_ · r) ≡⟨ pres· _ _ ⟩ f _ · f r ≡⟨ cong (λ u → u · f r) fx≡0 ⟩ 0r · f r ≡⟨ 0LeftAnnihilates S _ ⟩ 0r ∎ kernelIdeal : IdealsIn R fst kernelIdeal = kernel snd kernelIdeal = kernelIsIdeal kernelFiber : (x y : ⟨ R ⟩) → f x ≡ f y → x - y ∈ kernel kernelFiber x y fx≡fy = f (x - y) ≡⟨ pres+ x (- y) ⟩ f x + f (- y) ≡[ i ]⟨ fx≡fy i + pres- y i ⟩ f y - f y ≡⟨ +InvR (f y) ⟩ 0r ∎