From e3cae56b9308a6a239bab5d97fb77a97f8d19031 Mon Sep 17 00:00:00 2001 From: Felix Cherubini Date: Fri, 30 Aug 2024 17:15:01 +0200 Subject: [PATCH] add more calcualtions --- Cubical/Algebra/CommAlgebra/FP/Instances.agda | 52 +--- .../Polynomials/Typevariate/OnCoproduct.agda | 3 +- .../Polynomials/Typevariate/Properties.agda | 275 ++--------------- .../Typevariate/UniversalProperty.agda | 285 ++++++++++++++++++ 4 files changed, 312 insertions(+), 303 deletions(-) create mode 100644 Cubical/Algebra/CommRing/Instances/Polynomials/Typevariate/UniversalProperty.agda diff --git a/Cubical/Algebra/CommAlgebra/FP/Instances.agda b/Cubical/Algebra/CommAlgebra/FP/Instances.agda index 09738084d..6e3a42310 100644 --- a/Cubical/Algebra/CommAlgebra/FP/Instances.agda +++ b/Cubical/Algebra/CommAlgebra/FP/Instances.agda @@ -45,6 +45,7 @@ private module _ (R : CommRing ℓ) where open FinitePresentation + {- Every (multivariate) polynomial algebra is finitely presented -} module _ (n : ℕ) where private abstract @@ -52,7 +53,8 @@ module _ (R : CommRing ℓ) where p = sym $ 0FGIdeal≡0Ideal (Polynomials R n) compute : - CommAlgebraEquiv (Polynomials R n) $ (Polynomials R n) / ⟨ emptyFinVec ⟨ Polynomials R n ⟩ₐ ⟩[ _ ] + CommAlgebraEquiv (Polynomials R n) + ((Polynomials R n) / ⟨ emptyFinVec ⟨ Polynomials R n ⟩ₐ ⟩[ _ ]) compute = transport (λ i → CommAlgebraEquiv (Polynomials R n) ((Polynomials R n) / (p i))) $ zeroIdealQuotient (Polynomials R n) @@ -69,54 +71,6 @@ module _ (R : CommRing ℓ) where {- - {- Every (multivariate) polynomial algebra is finitely presented -} - module _ (n : ℕ) where - private - A : CommAlgebra R ℓ - A = Polynomials n - - emptyGen : FinVec (fst A) 0 - emptyGen = λ () - - B : CommAlgebra R ℓ - B = FPAlgebra n emptyGen - - polynomialAlgFP : FinitePresentation A - FinitePresentation.n polynomialAlgFP = n - m polynomialAlgFP = 0 - relations polynomialAlgFP = emptyGen - equiv polynomialAlgFP = - -- Idea: A and B enjoy the same universal property. - toAAsEquiv , snd toA - where - toA : CommAlgebraHom B A - toA = inducedHom n emptyGen A Construction.var (λ ()) - fromA : CommAlgebraHom A B - fromA = freeInducedHom B (generator _ _) - open AlgebraHoms - inverse1 : fromA ∘a toA ≡ idAlgebraHom _ - inverse1 = - fromA ∘a toA - ≡⟨ sym (unique _ _ B _ _ _ (λ i → cong (fst fromA) ( - fst toA (generator n emptyGen i) - ≡⟨ inducedHomOnGenerators _ _ _ _ _ _ ⟩ - Construction.var i - ∎))) ⟩ - inducedHom n emptyGen B (generator _ _) (relationsHold _ _) - ≡⟨ unique _ _ B _ _ _ (λ i → refl) ⟩ - idAlgebraHom _ - ∎ - inverse2 : toA ∘a fromA ≡ idAlgebraHom _ - inverse2 = isoFunInjective (homMapIso A) _ _ ( - evaluateAt A (toA ∘a fromA) ≡⟨ sym (naturalEvR {A = B} {B = A} toA fromA) ⟩ - fst toA ∘ evaluateAt B fromA ≡⟨ refl ⟩ - fst toA ∘ generator _ _ ≡⟨ funExt (inducedHomOnGenerators _ _ _ _ _)⟩ - Construction.var ∎) - toAAsEquiv : ⟨ B ⟩ ≃ ⟨ A ⟩ - toAAsEquiv = isoToEquiv (iso (fst toA) - (fst fromA) - (λ a i → fst (inverse2 i) a) - (λ b i → fst (inverse1 i) b)) {- The initial R-algebra is finitely presented -} private diff --git a/Cubical/Algebra/CommRing/Instances/Polynomials/Typevariate/OnCoproduct.agda b/Cubical/Algebra/CommRing/Instances/Polynomials/Typevariate/OnCoproduct.agda index 3290a2276..7ce31c7d2 100644 --- a/Cubical/Algebra/CommRing/Instances/Polynomials/Typevariate/OnCoproduct.agda +++ b/Cubical/Algebra/CommRing/Instances/Polynomials/Typevariate/OnCoproduct.agda @@ -17,7 +17,8 @@ open import Cubical.Data.Sum as ⊎ open import Cubical.Data.Sigma open import Cubical.Algebra.CommRing -open import Cubical.Algebra.CommRing.Instances.Polynomials.Typevariate +open import Cubical.Algebra.CommRing.Instances.Polynomials.Typevariate.Base +open import Cubical.Algebra.CommRing.Instances.Polynomials.Typevariate.UniversalProperty private variable diff --git a/Cubical/Algebra/CommRing/Instances/Polynomials/Typevariate/Properties.agda b/Cubical/Algebra/CommRing/Instances/Polynomials/Typevariate/Properties.agda index 0af77c592..bde4d50ea 100644 --- a/Cubical/Algebra/CommRing/Instances/Polynomials/Typevariate/Properties.agda +++ b/Cubical/Algebra/CommRing/Instances/Polynomials/Typevariate/Properties.agda @@ -1,18 +1,12 @@ {-# OPTIONS --safe #-} module Cubical.Algebra.CommRing.Instances.Polynomials.Typevariate.Properties where -{- - This file contains - * an elimination principle for proving some proposition for all elements of R[I]ᵣ - ('elimProp') - * definitions of the induced maps appearing in the universal property of R[I], --} open import Cubical.Foundations.Prelude open import Cubical.Foundations.Equiv open import Cubical.Foundations.Isomorphism open import Cubical.Foundations.HLevels open import Cubical.Foundations.Structure -open import Cubical.Foundations.Function hiding (const) +open import Cubical.Foundations.Function open import Cubical.Foundations.Isomorphism open import Cubical.Data.Sigma.Properties using (Σ≡Prop) @@ -20,9 +14,9 @@ open import Cubical.HITs.SetTruncation open import Cubical.Algebra.CommRing open import Cubical.Algebra.CommRing.Instances.Polynomials.Typevariate.Base -open import Cubical.Algebra.Ring.Properties +open import Cubical.Algebra.CommRing.Instances.Polynomials.Typevariate.UniversalProperty public -open import Cubical.Data.Empty +open import Cubical.Data.Empty as ⊥ open import Cubical.Data.Sigma open import Cubical.Tactics.CommRingSolver @@ -31,255 +25,30 @@ private variable ℓ ℓ' ℓ'' : Level -module _ {R : CommRing ℓ} {I : Type ℓ'} where +module _ {R : CommRing ℓ} where open CommRingStr ⦃...⦄ private instance _ = snd R - _ = snd (R [ I ]) - module C = Construction - open C using (const) + polynomialsOn⊥ : CommRingEquiv (R [ ⊥ ]) R + polynomialsOn⊥ = + isoToEquiv + (iso (to .fst) (from .fst) + (λ x → cong (λ f → f .fst x) to∘from) + (λ x → cong (λ f → f .fst x) from∘to)) , + isHom + where to : CommRingHom (R [ ⊥ ]) R + to = inducedHom R (idCommRingHom R) ⊥.rec - {- - Construction of the 'elimProp' eliminator. - -} - module _ - {P : ⟨ R [ I ] ⟩ → Type ℓ''} - (isPropP : {x : _} → isProp (P x)) - (onVar : {x : I} → P (C.var x)) - (onConst : {r : ⟨ R ⟩} → P (const r)) - (on+ : {x y : ⟨ R [ I ] ⟩} → P x → P y → P (x + y)) - (on· : {x y : ⟨ R [ I ] ⟩} → P x → P y → P (x · y)) - where + from : CommRingHom R (R [ ⊥ ]) + from = constPolynomial R ⊥ - private - on- : {x : ⟨ R [ I ] ⟩} → P x → P (- x) - on- {x} Px = subst P (minusByMult x) (on· onConst Px) - where minusByMult : (x : _) → (const (- 1r)) · x ≡ - x - minusByMult x = - (const (- 1r)) · x ≡⟨ cong (_· x) (pres- 1r) ⟩ - (- const (1r)) · x ≡⟨ cong (λ u → (- u) · x) pres1 ⟩ - (- 1r) · x ≡⟨ sym (-IsMult-1 x) ⟩ - - x ∎ - where open RingTheory (CommRing→Ring (R [ I ])) using (-IsMult-1) - open IsCommRingHom (constPolynomial R I .snd) + to∘from : to ∘cr from ≡ idCommRingHom R + to∘from = CommRingHom≡ refl - -- A helper to deal with the path constructor cases. - mkPathP : - {x0 x1 : ⟨ R [ I ] ⟩} → - (p : x0 ≡ x1) → - (Px0 : P (x0)) → - (Px1 : P (x1)) → - PathP (λ i → P (p i)) Px0 Px1 - mkPathP _ = isProp→PathP λ i → isPropP + from∘to : from ∘cr to ≡ idCommRingHom (R [ ⊥ ]) + from∘to = idByIdOnVars (from ∘cr to) refl (funExt ⊥.elim) - elimProp : ((x : _) → P x) - - elimProp (C.var _) = onVar - elimProp (const _) = onConst - elimProp (x C.+ y) = on+ (elimProp x) (elimProp y) - elimProp (C.- x) = on- (elimProp x) - elimProp (x C.· y) = on· (elimProp x) (elimProp y) - - elimProp (C.+-assoc x y z i) = - mkPathP (C.+-assoc x y z) - (on+ (elimProp x) (on+ (elimProp y) (elimProp z))) - (on+ (on+ (elimProp x) (elimProp y)) (elimProp z)) - i - elimProp (C.+-rid x i) = - mkPathP (C.+-rid x) - (on+ (elimProp x) onConst) - (elimProp x) - i - elimProp (C.+-rinv x i) = - mkPathP (C.+-rinv x) - (on+ (elimProp x) (on- (elimProp x))) - onConst - i - elimProp (C.+-comm x y i) = - mkPathP (C.+-comm x y) - (on+ (elimProp x) (elimProp y)) - (on+ (elimProp y) (elimProp x)) - i - elimProp (C.·-assoc x y z i) = - mkPathP (C.·-assoc x y z) - (on· (elimProp x) (on· (elimProp y) (elimProp z))) - (on· (on· (elimProp x) (elimProp y)) (elimProp z)) - i - elimProp (C.·-lid x i) = - mkPathP (C.·-lid x) - (on· onConst (elimProp x)) - (elimProp x) - i - elimProp (C.·-comm x y i) = - mkPathP (C.·-comm x y) - (on· (elimProp x) (elimProp y)) - (on· (elimProp y) (elimProp x)) - i - elimProp (C.ldist x y z i) = - mkPathP (C.ldist x y z) - (on· (on+ (elimProp x) (elimProp y)) (elimProp z)) - (on+ (on· (elimProp x) (elimProp z)) (on· (elimProp y) (elimProp z))) - i - elimProp (C.+HomConst s t i) = - mkPathP (C.+HomConst s t) - onConst - (on+ onConst onConst) - i - elimProp (C.·HomConst s t i) = - mkPathP (C.·HomConst s t) - onConst - (on· onConst onConst) - i - - elimProp (C.0-trunc x y p q i j) = - isOfHLevel→isOfHLevelDep 2 (λ _ → isProp→isSet isPropP) - (elimProp x) - (elimProp y) - (cong elimProp p) - (cong elimProp q) - (C.0-trunc x y p q) - i - j - - {- - Construction of the induced map. - In this module and the module below, we will show the universal property - of the polynomial ring as a commutative ring. - - R ──→ R[I] - \ ∣ - f ∃! for a given φ : I → S - ↘ ↙ - S - - -} - module _ (S : CommRing ℓ'') (f : CommRingHom R S) (φ : I → ⟨ S ⟩) where - private instance - _ = S .snd - - open IsCommRingHom - - inducedMap : ⟨ R [ I ] ⟩ → ⟨ S ⟩ - inducedMap (C.var x) = φ x - inducedMap (const r) = (f .fst r) - inducedMap (P C.+ Q) = (inducedMap P) + (inducedMap Q) - inducedMap (C.- P) = - inducedMap P - inducedMap (C.+-assoc P Q S i) = +Assoc (inducedMap P) (inducedMap Q) (inducedMap S) i - inducedMap (C.+-rid P i) = - let - eq : (inducedMap P) + (inducedMap (const 0r)) ≡ (inducedMap P) - eq = (inducedMap P) + (inducedMap (const 0r)) ≡⟨⟩ - (inducedMap P) + ((f .fst 0r)) ≡⟨ cong ((inducedMap P) +_) (pres0 (f .snd)) ⟩ - (inducedMap P) + 0r ≡⟨ +IdR _ ⟩ - (inducedMap P) ∎ - in eq i - inducedMap (C.+-rinv P i) = - let eq : (inducedMap P - inducedMap P) ≡ (inducedMap (const 0r)) - eq = (inducedMap P - inducedMap P) ≡⟨ +InvR _ ⟩ - 0r ≡⟨ sym (pres0 (f .snd)) ⟩ - (inducedMap (const 0r))∎ - in eq i - inducedMap (C.+-comm P Q i) = +Comm (inducedMap P) (inducedMap Q) i - inducedMap (P C.· Q) = inducedMap P · inducedMap Q - inducedMap (C.·-assoc P Q S i) = ·Assoc (inducedMap P) (inducedMap Q) (inducedMap S) i - inducedMap (C.·-lid P i) = - let eq = inducedMap (const 1r) · inducedMap P ≡⟨ cong (λ u → u · inducedMap P) (pres1 (f .snd)) ⟩ - 1r · inducedMap P ≡⟨ ·IdL (inducedMap P) ⟩ - inducedMap P ∎ - in eq i - inducedMap (C.·-comm P Q i) = ·Comm (inducedMap P) (inducedMap Q) i - inducedMap (C.ldist P Q S i) = ·DistL+ (inducedMap P) (inducedMap Q) (inducedMap S) i - inducedMap (C.+HomConst s t i) = pres+ (f .snd) s t i - inducedMap (C.·HomConst s t i) = pres· (f .snd) s t i - inducedMap (C.0-trunc P Q p q i j) = - is-set (inducedMap P) (inducedMap Q) (cong _ p) (cong _ q) i j - - module _ where - open IsCommRingHom - - inducedHom : CommRingHom (R [ I ]) S - inducedHom .fst = inducedMap - inducedHom .snd .pres0 = pres0 (f .snd) - inducedHom .snd .pres1 = pres1 (f. snd) - inducedHom .snd .pres+ = λ _ _ → refl - inducedHom .snd .pres· = λ _ _ → refl - inducedHom .snd .pres- = λ _ → refl - - opaque - inducedHomComm : inducedHom ∘cr constPolynomial R I ≡ f - inducedHomComm = CommRingHom≡ $ funExt (λ r → refl) - -module _ {R : CommRing ℓ} {I : Type ℓ'} (S : CommRing ℓ'') (f : CommRingHom R S) where - open CommRingStr ⦃...⦄ - private instance - _ = S .snd - _ = (R [ I ]) .snd - open IsCommRingHom - - evalVar : CommRingHom (R [ I ]) S → I → ⟨ S ⟩ - evalVar h = h .fst ∘ var - - opaque - unfolding var - evalInduce : ∀ (φ : I → ⟨ S ⟩) - → evalVar (inducedHom S f φ) ≡ φ - evalInduce φ = refl - - opaque - unfolding var - evalOnVars : ∀ (φ : I → ⟨ S ⟩) - → (i : I) → inducedHom S f φ .fst (var i) ≡ φ i - evalOnVars φ i = refl - - opaque - unfolding var - induceEval : (g : CommRingHom (R [ I ]) S) - (p : g .fst ∘ constPolynomial R I .fst ≡ f .fst) - → (inducedHom S f (evalVar g)) ≡ g - induceEval g p = - let theMap : ⟨ R [ I ] ⟩ → ⟨ S ⟩ - theMap = inducedMap S f (evalVar g) - in - CommRingHom≡ $ - funExt $ - elimProp - (is-set _ _) - (λ {x} → refl) - (λ {r} → sym (cong (λ f → f r) p)) - (λ {x} {y} eq-x eq-y → - theMap (x + y) ≡⟨ pres+ (inducedHom S f (evalVar g) .snd) x y ⟩ - theMap x + theMap y ≡[ i ]⟨ (eq-x i + eq-y i) ⟩ - (g $cr x + g $cr y) ≡⟨ sym (pres+ (g .snd) _ _) ⟩ - (g $cr (x + y)) ∎) - λ {x} {y} eq-x eq-y → - theMap (x · y) ≡⟨ pres· (inducedHom S f (evalVar g) .snd) x y ⟩ - theMap x · theMap y ≡[ i ]⟨ (eq-x i · eq-y i) ⟩ - (g $cr x · g $cr y) ≡⟨ sym (pres· (g .snd) _ _) ⟩ - (g $cr (x · y)) ∎ - - opaque - inducedHomUnique : (φ : I → ⟨ S ⟩) - (g : CommRingHom (R [ I ]) S) - (p : g .fst ∘ constPolynomial R I .fst ≡ f .fst) - (q : evalVar g ≡ φ) - → inducedHom S f φ ≡ g - inducedHomUnique φ g p q = cong (inducedHom S f) (sym q) ∙ induceEval g p - - opaque - hom≡ByValuesOnVars : (g h : CommRingHom (R [ I ]) S) - (p : g .fst ∘ constPolynomial _ _ .fst ≡ f .fst) (q : h .fst ∘ constPolynomial _ _ .fst ≡ f .fst) - → (evalVar g ≡ evalVar h) - → g ≡ h - hom≡ByValuesOnVars g h p q ≡OnVars = - sym (inducedHomUnique ϕ g p refl) ∙ inducedHomUnique ϕ h q (sym ≡OnVars) - where ϕ : I → ⟨ S ⟩ - ϕ = evalVar g - -opaque - idByIdOnVars : {R : CommRing ℓ} {I : Type ℓ'} - (g : CommRingHom (R [ I ]) (R [ I ])) - (p : g .fst ∘ constPolynomial _ _ .fst ≡ constPolynomial _ _ .fst) - → (g .fst ∘ var ≡ idfun _ ∘ var) - → g ≡ idCommRingHom (R [ I ]) - idByIdOnVars g p idOnVars = hom≡ByValuesOnVars _ (constPolynomial _ _) g (idCommRingHom _) p refl idOnVars + abstract + isHom : IsCommRingHom ((R [ ⊥ ]) .snd) (to .fst) (R .snd) + isHom = to .snd diff --git a/Cubical/Algebra/CommRing/Instances/Polynomials/Typevariate/UniversalProperty.agda b/Cubical/Algebra/CommRing/Instances/Polynomials/Typevariate/UniversalProperty.agda new file mode 100644 index 000000000..50e6aaf81 --- /dev/null +++ b/Cubical/Algebra/CommRing/Instances/Polynomials/Typevariate/UniversalProperty.agda @@ -0,0 +1,285 @@ +{-# OPTIONS --safe #-} +module Cubical.Algebra.CommRing.Instances.Polynomials.Typevariate.UniversalProperty where +{- + This file contains + * an elimination principle for proving some proposition for all elements of R[I]ᵣ + ('elimProp') + * definitions of the induced maps appearing in the universal property of R[I], +-} + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.HLevels +open import Cubical.Foundations.Structure +open import Cubical.Foundations.Function hiding (const) +open import Cubical.Foundations.Isomorphism + +open import Cubical.Data.Sigma.Properties using (Σ≡Prop) +open import Cubical.HITs.SetTruncation + +open import Cubical.Algebra.CommRing +open import Cubical.Algebra.CommRing.Instances.Polynomials.Typevariate.Base +open import Cubical.Algebra.Ring.Properties + +open import Cubical.Data.Empty +open import Cubical.Data.Sigma + +open import Cubical.Tactics.CommRingSolver + +private + variable + ℓ ℓ' ℓ'' : Level + +module _ {R : CommRing ℓ} {I : Type ℓ'} where + open CommRingStr ⦃...⦄ + private instance + _ = snd R + _ = snd (R [ I ]) + + module C = Construction + open C using (const) + + {- + Construction of the 'elimProp' eliminator. + -} + module _ + {P : ⟨ R [ I ] ⟩ → Type ℓ''} + (isPropP : {x : _} → isProp (P x)) + (onVar : {x : I} → P (C.var x)) + (onConst : {r : ⟨ R ⟩} → P (const r)) + (on+ : {x y : ⟨ R [ I ] ⟩} → P x → P y → P (x + y)) + (on· : {x y : ⟨ R [ I ] ⟩} → P x → P y → P (x · y)) + where + + private + on- : {x : ⟨ R [ I ] ⟩} → P x → P (- x) + on- {x} Px = subst P (minusByMult x) (on· onConst Px) + where minusByMult : (x : _) → (const (- 1r)) · x ≡ - x + minusByMult x = + (const (- 1r)) · x ≡⟨ cong (_· x) (pres- 1r) ⟩ + (- const (1r)) · x ≡⟨ cong (λ u → (- u) · x) pres1 ⟩ + (- 1r) · x ≡⟨ sym (-IsMult-1 x) ⟩ + - x ∎ + where open RingTheory (CommRing→Ring (R [ I ])) using (-IsMult-1) + open IsCommRingHom (constPolynomial R I .snd) + + -- A helper to deal with the path constructor cases. + mkPathP : + {x0 x1 : ⟨ R [ I ] ⟩} → + (p : x0 ≡ x1) → + (Px0 : P (x0)) → + (Px1 : P (x1)) → + PathP (λ i → P (p i)) Px0 Px1 + mkPathP _ = isProp→PathP λ i → isPropP + + elimProp : ((x : _) → P x) + + elimProp (C.var _) = onVar + elimProp (const _) = onConst + elimProp (x C.+ y) = on+ (elimProp x) (elimProp y) + elimProp (C.- x) = on- (elimProp x) + elimProp (x C.· y) = on· (elimProp x) (elimProp y) + + elimProp (C.+-assoc x y z i) = + mkPathP (C.+-assoc x y z) + (on+ (elimProp x) (on+ (elimProp y) (elimProp z))) + (on+ (on+ (elimProp x) (elimProp y)) (elimProp z)) + i + elimProp (C.+-rid x i) = + mkPathP (C.+-rid x) + (on+ (elimProp x) onConst) + (elimProp x) + i + elimProp (C.+-rinv x i) = + mkPathP (C.+-rinv x) + (on+ (elimProp x) (on- (elimProp x))) + onConst + i + elimProp (C.+-comm x y i) = + mkPathP (C.+-comm x y) + (on+ (elimProp x) (elimProp y)) + (on+ (elimProp y) (elimProp x)) + i + elimProp (C.·-assoc x y z i) = + mkPathP (C.·-assoc x y z) + (on· (elimProp x) (on· (elimProp y) (elimProp z))) + (on· (on· (elimProp x) (elimProp y)) (elimProp z)) + i + elimProp (C.·-lid x i) = + mkPathP (C.·-lid x) + (on· onConst (elimProp x)) + (elimProp x) + i + elimProp (C.·-comm x y i) = + mkPathP (C.·-comm x y) + (on· (elimProp x) (elimProp y)) + (on· (elimProp y) (elimProp x)) + i + elimProp (C.ldist x y z i) = + mkPathP (C.ldist x y z) + (on· (on+ (elimProp x) (elimProp y)) (elimProp z)) + (on+ (on· (elimProp x) (elimProp z)) (on· (elimProp y) (elimProp z))) + i + elimProp (C.+HomConst s t i) = + mkPathP (C.+HomConst s t) + onConst + (on+ onConst onConst) + i + elimProp (C.·HomConst s t i) = + mkPathP (C.·HomConst s t) + onConst + (on· onConst onConst) + i + + elimProp (C.0-trunc x y p q i j) = + isOfHLevel→isOfHLevelDep 2 (λ _ → isProp→isSet isPropP) + (elimProp x) + (elimProp y) + (cong elimProp p) + (cong elimProp q) + (C.0-trunc x y p q) + i + j + + {- + Construction of the induced map. + In this module and the module below, we will show the universal property + of the polynomial ring as a commutative ring. + + R ──→ R[I] + \ ∣ + f ∃! for a given φ : I → S + ↘ ↙ + S + + -} + module _ (S : CommRing ℓ'') (f : CommRingHom R S) (φ : I → ⟨ S ⟩) where + private instance + _ = S .snd + + open IsCommRingHom + + inducedMap : ⟨ R [ I ] ⟩ → ⟨ S ⟩ + inducedMap (C.var x) = φ x + inducedMap (const r) = (f .fst r) + inducedMap (P C.+ Q) = (inducedMap P) + (inducedMap Q) + inducedMap (C.- P) = - inducedMap P + inducedMap (C.+-assoc P Q S i) = +Assoc (inducedMap P) (inducedMap Q) (inducedMap S) i + inducedMap (C.+-rid P i) = + let + eq : (inducedMap P) + (inducedMap (const 0r)) ≡ (inducedMap P) + eq = (inducedMap P) + (inducedMap (const 0r)) ≡⟨⟩ + (inducedMap P) + ((f .fst 0r)) ≡⟨ cong ((inducedMap P) +_) (pres0 (f .snd)) ⟩ + (inducedMap P) + 0r ≡⟨ +IdR _ ⟩ + (inducedMap P) ∎ + in eq i + inducedMap (C.+-rinv P i) = + let eq : (inducedMap P - inducedMap P) ≡ (inducedMap (const 0r)) + eq = (inducedMap P - inducedMap P) ≡⟨ +InvR _ ⟩ + 0r ≡⟨ sym (pres0 (f .snd)) ⟩ + (inducedMap (const 0r))∎ + in eq i + inducedMap (C.+-comm P Q i) = +Comm (inducedMap P) (inducedMap Q) i + inducedMap (P C.· Q) = inducedMap P · inducedMap Q + inducedMap (C.·-assoc P Q S i) = ·Assoc (inducedMap P) (inducedMap Q) (inducedMap S) i + inducedMap (C.·-lid P i) = + let eq = inducedMap (const 1r) · inducedMap P ≡⟨ cong (λ u → u · inducedMap P) (pres1 (f .snd)) ⟩ + 1r · inducedMap P ≡⟨ ·IdL (inducedMap P) ⟩ + inducedMap P ∎ + in eq i + inducedMap (C.·-comm P Q i) = ·Comm (inducedMap P) (inducedMap Q) i + inducedMap (C.ldist P Q S i) = ·DistL+ (inducedMap P) (inducedMap Q) (inducedMap S) i + inducedMap (C.+HomConst s t i) = pres+ (f .snd) s t i + inducedMap (C.·HomConst s t i) = pres· (f .snd) s t i + inducedMap (C.0-trunc P Q p q i j) = + is-set (inducedMap P) (inducedMap Q) (cong _ p) (cong _ q) i j + + module _ where + open IsCommRingHom + + inducedHom : CommRingHom (R [ I ]) S + inducedHom .fst = inducedMap + inducedHom .snd .pres0 = pres0 (f .snd) + inducedHom .snd .pres1 = pres1 (f. snd) + inducedHom .snd .pres+ = λ _ _ → refl + inducedHom .snd .pres· = λ _ _ → refl + inducedHom .snd .pres- = λ _ → refl + + opaque + inducedHomComm : inducedHom ∘cr constPolynomial R I ≡ f + inducedHomComm = CommRingHom≡ $ funExt (λ r → refl) + +module _ {R : CommRing ℓ} {I : Type ℓ'} (S : CommRing ℓ'') (f : CommRingHom R S) where + open CommRingStr ⦃...⦄ + private instance + _ = S .snd + _ = (R [ I ]) .snd + open IsCommRingHom + + evalVar : CommRingHom (R [ I ]) S → I → ⟨ S ⟩ + evalVar h = h .fst ∘ var + + opaque + unfolding var + evalInduce : ∀ (φ : I → ⟨ S ⟩) + → evalVar (inducedHom S f φ) ≡ φ + evalInduce φ = refl + + opaque + unfolding var + evalOnVars : ∀ (φ : I → ⟨ S ⟩) + → (i : I) → inducedHom S f φ .fst (var i) ≡ φ i + evalOnVars φ i = refl + + opaque + unfolding var + induceEval : (g : CommRingHom (R [ I ]) S) + (p : g .fst ∘ constPolynomial R I .fst ≡ f .fst) + → (inducedHom S f (evalVar g)) ≡ g + induceEval g p = + let theMap : ⟨ R [ I ] ⟩ → ⟨ S ⟩ + theMap = inducedMap S f (evalVar g) + in + CommRingHom≡ $ + funExt $ + elimProp + (is-set _ _) + (λ {x} → refl) + (λ {r} → sym (cong (λ f → f r) p)) + (λ {x} {y} eq-x eq-y → + theMap (x + y) ≡⟨ pres+ (inducedHom S f (evalVar g) .snd) x y ⟩ + theMap x + theMap y ≡[ i ]⟨ (eq-x i + eq-y i) ⟩ + (g $cr x + g $cr y) ≡⟨ sym (pres+ (g .snd) _ _) ⟩ + (g $cr (x + y)) ∎) + λ {x} {y} eq-x eq-y → + theMap (x · y) ≡⟨ pres· (inducedHom S f (evalVar g) .snd) x y ⟩ + theMap x · theMap y ≡[ i ]⟨ (eq-x i · eq-y i) ⟩ + (g $cr x · g $cr y) ≡⟨ sym (pres· (g .snd) _ _) ⟩ + (g $cr (x · y)) ∎ + + opaque + inducedHomUnique : (φ : I → ⟨ S ⟩) + (g : CommRingHom (R [ I ]) S) + (p : g .fst ∘ constPolynomial R I .fst ≡ f .fst) + (q : evalVar g ≡ φ) + → inducedHom S f φ ≡ g + inducedHomUnique φ g p q = cong (inducedHom S f) (sym q) ∙ induceEval g p + + opaque + hom≡ByValuesOnVars : (g h : CommRingHom (R [ I ]) S) + (p : g .fst ∘ constPolynomial _ _ .fst ≡ f .fst) (q : h .fst ∘ constPolynomial _ _ .fst ≡ f .fst) + → (evalVar g ≡ evalVar h) + → g ≡ h + hom≡ByValuesOnVars g h p q ≡OnVars = + sym (inducedHomUnique ϕ g p refl) ∙ inducedHomUnique ϕ h q (sym ≡OnVars) + where ϕ : I → ⟨ S ⟩ + ϕ = evalVar g + +opaque + idByIdOnVars : {R : CommRing ℓ} {I : Type ℓ'} + (g : CommRingHom (R [ I ]) (R [ I ])) + (p : g .fst ∘ constPolynomial _ _ .fst ≡ constPolynomial _ _ .fst) + → (g .fst ∘ var ≡ idfun _ ∘ var) + → g ≡ idCommRingHom (R [ I ]) + idByIdOnVars g p idOnVars = hom≡ByValuesOnVars _ (constPolynomial _ _) g (idCommRingHom _) p refl idOnVars