strengthen makeCommAlgebraHom

agda · Jan 19, 2024 · 75b87d7 · 75b87d7
1 parent c1b3508
commit 75b87d7
Show file tree

Hide file tree

Showing 3 changed files with 17 additions and 9 deletions.
diff --git a/Cubical/Algebra/CommAlgebra/Base.agda b/Cubical/Algebra/CommAlgebra/Base.agda
@@ -207,9 +207,9 @@ module _ {R : CommRing ℓ} where
                            → (fPres1 : f 1a ≡ 1a)
                            → (fPres+ : (x y : fst M) → f (x + y) ≡ f x + f y)
                            → (fPres· : (x y : fst M) → f (x · y) ≡ f x · f y)
-                           → (fPres⋆ : (r : fst R) (x : fst M) → f (r ⋆ x) ≡ r ⋆ f x)
+                           → (fPres⋆1a : (r : fst R) → f (r ⋆ 1a) ≡ r ⋆ 1a)
                            → CommAlgebraHom M N
-    makeCommAlgebraHom f fPres1 fPres+ fPres· fPres⋆ = f , isHom
+    makeCommAlgebraHom f fPres1 fPres+ fPres· fPres⋆1a = f , isHom
       where fPres0 =
                     f 0a                  ≡⟨ sym (+IdR _) ⟩
                     f 0a + 0a             ≡⟨ cong (λ u → f 0a + u) (sym (+InvR (f 0a))) ⟩
@@ -232,7 +232,14 @@ module _ {R : CommRing ℓ} where
                                (f ((- x) + x) - f x) ≡⟨ cong (λ u → f u - f x) (+InvL x) ⟩
                                (f 0a - f x) ≡⟨ cong (λ u → u - f x) fPres0 ⟩
                                (0a - f x) ≡⟨ +IdL _ ⟩ (- f x) ∎)
-            pres⋆ isHom = fPres⋆
+            pres⋆ isHom r y =
+              f (r ⋆ y)         ≡⟨ cong f (cong (r ⋆_) (sym (·IdL y))) ⟩
+              f (r ⋆ (1a · y))  ≡⟨ cong f (sym (⋆AssocL r 1a y)) ⟩
+              f ((r ⋆ 1a) · y)  ≡⟨ fPres· (r ⋆ 1a) y ⟩
+              f (r ⋆ 1a) · f y  ≡⟨ cong (_· f y) (fPres⋆1a r) ⟩
+              (r ⋆ 1a) · f y    ≡⟨ ⋆AssocL r 1a (f y) ⟩
+              r ⋆ (1a · f y)    ≡⟨ cong (r ⋆_) (·IdL (f y)) ⟩
+              r ⋆ f y           ∎
 
     isPropIsCommAlgebraHom : (f : fst M → fst N) → isProp (IsCommAlgebraHom (snd M) f (snd N))
     isPropIsCommAlgebraHom f = isPropIsAlgebraHom

diff --git a/Cubical/Algebra/CommAlgebra/Instances/Initial.agda b/Cubical/Algebra/CommAlgebra/Instances/Initial.agda
@@ -64,8 +64,8 @@ module _ (R : CommRing ℓ) where
                            x * (y * 1a)                   ≡[ i ]⟨ x * (·IdL (y * 1a) (~ i)) ⟩
                            x * (1a · (y * 1a))            ≡⟨ sym (⋆AssocL _ _ _) ⟩
                            (x * 1a) · (y * 1a) ∎)
-        (λ r x → (r · x) * 1a   ≡⟨ ⋆Assoc _ _ _ ⟩
-                         (r * (x * 1a)) ∎)
+        (λ r → (r · _) * 1a   ≡⟨ cong (_* 1a) (·IdR r) ⟩
+               (r * 1a) ∎)
 
     initialMapEq : (f : CommAlgebraHom initialCAlg A)
                    → f ≡ initialMap

diff --git a/Cubical/Algebra/CommAlgebra/Properties.agda b/Cubical/Algebra/CommAlgebra/Properties.agda
@@ -157,10 +157,11 @@ module CommAlgChar (R : CommRing ℓ) {ℓ' : Level} where
    instance
     _ = snd A
     _ = snd B
-   pres⋆h : ∀ r x → fst h (fst f r · x) ≡ fst g r · fst h x
-   pres⋆h r x = fst h (fst f r · x)       ≡⟨ pres· (snd h) _ _ ⟩
-                fst h (fst f r) · fst h x ≡⟨ cong (λ φ → fst φ r · fst h x) commDiag ⟩
-                fst g r · fst h x ∎
+   pres⋆h : ∀ r → fst h (fst f r · 1r) ≡ fst g r · 1r
+   pres⋆h r = fst h (fst f r · 1r)       ≡⟨ pres· (snd h) _ _ ⟩
+              fst h (fst f r) · fst h 1r ≡⟨ cong (λ φ → fst φ r · fst h 1r) commDiag ⟩
+              fst g r · fst h 1r         ≡⟨ cong (fst g r ·_) (pres1 (snd h))  ⟩
+              fst g r · 1r ∎
 
  fromCommAlgebraHom : (A B : CommAlgebra R ℓ') → CommAlgebraHom A B
                     → CommRingWithHomHom (fromCommAlg A) (fromCommAlg B)