diff --git a/Cubical/Algebra/Algebra/Properties.agda b/Cubical/Algebra/Algebra/Properties.agda index 839698bd70..cd878fd46e 100644 --- a/Cubical/Algebra/Algebra/Properties.agda +++ b/Cubical/Algebra/Algebra/Properties.agda @@ -39,13 +39,20 @@ module AlgebraTheory (R : Ring ℓ) (A : Algebra R ℓ') where open RingStr (snd R) renaming (_+_ to _+r_ ; _·_ to _·r_) open AlgebraStr (A .snd) - 0-actsNullifying : (x : ⟨ A ⟩) → 0r ⋆ x ≡ 0a - 0-actsNullifying x = + ⋆AnnihilL : (x : ⟨ A ⟩) → 0r ⋆ x ≡ 0a + ⋆AnnihilL x = let idempotent-+ = 0r ⋆ x ≡⟨ cong (λ u → u ⋆ x) (sym (RingTheory.0Idempotent R)) ⟩ (0r +r 0r) ⋆ x ≡⟨ ⋆DistL+ 0r 0r x ⟩ (0r ⋆ x) + (0r ⋆ x) ∎ in RingTheory.+Idempotency→0 (Algebra→Ring A) (0r ⋆ x) idempotent-+ + ⋆AnnihilR : (r : ⟨ R ⟩) → r ⋆ 0a ≡ 0a + ⋆AnnihilR r = RingTheory.+Idempotency→0 (Algebra→Ring A) (r ⋆ 0a) helper + where helper = + r ⋆ 0a ≡⟨ cong (λ u → r ⋆ u) (sym (RingTheory.0Idempotent (Algebra→Ring A))) ⟩ + r ⋆ (0a + 0a) ≡⟨ ⋆DistR+ r 0a 0a ⟩ + (r ⋆ 0a) + (r ⋆ 0a) ∎ + ⋆Dist· : (x y : ⟨ R ⟩) (a b : ⟨ A ⟩) → (x ·r y) ⋆ (a · b) ≡ (x ⋆ a) · (y ⋆ b) ⋆Dist· x y a b = (x ·r y) ⋆ (a · b) ≡⟨ ⋆AssocR _ _ _ ⟩ a · ((x ·r y) ⋆ b) ≡⟨ cong (a ·_) (⋆Assoc _ _ _) ⟩ diff --git a/Cubical/Algebra/CommAlgebra/FreeCommAlgebra/Properties.agda b/Cubical/Algebra/CommAlgebra/FreeCommAlgebra/Properties.agda index c80a092cc0..90c2ea32e8 100644 --- a/Cubical/Algebra/CommAlgebra/FreeCommAlgebra/Properties.agda +++ b/Cubical/Algebra/CommAlgebra/FreeCommAlgebra/Properties.agda @@ -38,7 +38,7 @@ module Theory {R : CommRing ℓ} {I : Type ℓ'} where open Construction using (var; const) renaming (_+_ to _+c_; -_ to -c_; _·_ to _·c_) imageOf0Works : 0r ⋆ 1a ≡ 0a - imageOf0Works = 0-actsNullifying 1a + imageOf0Works = ⋆AnnihilL 1a imageOf1Works : 1r ⋆ 1a ≡ 1a imageOf1Works = ⋆IdL 1a @@ -91,7 +91,7 @@ module Theory {R : CommRing ℓ} {I : Type ℓ'} where inducedHom : CommAlgebraHom (R [ I ]) A inducedHom .fst = inducedMap - inducedHom .snd .pres0 = 0-actsNullifying _ + inducedHom .snd .pres0 = ⋆AnnihilL _ inducedHom .snd .pres1 = imageOf1Works inducedHom .snd .pres+ x y = refl inducedHom .snd .pres· x y = refl diff --git a/Cubical/Algebra/CommAlgebra/UnivariatePolyList.agda b/Cubical/Algebra/CommAlgebra/UnivariatePolyList.agda index f0011a1770..0e6d95cf28 100644 --- a/Cubical/Algebra/CommAlgebra/UnivariatePolyList.agda +++ b/Cubical/Algebra/CommAlgebra/UnivariatePolyList.agda @@ -2,29 +2,224 @@ module Cubical.Algebra.CommAlgebra.UnivariatePolyList where open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Structure open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.Equiv + +open import Cubical.Data.Sigma open import Cubical.Algebra.Ring open import Cubical.Algebra.CommRing +open import Cubical.Algebra.AbGroup open import Cubical.Algebra.CommAlgebra +open import Cubical.Algebra.Algebra open import Cubical.Algebra.CommRing.Instances.Polynomials.UnivariatePolyList open import Cubical.Algebra.Polynomials.UnivariateList.Base open import Cubical.Algebra.Polynomials.UnivariateList.Properties +open import Cubical.Tactics.CommRingSolver.Reflection + private variable - ℓ : Level + ℓ ℓ' : Level module _ (R : CommRing ℓ) where - open CommRingStr ⦃...⦄ + open RingStr ⦃...⦄ -- Not CommRingStr, so it can be used together with AlgebraStr open PolyModTheory R private ListPoly = UnivariatePolyList R instance - _ = snd ListPoly - _ = snd R + _ = snd (CommRing→Ring ListPoly) + _ = snd (CommRing→Ring R) ListPolyCommAlgebra : CommAlgebra R ℓ ListPolyCommAlgebra = Iso.inv (CommAlgChar.CommAlgIso R) (ListPoly , constantPolynomialHom R) + + {- Universal Property -} + module _ (A : Algebra (CommRing→Ring R) ℓ') where + open AlgebraStr ⦃...⦄ using (_⋆_; 0a; 1a; ⋆IdL; ⋆DistL+; ⋆DistR+; ⋆AssocL; ⋆AssocR; ⋆Assoc) + private instance + _ = snd A + _ = snd (Algebra→Ring A) + _ = snd (CommAlgebra→Algebra ListPolyCommAlgebra) + private + X : ⟨ ListPolyCommAlgebra ⟩ + X = 0r ∷ 1r ∷ [] + + module _ (x : ⟨ A ⟩) where + open AlgebraTheory using (⋆AnnihilL; ⋆AnnihilR) + open RingTheory using (0RightAnnihilates; 0LeftAnnihilates) + open AbGroupTheory using (comm-4) + open PolyMod using (ElimProp; elimProp2; isSetPoly) + + + inducedMap : ⟨ ListPolyCommAlgebra ⟩ → ⟨ A ⟩ + inducedMap [] = 0a + inducedMap (a ∷ p) = a ⋆ 1a + (x · inducedMap p) + inducedMap (drop0 i) = eq i + where + eq = 0r ⋆ 1a + (x · 0a) ≡[ i ]⟨ ⋆AnnihilL (CommRing→Ring R) A 1a i + (x · 0a) ⟩ + 0a + (x · 0a) ≡⟨ +IdL (x · 0a) ⟩ + x · 0a ≡⟨ 0RightAnnihilates (Algebra→Ring A) x ⟩ + 0a ∎ + + private + ϕ = inducedMap + inducedMap1 : ϕ (1r ∷ []) ≡ 1a + inducedMap1 = + ϕ [ 1r ] ≡⟨⟩ + 1r ⋆ 1a + (x · 0a) ≡[ i ]⟨ ⋆IdL 1a i + 0RightAnnihilates (Algebra→Ring A) x i ⟩ + 1a + 0a ≡⟨ +IdR 1a ⟩ + 1a ∎ + + inducedMapPolyConst⋆ : (r : ⟨ R ⟩) (p : _) → ϕ (r PolyConst* p) ≡ r ⋆ ϕ p + inducedMapPolyConst⋆ r = + ElimProp R + (λ p → ϕ (r PolyConst* p) ≡ r ⋆ ϕ p) + (ϕ (r PolyConst* []) ≡⟨⟩ + ϕ [] ≡⟨⟩ + 0a ≡⟨ sym (⋆AnnihilR (CommRing→Ring R) A r) ⟩ + r ⋆ 0a ∎) + (λ s p IH → + ϕ (r PolyConst* (s ∷ p)) ≡⟨⟩ + ϕ ((r · s) ∷ (r PolyConst* p)) ≡⟨⟩ + (r · s) ⋆ 1a + x · ϕ (r PolyConst* p) ≡[ i ]⟨ ⋆Assoc r s 1a i + x · IH i ⟩ + r ⋆ (s ⋆ 1a) + x · (r ⋆ ϕ p) ≡⟨ step s p ⟩ + r ⋆ (s ⋆ 1a) + r ⋆ (x · ϕ p) ≡⟨ sym (⋆DistR+ r (s ⋆ 1a) (x · ϕ p)) ⟩ + r ⋆ (s ⋆ 1a + x · ϕ p) ≡⟨⟩ + r ⋆ ϕ (s ∷ p) ∎) + (is-set _ _) + where + step : (s : ⟨ R ⟩) (p : _) → _ ≡ _ + step s p i = r ⋆ (s ⋆ 1a) + sym (⋆AssocR r x (ϕ p)) i + + inducedMap⋆ : (r : ⟨ R ⟩) (p : _) → ϕ (r ⋆ p) ≡ r ⋆ ϕ p + inducedMap⋆ r p = + ϕ (r ⋆ p) ≡⟨ cong ϕ (sym (PolyConst*≡Poly* r p)) ⟩ + ϕ (r PolyConst* p) ≡⟨ inducedMapPolyConst⋆ r p ⟩ + r ⋆ ϕ p ∎ + + inducedMap+ : (p q : _) → ϕ (p + q) ≡ ϕ p + ϕ q + inducedMap+ = + elimProp2 R + (λ x y → ϕ (x + y) ≡ ϕ x + ϕ y) + (0a ≡⟨ sym (+IdR _) ⟩ 0a + 0a ∎) + (λ r p _ → + ϕ ((r ∷ p) + []) ≡⟨⟩ + ϕ (r ∷ p) ≡⟨ sym (+IdR _) ⟩ + (ϕ (r ∷ p) + 0a) ∎) + (λ s q _ → + ϕ ([] + (s ∷ q)) ≡⟨⟩ + ϕ (s ∷ q) ≡⟨ sym (+IdL _) ⟩ + 0a + ϕ (s ∷ q) ∎) + (λ r s p q IH → + ϕ ((r ∷ p) + (s ∷ q)) ≡⟨⟩ + ϕ (r + s ∷ p + q) ≡⟨⟩ + (r + s) ⋆ 1a + x · ϕ (p + q) ≡[ i ]⟨ (r + s) ⋆ 1a + x · IH i ⟩ + (r + s) ⋆ 1a + (x · (ϕ p + ϕ q)) ≡[ i ]⟨ step1 r s p q i ⟩ + (r ⋆ 1a + s ⋆ 1a) + (x · ϕ p + x · ϕ q) ≡⟨ comm-4 (Algebra→AbGroup A) _ _ _ _ ⟩ + (r ⋆ 1a + x · ϕ p) + (s ⋆ 1a + x · ϕ q) ≡⟨⟩ + ϕ (r ∷ p) + ϕ (s ∷ q) ∎) + (is-set _ _) + where step1 : (r s : ⟨ R ⟩) (p q : _) → _ ≡ _ + step1 r s p q i = ⋆DistL+ r s 1a i + ·DistR+ x (ϕ p) (ϕ q) i + M = (AbGroup→CommMonoid (Algebra→AbGroup A)) + + inducedMap· : (p q : _) → ϕ (p · q) ≡ ϕ p · ϕ q + inducedMap· p q = + ElimProp R + (λ p → ϕ (p · q) ≡ ϕ p · ϕ q) + (ϕ ([] · q) ≡⟨⟩ + ϕ [] ≡⟨⟩ + 0a ≡⟨ sym (0LeftAnnihilates (Algebra→Ring A) _) ⟩ + 0a · ϕ q ∎) + (λ r p IH → + ϕ ((r ∷ p) · q) ≡⟨⟩ + ϕ ((r PolyConst* q) + (0r ∷ (p · q))) ≡⟨ step1 r p ⟩ + ϕ (r PolyConst* q) + ϕ (0r ∷ (p · q)) ≡⟨ step2 r p ⟩ + ϕ (r ⋆ q) + ϕ (0r ∷ (p · q)) ≡⟨ step3 r p ⟩ + r ⋆ ϕ q + ϕ (0r ∷ (p · q)) ≡⟨ step4 r p ⟩ + r ⋆ ϕ q + (0a + x · ϕ (p · q)) ≡⟨ step5 r p ⟩ + r ⋆ ϕ q + x · ϕ (p · q) ≡⟨ step6 r p IH ⟩ + r ⋆ ϕ q + x · (ϕ p · ϕ q) ≡⟨ step7 r p ⟩ + r ⋆ (1a · ϕ q) + (x · ϕ p) · ϕ q ≡⟨ step8 r p ⟩ + (r ⋆ 1a) · ϕ q + (x · ϕ p) · ϕ q ≡⟨ sym (·DistL+ _ _ _) ⟩ + (r ⋆ 1a + x · ϕ p) · ϕ q ≡⟨⟩ + ϕ (r ∷ p) · ϕ q ∎) + (is-set _ _) p + where + step1 : (r : ⟨ R ⟩) (p : _) → _ ≡ _ + step1 r p = inducedMap+ (r PolyConst* q) (0r ∷ (p Poly* q)) + + step2 : (r : ⟨ R ⟩) (p : _) → _ ≡ _ + step2 r p i = ϕ (PolyConst*≡Poly* r q i) + ϕ (0r ∷ (p Poly* q)) + + step3 : (r : ⟨ R ⟩) (p : _) → _ ≡ _ + step3 r p i = inducedMap⋆ r q i + ϕ (0r ∷ (p Poly* q)) + + step4 : (r : ⟨ R ⟩) (p : _) → _ ≡ _ + step4 r p i = r ⋆ ϕ q + (⋆AnnihilL (CommRing→Ring R) A 1a i + x · ϕ (p · q)) + + step5 : (r : ⟨ R ⟩) (p : _) → _ ≡ _ + step5 r p i = r ⋆ ϕ q + +IdL (x · ϕ (p · q)) i + + step6 : (r : ⟨ R ⟩) (p : _) → _ → _ ≡ _ + step6 r p IH i = r ⋆ ϕ q + x · IH i + + step7 : (r : ⟨ R ⟩) (p : _) → _ ≡ _ + step7 r p i = r ⋆ (sym (·IdL (ϕ q)) i) + ·Assoc x (ϕ p) (ϕ q) i + + step8 : (r : ⟨ R ⟩) (p : _) → _ ≡ _ + step8 r p i = sym (⋆AssocL r 1a (ϕ q)) i + (x · ϕ p) · ϕ q + + inducedHom : AlgebraHom (CommAlgebra→Algebra ListPolyCommAlgebra) A + fst inducedHom = inducedMap + snd inducedHom = makeIsAlgebraHom inducedMap1 inducedMap+ inducedMap· inducedMap⋆ + + inducedMapGenerator : ϕ X ≡ x + inducedMapGenerator = + 0r ⋆ 1a + (x · ϕ (1r ∷ [])) ≡[ i ]⟨ ⋆AnnihilL + (CommRing→Ring R) A 1a i + (x · ϕ (1r ∷ [])) ⟩ + 0a + (x · ϕ (1r ∷ [])) ≡⟨ +IdL _ ⟩ + x · ϕ (1r ∷ []) ≡[ i ]⟨ x · inducedMap1 i ⟩ + x · 1a ≡⟨ ·IdR _ ⟩ + x ∎ + + {- Uniqueness -} + inducedHomUnique : (f : AlgebraHom (CommAlgebra→Algebra ListPolyCommAlgebra) A) + → fst f X ≡ x + → f ≡ inducedHom + inducedHomUnique f fX≡x = + Σ≡Prop + (λ _ → isPropIsAlgebraHom _ _ _ _) + λ i p → pwEq p i + where + open IsAlgebraHom (snd f) + pwEq : (p : ⟨ ListPolyCommAlgebra ⟩) → fst f p ≡ fst inducedHom p + pwEq = + ElimProp R + (λ p → fst f p ≡ fst inducedHom p) + pres0 + (λ r p IH → + fst f (r ∷ p) ≡[ i ]⟨ fst f ((sym (+IdR r) i) ∷ sym (Poly+Lid p) i) ⟩ + fst f ([ r ] + (0r ∷ p)) ≡[ i ]⟨ fst f ([ useSolver r i ] + sym (X*Poly p) i) ⟩ + fst f (r ⋆ 1a + X · p) ≡⟨ pres+ (r ⋆ 1a) (X · p) ⟩ + fst f (r ⋆ 1a) + fst f (X · p) ≡[ i ]⟨ pres⋆ r 1a i + pres· X p i ⟩ + r ⋆ fst f 1a + fst f X · fst f p ≡[ i ]⟨ r ⋆ pres1 i + fX≡x i · fst f p ⟩ + r ⋆ 1a + x · fst f p ≡[ i ]⟨ r ⋆ 1a + (x · IH i) ⟩ + r ⋆ 1a + x · inducedMap p ≡⟨⟩ + inducedMap (r ∷ p) ∎) + (is-set _ _) + where + useSolver : (r : ⟨ R ⟩) → r ≡ (r · 1r) + 0r + useSolver = solve R + + {- Reforumlation in terms of the R-AlgebraHom from R[X] to A -} + indcuedHomEquivalence : AlgebraHom (CommAlgebra→Algebra ListPolyCommAlgebra) A ≃ ⟨ A ⟩ + fst indcuedHomEquivalence f = fst f X + fst (fst (equiv-proof (snd indcuedHomEquivalence) x)) = inducedHom x + snd (fst (equiv-proof (snd indcuedHomEquivalence) x)) = inducedMapGenerator x + snd (equiv-proof (snd indcuedHomEquivalence) x) (g , gX≡x) = + Σ≡Prop (λ _ → isSetAlgebra A _ _) (sym (inducedHomUnique x g gX≡x)) diff --git a/Cubical/Algebra/Polynomials/UnivariateList/Base.agda b/Cubical/Algebra/Polynomials/UnivariateList/Base.agda index 27dc67f987..402fa47adf 100644 --- a/Cubical/Algebra/Polynomials/UnivariateList/Base.agda +++ b/Cubical/Algebra/Polynomials/UnivariateList/Base.agda @@ -1,7 +1,7 @@ {-# OPTIONS --safe #-} module Cubical.Algebra.Polynomials.UnivariateList.Base where -{-A +{- Polynomials over commutative rings ================================== -} @@ -62,18 +62,32 @@ module PolyMod (R' : CommRing ℓ) where f (x ∷ p) = cons* x p (f p) f (drop0 i) = drop0* i - -- Given a proposition (as type) ϕ ranging over polynomials, we prove it by: -- ElimProp.f ϕ ⌜proof for base case []⌝ ⌜proof for induction case a ∷ p⌝ -- ⌜proof that ϕ actually is a proposition over the domain of polynomials⌝ module _ (B : Poly R' → Type ℓ') - ([]* : B []) - (cons* : (r : R) (p : Poly R') (b : B p) → B (r ∷ p)) - (BProp : {p : Poly R'} → isProp (B p)) where + ([]* : B []) + (cons* : (r : R) (p : Poly R') (b : B p) → B (r ∷ p)) + (BProp : {p : Poly R'} → isProp (B p)) where ElimProp : (p : Poly R') → B p ElimProp = Elim.f B []* cons* (toPathP (BProp (transport (λ i → B (drop0 i)) (cons* 0r [] []*)) []*)) + module _ (B : Poly R' → Poly R' → Type ℓ') + ([][]* : B [] []) + (cons[]* : (r : R) (p : Poly R') (b : B p []) → B (r ∷ p) []) + ([]cons* : (r : R) (p : Poly R') (b : B [] p) → B [] (r ∷ p)) + (conscons* : (r s : R) (p q : Poly R') (b : B p q) → B (r ∷ p) (s ∷ q)) + (BProp : {p q : Poly R'} → isProp (B p q)) where + + elimProp2 : (p q : Poly R') → B p q + elimProp2 = + ElimProp + (λ p → (q : Poly R') → B p q) + (ElimProp (B []) [][]* (λ r p b → []cons* r p b) BProp) + (λ r p b → ElimProp (λ q → B (r ∷ p) q) (cons[]* r p (b [])) (λ s q b' → conscons* r s p q (b q)) BProp) + (isPropΠ (λ _ → BProp)) + module Rec (B : Type ℓ') ([]* : B) (cons* : R → B → B) diff --git a/Cubical/Algebra/Polynomials/UnivariateList/Properties.agda b/Cubical/Algebra/Polynomials/UnivariateList/Properties.agda index 2cc55a3872..373d4320d9 100644 --- a/Cubical/Algebra/Polynomials/UnivariateList/Properties.agda +++ b/Cubical/Algebra/Polynomials/UnivariateList/Properties.agda @@ -228,6 +228,17 @@ module PolyModTheory (R' : CommRing ℓ) where (r PolyConst* [ s ]) Poly+ [] ≡⟨ Poly+Rid _ ⟩ [ r · s ] ∎ + PolyConst*≡Poly* : (r : R) (x : Poly R') → r PolyConst* x ≡ [ r ] Poly* x + PolyConst*≡Poly* r = + ElimProp + (λ x → (r PolyConst* x) ≡ ([ r ] Poly* x)) + (sym drop0) + (λ s x IH → + r PolyConst* (s ∷ x) ≡⟨⟩ + (r PolyConst* (s ∷ x)) Poly+ [] ≡[ i ]⟨ (r PolyConst* (s ∷ x)) Poly+ (sym drop0 i) ⟩ + (r PolyConst* (s ∷ x)) Poly+ (0r ∷ []) ≡⟨⟩ + [ r ] Poly* (s ∷ x) ∎) + (isSetPoly _ _) -- For any polynomial p we have: p Poly* [ 1r ] = p Poly*Lid : ∀ q → 1P Poly* q ≡ q @@ -246,6 +257,29 @@ module PolyModTheory (R' : CommRing ℓ) where r ∷ p ∎ + + X*Poly : (p : Poly R') → (0r ∷ 1r ∷ []) Poly* p ≡ 0r ∷ p + X*Poly = + ElimProp (λ p → (0r ∷ 1r ∷ []) Poly* p ≡ 0r ∷ p) + ((0r ∷ [ 1r ]) Poly* [] ≡⟨ (0PLeftAnnihilates (0r ∷ [ 1r ])) ⟩ + [] ≡⟨ sym drop0 ⟩ + [ 0r ] ∎) + (λ r p _ → + (0r ∷ [ 1r ]) Poly* (r ∷ p) ≡⟨⟩ + (0r PolyConst* (r ∷ p)) Poly+ (0r ∷ ([ 1r ] Poly* (r ∷ p))) ≡⟨ step r p ⟩ + [ 0r ] Poly+ (0r ∷ ([ 1r ] Poly* (r ∷ p))) ≡⟨ step2 r p ⟩ + [] Poly+ (0r ∷ (r ∷ p)) ≡⟨⟩ + 0r ∷ r ∷ p ∎) + (isSetPoly _ _) + + where + step : (r : _) → (p : _) → _ ≡ _ + step r p i = (0rLeftAnnihilatesPoly (r ∷ p) i) Poly+ (0r ∷ ([ 1r ] Poly* (r ∷ p))) + + step2 : (r : _) → (p : _) → _ ≡ _ + step2 r p i = drop0 i Poly+ (0r ∷ Poly*Lid (r ∷ p) i) + + -- Distribution of indeterminate: (p + q)x = px + qx XLDistrPoly+ : ∀ p q → (0r ∷ (p Poly+ q)) ≡ ((0r ∷ p) Poly+ (0r ∷ q)) XLDistrPoly+ = diff --git a/Cubical/Algebra/Polynomials/UnivariateList/UniversalProperty.agda b/Cubical/Algebra/Polynomials/UnivariateList/UniversalProperty.agda new file mode 100644 index 0000000000..a4167cfcfd --- /dev/null +++ b/Cubical/Algebra/Polynomials/UnivariateList/UniversalProperty.agda @@ -0,0 +1,8 @@ +{-# OPTIONS --safe #-} +module Cubical.Algebra.Polynomials.UnivariateList.UniversalProperty where + +{- + Export an CommAlgebra-Instance for the UnivariateList-Polynomials. + Also export the universal property with respect to not-necessarily commutative algebras. +-} +open import Cubical.Algebra.CommAlgebra.UnivariatePolyList public