From 89ff9539e304a53431bb0d3bcfaeb050e9c9ee2f Mon Sep 17 00:00:00 2001 From: Felix Cherubini Date: Sun, 4 Aug 2024 17:32:41 +0200 Subject: [PATCH] start with OnCoproduct, change default notation for R[I] --- .../CommAlgebraAlt/Instances/Polynomials.agda | 7 +- .../Polynomials/Typevariate/Base.agda | 10 +-- .../Polynomials/Typevariate/OnCoproduct.agda | 81 +++++++++++++++++++ .../Polynomials/Typevariate/Properties.agda | 48 +++++++---- 4 files changed, 122 insertions(+), 24 deletions(-) create mode 100644 Cubical/Algebra/CommRing/Instances/Polynomials/Typevariate/OnCoproduct.agda diff --git a/Cubical/Algebra/CommAlgebraAlt/Instances/Polynomials.agda b/Cubical/Algebra/CommAlgebraAlt/Instances/Polynomials.agda index a34e78391..481aed53b 100644 --- a/Cubical/Algebra/CommAlgebraAlt/Instances/Polynomials.agda +++ b/Cubical/Algebra/CommAlgebraAlt/Instances/Polynomials.agda @@ -9,11 +9,10 @@ open import Cubical.Algebra.CommRing.Instances.Polynomials.Typevariate private variable - ℓ ℓ' : Level - -_[_] : (R : CommRing ℓ) (I : Type ℓ') → CommAlgebra R _ -R [ I ] = (R [ I ]ᵣ) , constPolynomial R I + ℓ ℓ' ℓ'' : Level +_[_]ₐ : (R : CommRing ℓ) (I : Type ℓ') → CommAlgebra R _ +R [ I ]ₐ = (R [ I ]) , constPolynomial R I {- evaluateAt : {R : CommRing ℓ} {I : Type ℓ'} (A : CommAlgebra R ℓ'') diff --git a/Cubical/Algebra/CommRing/Instances/Polynomials/Typevariate/Base.agda b/Cubical/Algebra/CommRing/Instances/Polynomials/Typevariate/Base.agda index 058e2b2c4..93c792d11 100644 --- a/Cubical/Algebra/CommRing/Instances/Polynomials/Typevariate/Base.agda +++ b/Cubical/Algebra/CommRing/Instances/Polynomials/Typevariate/Base.agda @@ -81,15 +81,15 @@ module Construction (R : CommRing ℓ) where constIsCommRingHom : (I : Type ℓ') → IsCommRingHom (R .snd) (const {I = I}) (commRingStr I) constIsCommRingHom I = makeIsCommRingHom refl +HomConst ·HomConst -_[_]ᵣ : (R : CommRing ℓ) (I : Type ℓ') → CommRing (ℓ-max ℓ ℓ') -fst (R [ I ]ᵣ) = Construction.R[_] R I -snd (R [ I ]ᵣ) = Construction.commRingStr R I +_[_] : (R : CommRing ℓ) (I : Type ℓ') → CommRing (ℓ-max ℓ ℓ') +fst (R [ I ]) = Construction.R[_] R I +snd (R [ I ]) = Construction.commRingStr R I -constPolynomial : (R : CommRing ℓ) (I : Type ℓ') → CommRingHom R (R [ I ]ᵣ) +constPolynomial : (R : CommRing ℓ) (I : Type ℓ') → CommRingHom R (R [ I ]) constPolynomial R I .fst = let open Construction R in R[_].const constPolynomial R I .snd = Construction.constIsCommRingHom R I opaque - var : {R : CommRing ℓ} {I : Type ℓ'} → I → ⟨ R [ I ]ᵣ ⟩ + var : {R : CommRing ℓ} {I : Type ℓ'} → I → ⟨ R [ I ] ⟩ var = Construction.var diff --git a/Cubical/Algebra/CommRing/Instances/Polynomials/Typevariate/OnCoproduct.agda b/Cubical/Algebra/CommRing/Instances/Polynomials/Typevariate/OnCoproduct.agda new file mode 100644 index 000000000..eea5dda7a --- /dev/null +++ b/Cubical/Algebra/CommRing/Instances/Polynomials/Typevariate/OnCoproduct.agda @@ -0,0 +1,81 @@ +{-# OPTIONS --safe #-} +{- + The goal of this module is to show that for two types I,J, there is an + isomorphism of algebras + + R[I][J] ≃ R[ I ⊎ J ] + + where '⊎' is the disjoint sum. +-} +module Cubical.Algebra.CommRing.Instances.Polynomials.Typevariate.OnCoproduct where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Function using (_∘_) +open import Cubical.Foundations.Structure using (⟨_⟩) + +open import Cubical.Data.Sum as ⊎ +open import Cubical.Data.Sigma + +open import Cubical.Algebra.CommRing +open import Cubical.Algebra.CommRing.Instances.Polynomials.Typevariate + +private + variable + ℓ ℓ' : Level + +module CalculatePolynomialsOnCoproduct (R : CommRing ℓ) (I J : Type ℓ) where + private + I→I+J : CommRingHom (R [ I ]) (R [ I ⊎ J ]) + I→I+J = inducedHom (R [ I ⊎ J ]) (constPolynomial R (I ⊎ J)) (var ∘ inl) + + to : CommRingHom ((R [ I ]) [ J ]) (R [ I ⊎ J ]) + to = inducedHom (R [ I ⊎ J ]) I→I+J (var ∘ inr) + + constPolynomialIJ : CommRingHom R ((R [ I ]) [ J ]) + constPolynomialIJ = constPolynomial _ _ ∘cr constPolynomial _ _ + + evalVarTo : to .fst ∘ var ≡ var ∘ inr + evalVarTo = evalInduce (R [ I ⊎ J ]) I→I+J (var ∘ inr) + + commConstTo : to ∘cr constPolynomialIJ ≡ constPolynomial _ _ + commConstTo = CommRingHom≡ refl + + mapVars : I ⊎ J → ⟨ (R [ I ]) [ J ] ⟩ + mapVars (inl i) = constPolynomial _ _ $cr var i + mapVars (inr j) = var j + + to∘MapVars : to .fst ∘ mapVars ≡ var + to∘MapVars = funExt λ {(inl i) → to .fst (constPolynomial _ _ $cr var i) + ≡⟨ cong (λ z → z i) (evalInduce (R [ I ⊎ J ]) (constPolynomial R (I ⊎ J)) (var ∘ inl)) ⟩ + var (inl i) ∎; + (inr j) → (to .fst (var j) ≡⟨ cong (λ z → z j) evalVarTo ⟩ var (inr j) ∎)} + + from : CommRingHom (R [ I ⊎ J ]) ((R [ I ]) [ J ]) + from = inducedHom + ((R [ I ]) [ J ]) + (constPolynomial (R [ I ]) J ∘cr constPolynomial R I) + mapVars + + evalVarFrom : from .fst ∘ var ≡ mapVars + evalVarFrom = evalInduce ((R [ I ]) [ J ]) (constPolynomial (R [ I ]) J ∘cr constPolynomial R I) mapVars + + toFrom : to ∘cr from ≡ (idCommRingHom _) + toFrom = + idByIdOnVars + (to ∘cr from) + (to .fst ∘ from .fst ∘ constPolynomial R (I ⊎ J) .fst ≡⟨⟩ + constPolynomial R (I ⊎ J) .fst ∎) + (to .fst ∘ from .fst ∘ var ≡⟨ cong (to .fst ∘_) evalVarFrom ⟩ + to .fst ∘ mapVars ≡⟨ to∘MapVars ⟩ + var ∎) +{- + fromTo : from ∘cr to ≡ (idCommRingHom _) + fromTo = + idByIdOnVars + (from ∘cr to) + (from .fst ∘ to .fst ∘ constPolynomial (R [ I ]) J .fst ≡⟨⟩ + from .fst ∘ I→I+J .fst + ≡⟨ cong fst (hom≡ByValuesOnVars ((R [ I ]) [ J ]) {!from ∘cr I→I+J!} {!I→I+J!} {!!} {!!} {!!} {!!}) ⟩ + constPolynomial (R [ I ]) J .fst ∎) + (from .fst ∘ to .fst ∘ var ≡⟨ {!!} ⟩ var ∎) +-} diff --git a/Cubical/Algebra/CommRing/Instances/Polynomials/Typevariate/Properties.agda b/Cubical/Algebra/CommRing/Instances/Polynomials/Typevariate/Properties.agda index e72120384..65675589b 100644 --- a/Cubical/Algebra/CommRing/Instances/Polynomials/Typevariate/Properties.agda +++ b/Cubical/Algebra/CommRing/Instances/Polynomials/Typevariate/Properties.agda @@ -35,7 +35,7 @@ module _ {R : CommRing ℓ} {I : Type ℓ'} where open CommRingStr ⦃...⦄ private instance _ = snd R - _ = snd (R [ I ]ᵣ) + _ = snd (R [ I ]) module C = Construction open C using (const) @@ -44,16 +44,16 @@ module _ {R : CommRing ℓ} {I : Type ℓ'} where Construction of the 'elimProp' eliminator. -} module _ - {P : ⟨ R [ I ]ᵣ ⟩ → Type ℓ''} + {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)) + (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 : ⟨ 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 = @@ -61,12 +61,12 @@ module _ {R : CommRing ℓ} {I : Type ℓ'} where (- 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) + 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 ]ᵣ ⟩} → + {x0 x1 : ⟨ R [ I ] ⟩} → (p : x0 ≡ x1) → (Px0 : P (x0)) → (Px1 : P (x1)) → @@ -160,7 +160,7 @@ module _ {R : CommRing ℓ} {I : Type ℓ'} where open IsCommRingHom - inducedMap : ⟨ R [ I ]ᵣ ⟩ → ⟨ S ⟩ + inducedMap : ⟨ R [ I ] ⟩ → ⟨ S ⟩ inducedMap (C.var x) = φ x inducedMap (const r) = (f .fst r) inducedMap (P C.+ Q) = (inducedMap P) + (inducedMap Q) @@ -198,7 +198,7 @@ module _ {R : CommRing ℓ} {I : Type ℓ'} where module _ where open IsCommRingHom - inducedHom : CommRingHom (R [ I ]ᵣ) S + inducedHom : CommRingHom (R [ I ]) S inducedHom .fst = inducedMap inducedHom .snd .pres0 = pres0 (f .snd) inducedHom .snd .pres1 = pres1 (f. snd) @@ -214,11 +214,11 @@ module _ {R : CommRing ℓ} {I : Type ℓ'} (S : CommRing ℓ'') (f : CommRingH open CommRingStr ⦃...⦄ private instance _ = S .snd - _ = (R [ I ]ᵣ) .snd + _ = (R [ I ]) .snd open IsCommRingHom - evalVar : CommRingHom (R [ I ]ᵣ) S → I → ⟨ S ⟩ - evalVar f = f .fst ∘ var + evalVar : CommRingHom (R [ I ]) S → I → ⟨ S ⟩ + evalVar h = h .fst ∘ var opaque unfolding var @@ -228,11 +228,11 @@ module _ {R : CommRing ℓ} {I : Type ℓ'} (S : CommRing ℓ'') (f : CommRingH opaque unfolding var - induceEval : (g : CommRingHom (R [ I ]ᵣ) S) + 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 ⟩ + let theMap : ⟨ R [ I ] ⟩ → ⟨ S ⟩ theMap = inducedMap S f (evalVar g) in CommRingHom≡ $ @@ -254,8 +254,26 @@ module _ {R : CommRing ℓ} {I : Type ℓ'} (S : CommRing ℓ'') (f : CommRingH opaque inducedHomUnique : (φ : I → ⟨ S ⟩) - (g : CommRingHom (R [ 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