The FreeCommAlgebra on a coproduct of types

Cubical/Algebra/CommAlgebra/FreeCommAlgebra/OnCoproduct.agda

@@ -0,0 +1,260 @@
+{-# 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.CommAlgebra.FreeCommAlgebra.OnCoproduct where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Equiv.BiInvertible
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Structure
+open import Cubical.Foundations.GroupoidLaws
+open import Cubical.Foundations.Structure
+
+open import Cubical.Data.Sum as ⊎
+open import Cubical.Data.Sigma
+
+open import Cubical.Algebra.Ring
+open import Cubical.Algebra.Algebra
+open import Cubical.Algebra.CommRing
+open import Cubical.Algebra.CommAlgebra
+open import Cubical.Algebra.CommAlgebra.FreeCommAlgebra
+
+private variable
+    ℓ ℓ' : Level
+
+module CalculateFreeCommAlgebraOnCoproduct (R : CommRing ℓ) (I J : Type ℓ) where
+  open Construction using (var; const)
+  open CommAlgebraStr ⦃...⦄
+
+  {-
+     We start by defining as R[I][J] and R[I⊎J] as R[I] algebras,
+     which we need later to use universal properties
+  -}
+  R[I][J]overR[I] : CommAlgebra (CommAlgebra→CommRing (R [ I ])) ℓ
+  R[I][J]overR[I] = (CommAlgebra→CommRing (R [ I ])) [ J ]
+
+  R[I][J] : CommAlgebra R ℓ
+  R[I][J] = baseChange baseRingHom R[I][J]overR[I]
+
+  ψOverR : CommAlgebraHom (R [ I ]) (R [ I ⊎ J ])
+  ψOverR = inducedHom (R [ I ⊎ J ]) (λ i → var (inl i))
+
+  ψ : CommRingHom (CommAlgebra→CommRing (R [ I ])) (CommAlgebra→CommRing (R [ I ⊎ J ]))
+  ψ = CommAlgebraHom→CommRingHom (R [ I ]) (R [ I ⊎ J ]) ψOverR
+
+  to : CommAlgebraHom (R [ I ⊎ J ]) R[I][J]
+  to = inducedHom R[I][J]
+                  (⊎.rec (λ i → const (var i))
+                         λ j → var j)
+
+  R[I⊎J]overR[I] : CommAlgebra (CommAlgebra→CommRing (R [ I ])) ℓ
+  R[I⊎J]overR[I] = Iso.inv (CommAlgChar.CommAlgIso (CommAlgebra→CommRing (R [ I ])))
+                   (CommAlgebra→CommRing (R [ I ⊎ J ]) ,
+                    ψ)
+
+  {-
+    Now we use universal properties to construct maps in both directions.
+  -}
+  open RingHoms
+  open RingStr ⦃...⦄ using (1r)
+  instance _ = snd (R [ I ])
+           _ = snd R[I⊎J]overR[I]
+           _ = snd (CommRing→Ring R)
+  module R[I] = CommAlgebraStr (snd (R [ I ]))
+  module R[I⊎J]overR[I] = CommAlgebraStr (snd R[I⊎J]overR[I])
+  module R[I⊎J] = CommAlgebraStr (snd (R [ I ⊎ J ]))
+
+  isoR = CommAlgChar.CommAlgIso R
+  isoR[I] = CommAlgChar.CommAlgIso (CommAlgebra→CommRing (R [ I ]))
+  asHomOverR[I] = Iso.fun isoR[I] R[I⊎J]overR[I]
+  asHomOverR = Iso.fun isoR (R [ I ⊎ J ])
+
+  ≡RingHoms : (x : ⟨ R ⟩) → fst (snd asHomOverR[I] ∘r baseRingHom) x ≡ fst baseRingHom x
+  ≡RingHoms x =
+    fst (snd asHomOverR[I] ∘r baseRingHom) x ≡⟨⟩
+    fst (snd asHomOverR[I]) (const x · 1a)   ≡⟨⟩
+    (const x · 1a) ⋆ 1a                      ≡⟨ cong (_⋆ 1a) (·IdR (const x)) ⟩
+    const x ⋆ 1a                             ≡⟨⟩
+    (fst ψ (const x)) · 1a                   ≡⟨⟩
+    (const x · const 1r) · 1a                ≡⟨ cong (_· 1a) (·IdR (const x)) ⟩
+    const x · 1a ∎
+
+  ≡R[I⊎J] =
+    baseChange baseRingHom R[I⊎J]overR[I]                                                     ≡⟨⟩
+    Iso.inv isoR ((CommAlgebra→CommRing R[I⊎J]overR[I]) , (snd asHomOverR[I]) ∘r baseRingHom) ≡⟨ step1 ⟩
+    Iso.inv isoR (CommAlgebra→CommRing (R [ I ⊎ J ]) , baseRingHom)                           ≡⟨⟩
+    Iso.inv isoR asHomOverR                                                                   ≡⟨ step2 ⟩
+    R [ I ⊎ J ] ∎
+    where
+      hom≡ : (snd asHomOverR[I]) ∘r baseRingHom ≡ baseRingHom
+      hom≡ = Σ≡Prop (λ _ → isPropIsRingHom _ _ _)
+                    (λ j x → ≡RingHoms x j)
+
+      step1 : Iso.inv isoR ((CommAlgebra→CommRing R[I⊎J]overR[I]) , (snd asHomOverR[I]) ∘r baseRingHom)
+              ≡ Iso.inv isoR (CommAlgebra→CommRing (R [ I ⊎ J ]) , baseRingHom)
+      step1 i = Iso.inv isoR ((CommAlgebra→CommRing R[I⊎J]overR[I]) , hom≡ i)
+
+      step2 = Iso.leftInv isoR (R [ I ⊎ J ])
+
+  fst≡R[I⊎J] : cong fst ≡R[I⊎J] ≡ refl
+  fst≡R[I⊎J] =
+    cong fst ≡R[I⊎J]    ≡⟨⟩
+    refl ∙ (refl ∙ refl) ≡⟨ sym (lUnit _) ⟩
+    refl ∙ refl          ≡⟨ sym (lUnit _) ⟩
+    refl ∎
+
+  fromOverR[I] : CommAlgebraHom R[I][J]overR[I] R[I⊎J]overR[I]
+  fromOverR[I] = inducedHom R[I⊎J]overR[I] (λ j → var (inr j))
+
+  from' : CommAlgebraHom R[I][J] (baseChange baseRingHom R[I⊎J]overR[I])
+  from' = baseChangeHom {S = R}
+                        baseRingHom
+                        R[I][J]overR[I]
+                        R[I⊎J]overR[I]
+                        fromOverR[I]
+
+  from : CommAlgebraHom R[I][J] (R [ I ⊎ J ])
+  from = subst (CommAlgebraHom R[I][J]) ≡R[I⊎J] from'
+
+
+  {-
+    Calculate, that the maps 'to' and 'from' preserve the variables/generators
+    This is needed to use universal properties, to show that to and from are
+    inverse to each other.
+  -}
+
+  incVar : (x : I ⊎ J) → ⟨ R[I][J] ⟩
+  incVar (inl i) = const (var i)
+  incVar (inr j) = var j
+
+  toOnGenerators : (x : I ⊎ J) → fst to (var x) ≡ incVar x
+  toOnGenerators (inl i) = refl
+  toOnGenerators (inr j) = refl
+
+  fromOnGenerators : (x : I ⊎ J) → fst from (incVar x) ≡ (var x)
+  fromOnGenerators (inl i) =
+    fst from (const (var i))                                                      ≡⟨⟩
+    (subst (λ X → ⟨ R[I][J] ⟩ → X) (cong fst ≡R[I⊎J]) (fst from')) (const (var i)) ≡⟨ step1 ⟩
+    (subst (λ X → ⟨ R[I][J] ⟩ → X) refl (fst from')) (const (var i))               ≡⟨ step2 ⟩
+    (fst from') (const (var i))                                                   ≡⟨⟩
+    var (inl i) · 1a                                                              ≡⟨ ·IdR _ ⟩
+    var (inl i) ∎
+      where step1 : _ ≡ _
+            step1 = cong (λ u → subst (λ X → ⟨ R[I][J] ⟩ → X) u (fst from') (const (var i))) fst≡R[I⊎J]
+            step2 : _ ≡ _
+            step2 = cong (λ u → u (const (var i)))
+                         (substRefl {B = λ (X : Type ℓ) → ⟨ R[I][J] ⟩ → X} (fst from'))
+  fromOnGenerators (inr j) =
+    fst from (var j)                                                      ≡⟨⟩
+    (subst (λ X → ⟨ R[I][J] ⟩ → X) (cong fst ≡R[I⊎J]) (fst from')) (var j) ≡⟨ step1 ⟩
+    (subst (λ X → ⟨ R[I][J] ⟩ → X) refl (fst from')) (var j)               ≡⟨ step2 ⟩
+    (fst from') (var j)                                                   ≡⟨⟩
+    (var (inr j)) ∎
+      where step1 = cong (λ u → subst (λ X → ⟨ R[I][J] ⟩ → X) u (fst from') (var j)) fst≡R[I⊎J]
+            step2 = cong (λ u → u (var j))
+                         (substRefl {B = λ (X : Type ℓ) → ⟨ R[I][J] ⟩ → X} (fst from'))
+
+  open AlgebraHoms
+  fromTo : (x : ⟨ R [ I ⊎ J ] ⟩) → fst (from ∘a to) x ≡ x
+  fromTo = isIdByUMP (from ∘a to)
+                     λ x → fst (from ∘a to) (var x) ≡⟨ cong (λ u → fst from u) (toOnGenerators x) ⟩
+                           fst from (incVar x)      ≡⟨ fromOnGenerators x ⟩
+                           var x ∎
+
+  {-
+    For 'to ∘a from', we need 'to' and 'from' as homomorphisms of R[I]-algebras.
+  -}
+
+  module _ where
+    open IsAlgebraHom
+    private
+      z = to .snd
+      instance _ = snd R[I][J]overR[I]
+               -- _ = snd R[I][J]
+               _ = snd R
+
+    toOverR[I] : CommAlgebraHom R[I⊎J]overR[I] R[I][J]overR[I]
+    toOverR[I] .fst = to .fst
+    (toOverR[I] .snd) .pres0 = z .pres0
+    (toOverR[I] .snd) .pres1 = z .pres1
+    (toOverR[I] .snd) .pres+ = z .pres+
+    (toOverR[I] .snd) .pres· = z .pres·
+    (toOverR[I] .snd) .pres- = z .pres-
+    (toOverR[I] .snd) .pres⋆ r x =
+      fst to (r ⋆ x)              ≡⟨⟩
+      fst to (fst ψ r · x)        ≡⟨ z .pres· (fst ψ r) x ⟩
+      fst to (fst ψ r) · fst to x ≡⟨ cong (_· fst to x) (to∘ψ≡const r) ⟩
+      const r · fst to x          ≡⟨⟩
+      (r ⋆ fst to x) ∎
+      where
+        {-
+          We use the UMP of R[I] on
+
+          R[I] ─ψ─→ R[I⊎J] ─to─→ R[I][J]
+             \                   /
+              \______const______/
+
+          To do that, we have to show that
+          const is an R-algebra homomorphism
+        -}
+        open Construction using (+HomConst; ·HomConst)
+        constHom : CommAlgebraHom (R [ I ]) R[I][J]
+        constHom .fst = const
+        constHom .snd =
+          makeIsAlgebraHom
+            refl
+            +HomConst
+            ·HomConst
+            λ r x →
+              const (const r · x)                                       ≡⟨ ·HomConst (const r) x ⟩
+              const (const r) · const x                                 ≡[ i ]⟨
+                                                                        const (sym (·IdR (const r)) i) · const x ⟩
+              const (const r · const 1r) · const x                      ≡[ i ]⟨
+                                                                        sym (·IdR (const (const r · const 1r))) i
+                                                                           · const x ⟩
+              (const (const r · const 1r) · const (const 1r)) · const x ≡⟨⟩
+              CommAlgebraStr._⋆_ (snd R[I][J]) r (const x) ∎
+
+        to∘ψOnVar : (i : I) → fst (to ∘a ψOverR) (var i) ≡ const (var i)
+        to∘ψOnVar i = refl
+
+        to∘ψ≡const : (x : ⟨ R [ I ] ⟩) → fst to (fst ψ x) ≡ const x
+        to∘ψ≡const =
+          equalByUMP R[I][J] (to ∘a ψOverR) constHom to∘ψOnVar
+
+
+  toFromOverR[I] : (x : ⟨ R[I][J]overR[I] ⟩) → fst (toOverR[I] ∘a fromOverR[I]) x ≡ x
+  toFromOverR[I] = isIdByUMP (toOverR[I] ∘a fromOverR[I]) λ _ → refl
+
+{- export bundled results -}
+module _ {R : CommRing ℓ} {I J : Type ℓ} where
+  open CalculateFreeCommAlgebraOnCoproduct R I J
+
+  equivFreeCommSum : CommAlgebraEquiv (R [ I ⊎ J ]) R[I][J]
+  equivFreeCommSum = (biInvEquiv→Equiv-left asBiInv) , snd to
+    where
+      open BiInvEquiv
+      asBiInv : BiInvEquiv _ _
+      fun asBiInv = fst to
+      invr asBiInv = fst fromOverR[I]
+      invr-rightInv asBiInv = toFromOverR[I]
+      invl asBiInv = fst from
+      invl-leftInv asBiInv = fromTo
+
+  equivFreeCommSumOverR[I] : CommAlgebraEquiv R[I⊎J]overR[I] R[I][J]overR[I]
+  equivFreeCommSumOverR[I] = biInvEquiv→Equiv-right asBiInv , snd toOverR[I]
+    where
+      open BiInvEquiv
+      asBiInv : BiInvEquiv _ _
+      fun asBiInv = fst toOverR[I]
+      invr asBiInv = fst fromOverR[I]
+      invr-rightInv asBiInv = toFromOverR[I]
+      invl asBiInv = fst from
+      invl-leftInv asBiInv = fromTo

Cubical/Algebra/CommAlgebra/FreeCommAlgebra/Properties.agda

@@ -352,6 +352,46 @@ Iso.leftInv (homMapIso {R = R} {I = I} A) =
   λ f → Σ≡Prop (λ f → isPropIsCommAlgebraHom {M = R [ I ]} {N = A} f)
                (Theory.homRetrievable A f)
 
+inducedHomUnique :
+  {R : CommRing ℓ} {I : Type ℓ'} (A : CommAlgebra R ℓ'') (φ : I → fst A )
+  → (f : CommAlgebraHom (R [ I ]) A) → ((i : I) → fst f (Construction.var i) ≡ φ i)
+  → f ≡ inducedHom A φ
+inducedHomUnique {I = I} A φ f p =
+  f                                            ≡⟨ sym (Iso.leftInv (homMapIso A) f) ⟩
+  inducedHom A (evaluateAt A f)                ≡⟨ ind∘ev≡ ⟩
+  inducedHom A (evaluateAt A (inducedHom A φ)) ≡⟨ Iso.leftInv (homMapIso A) _ ⟩
+  inducedHom A φ ∎
+  where ev≡ : (i : I) → evaluateAt A f i ≡ evaluateAt A (inducedHom A φ) i
+        ev≡ i = p i
+
+        ind∘ev≡ : inducedHom A (evaluateAt A f) ≡ inducedHom A (evaluateAt A (inducedHom A φ))
+        ind∘ev≡ = cong (inducedHom A) (λ j i → ev≡ i j)
+
+{- Corollary: Two homomorphisms with the same values on generators are equal -}
+equalByUMP : {R : CommRing ℓ} {I : Type ℓ'}
+           → (A : CommAlgebra R ℓ'')
+           → (f g : CommAlgebraHom (R [ I ]) A)
+           → ((i : I) → fst f (Construction.var i) ≡ fst g (Construction.var i))
+           → (x : ⟨ R [ I ] ⟩) → fst f x ≡ fst g x
+equalByUMP {R = R} {I = I} A f g p x =
+    fst f x                                                 ≡⟨ step1 ⟩
+    fst (inducedHom A (λ i → fst f (Construction.var i))) x ≡⟨ step2 ⟩
+    fst (inducedHom A (λ i → fst g (Construction.var i))) x ≡⟨ step3 ⟩
+    fst g x ∎
+    where
+      step1 = cong (λ u → fst u x) (inducedHomUnique A (λ i → fst f (Construction.var i)) f (λ _ → refl))
+      step2 : _ ≡ _
+      step2 i = fst (inducedHom A (λ j → p j i)) x
+      step3 = cong (λ u → fst u x) (sym (inducedHomUnique A (λ i → fst g (Construction.var i)) g (λ _ → refl)))
+
+{- A corollary, which is useful for constructing isomorphisms to
+   algebras with the same universal property -}
+isIdByUMP : {R : CommRing ℓ} {I : Type ℓ'}
+          → (f : CommAlgebraHom (R [ I ]) (R [ I ]))
+          → ((i : I) → fst f (Construction.var i) ≡ Construction.var i)
+          → (x : ⟨ R [ I ] ⟩) → fst f x ≡ x
+isIdByUMP {R = R} {I = I} f p = equalByUMP (R [ I ]) f (idCAlgHom (R [ I ])) p
+
 homMapPath : {R : CommRing ℓ} {I : Type ℓ'} (A : CommAlgebra R (ℓ-max ℓ ℓ'))
              → CommAlgebraHom (R [ I ]) A ≡ (I → fst A)
 homMapPath A = isoToPath (homMapIso A)
@@ -431,3 +471,7 @@ module _ {R : CommRing ℓ} where
                      isoToEquiv
                        (iso to from (λ x → isContr→isOfHLevel 1 isContr⊥→A _ _) from-to)
                in isOfHLevelRespectEquiv 0 (invEquiv equiv) isContr⊥→A
+
+module _ {R : CommRing ℓ} {I : Type ℓ} where
+  baseRingHom : CommRingHom R (CommAlgebra→CommRing (R [ I ]))
+  baseRingHom = snd (Iso.fun (CommAlgChar.CommAlgIso R) (R [ I ]))

Cubical/Algebra/CommAlgebra/Properties.agda

@@ -135,13 +135,6 @@ module CommAlgChar (R : CommRing ℓ) where
     (λ i → isPropIsCommAlgebra _ _ _ _ _ _ (CommAlgebraStr._⋆_ (AlgStrPathP i)))
     (CommAlgebraStr.isCommAlgebra (snd (toCommAlg (fromCommAlg A)))) isCommAlgebra i
 
-  CommAlgIso : Iso (CommAlgebra R ℓ) CommRingWithHom
-  fun CommAlgIso = fromCommAlg
-  inv CommAlgIso = toCommAlg
-  rightInv CommAlgIso = CommRingWithHomRoundTrip
-  leftInv CommAlgIso = CommAlgRoundTrip
-
-
  CommAlgIso : Iso (CommAlgebra R ℓ) CommRingWithHom
  fun CommAlgIso = fromCommAlg
  inv CommAlgIso = toCommAlg
@@ -365,3 +358,63 @@ module _ {R : CommRing ℓ} {A B : CommAlgebra R ℓ} where
   pres· (snd (CommAlgebraHomFromRingHom ϕ pres*)) = IsRingHom.pres· (snd ϕ)
   pres- (snd (CommAlgebraHomFromRingHom ϕ pres*)) = IsRingHom.pres- (snd ϕ)
   pres⋆ (snd (CommAlgebraHomFromRingHom ϕ pres*)) = pres*
+
+
+module _ {R S : CommRing ℓ} (f : CommRingHom S R) where
+  baseChange : CommAlgebra R ℓ → CommAlgebra S ℓ
+  baseChange A =
+    Iso.inv (CommAlgChar.CommAlgIso S) (fst asRingHom , compCommRingHom _ _ _ f (snd asRingHom))
+    where
+      asRingHom : CommAlgChar.CommRingWithHom R
+      asRingHom = Iso.fun (CommAlgChar.CommAlgIso R) A
+
+  baseChangeHom : (A B : CommAlgebra R ℓ) → CommAlgebraHom A B → CommAlgebraHom (baseChange A) (baseChange B)
+  baseChangeHom A B ϕ =
+    CommAlgChar.toCommAlgebraHom S (fst homA , snd homA ∘r f) (fst homB , snd homB ∘r f) (fst pbSliceHom) (snd pbSliceHom)
+    where open RingHoms
+          homA = Iso.fun (CommAlgChar.CommAlgIso R) A
+          homB = Iso.fun (CommAlgChar.CommAlgIso R) B
+
+          asSliceHom : Σ[ h ∈ CommRingHom (CommAlgebra→CommRing A) (CommAlgebra→CommRing B) ] h ∘r (snd homA) ≡ snd homB
+          asSliceHom = CommAlgChar.fromCommAlgebraHom R A B ϕ
+
+          pbSliceHom : Σ[ k ∈ CommRingHom (CommAlgebra→CommRing A) (CommAlgebra→CommRing B) ]
+                       k ∘r ((snd homA) ∘r f) ≡ ((snd homB) ∘r f)
+          pbSliceHom = fst asSliceHom , Σ≡Prop (λ _ → isPropIsRingHom _ _ _) λ i x → fst ((snd asSliceHom) i) (fst f x)
+
+module _ {R : CommRing ℓ} (A : CommAlgebra R ℓ) where
+  open RingHoms
+  baseChangeId : baseChange (idRingHom (CommRing→Ring R)) A ≡ A
+  baseChangeId =
+    baseChange (idRingHom (CommRing→Ring R)) A ≡⟨⟩
+    Iso.inv isoToRingHom (fst asRingHom , (snd asRingHom) ∘r id) ≡⟨ congIdComp ⟩
+    Iso.inv isoToRingHom asRingHom                               ≡⟨ useIso ⟩
+    A ∎
+    where
+      isoToRingHom = CommAlgChar.CommAlgIso R
+      id = idRingHom (CommRing→Ring R)
+      asRingHom : CommAlgChar.CommRingWithHom R
+      asRingHom = Iso.fun isoToRingHom A
+      congIdComp = λ i → Iso.inv isoToRingHom (fst asRingHom , compIdRingHom (snd asRingHom) i)
+      useIso = Iso.leftInv isoToRingHom A
+
+module _ {R S T : CommRing ℓ} (f : CommRingHom S R) (g : CommRingHom T S) where
+  open RingHoms
+  baseChangeComp : (A : CommAlgebra R ℓ)
+                 → baseChange g (baseChange f A) ≡ baseChange (f ∘r g) A
+  baseChangeComp A =
+      compAndBundle (Iso.fun isoS (Iso.inv isoS changedAasHom)) ≡⟨ cong compAndBundle (Iso.rightInv isoS changedAasHom) ⟩
+      Iso.inv isoT (fst asHomA , ((snd asHomA) ∘r f) ∘r g)      ≡⟨ congStep  ⟩
+      baseChange (compRingHom g f) A ∎
+    where
+      isoR = CommAlgChar.CommAlgIso R
+      isoS = CommAlgChar.CommAlgIso S
+      isoT = CommAlgChar.CommAlgIso T
+
+      compAndBundle : Σ[ W ∈ CommRing ℓ ] CommRingHom _ W → CommAlgebra T ℓ
+      compAndBundle (W , r) = Iso.inv isoT (W , (r ∘r g))
+      asHomA = Iso.fun isoR A
+      changedAasHom = fst asHomA , (snd asHomA) ∘r f
+
+      congStep : Iso.inv isoT (fst asHomA , ((snd asHomA) ∘r f) ∘r g) ≡ baseChange (compRingHom g f) A
+      congStep i = Iso.inv isoT (fst asHomA , sym (compAssocRingHom g f (snd asHomA)) i)