small additions

agda · Aug 8, 2024 · b365c2d · b365c2d
1 parent e675105
commit b365c2d
Show file tree

Hide file tree

Showing 4 changed files with 22 additions and 6 deletions.
diff --git a/Cubical/Algebra/CommAlgebra/Properties.agda b/Cubical/Algebra/CommAlgebra/Properties.agda
@@ -31,3 +31,18 @@ module _ {R : CommRing ℓ} where
                            (f : CommAlgebraHom A B) (g : CommAlgebraHom B C) (h : CommAlgebraHom C D)
                          →  h ∘ca (g ∘ca f) ≡ (h ∘ca g) ∘ca f
     compAssocCommAlgebraHom f g h = CommAlgebraHom≡ refl
+
+  invCommAlgebraEquiv : {A B : CommAlgebra R ℓ'}
+                        → CommAlgebraEquiv A B
+                        → CommAlgebraEquiv B A
+  invCommAlgebraEquiv {A = A} {B = B} f = f⁻¹ , commutes
+    where f⁻¹ = invCommRingEquiv (CommAlgebra→CommRing A) (CommAlgebra→CommRing B) (f .fst)
+          f⁻¹∘f≡Id : f⁻¹ .fst .fst ∘ f .fst .fst .fst ≡ idfun _
+          f⁻¹∘f≡Id = funExt (secIsEq (equivIsEquiv (f⁻¹ .fst)))
+          abstract
+            commutes : (CommRingEquiv→CommRingHom f⁻¹) ∘cr B .snd ≡ A .snd
+            commutes =
+              CommRingHom≡ $
+                f⁻¹ .fst .fst ∘ B .snd .fst                     ≡⟨ sym ( cong ((f⁻¹ .fst .fst) ∘_) (cong fst (f .snd))) ⟩
+                f⁻¹ .fst .fst ∘  f .fst .fst .fst ∘ A .snd .fst ≡⟨ cong (_∘ A .snd .fst) f⁻¹∘f≡Id  ⟩
+                A .snd .fst ∎
diff --git a/Cubical/Algebra/CommAlgebra/QuotientAlgebra.agda b/Cubical/Algebra/CommAlgebra/QuotientAlgebra.agda
@@ -38,11 +38,11 @@ module _ {R : CommRing ℓ} (A : CommAlgebra R ℓ') (I : IdealsIn R A) where
     _ = A
 
   _/_ : CommAlgebra R ℓ'
-  _/_ =  ((fst A) CommRing./ I) ,
-         (CommRing.quotientHom (fst A) I ∘cr A .snd)
+  _/_ = ((fst A) CommRing./ I) ,
+        (withOpaqueStr $ (CommRing.quotientHom (fst A) I ∘cr A .snd))
 
   quotientHom : CommAlgebraHom A (_/_)
-  quotientHom = withOpaqueStr $ (CommRing.quotientHom (fst A) I) , refl
+  quotientHom = withOpaqueStr $ (CommRing.quotientHom (fst A) I) , CommRingHom≡ refl
 
 module _ {R : CommRing ℓ} (A : CommAlgebra R ℓ) (I : IdealsIn R A) where
   open CommRingStr ⦃...⦄

diff --git a/Cubical/Algebra/CommRing/Properties.agda b/Cubical/Algebra/CommRing/Properties.agda
@@ -187,7 +187,7 @@ module _ where
                  → (x y : R .fst) → f .fst .fun x ≡ f .fst .fun y → x ≡ y
   injCommRingIso f x y h = sym (f .fst .leftInv x) ∙∙ cong (f .fst .inv) h ∙∙ f .fst .leftInv y
 
-module CommRingEquivs where
+module _ where
   open RingEquivs
 
   compCommRingEquiv : {A : CommRing ℓ} {B : CommRing ℓ'} {C : CommRing ℓ''}
@@ -319,7 +319,6 @@ module CommRingTheory (R' : CommRing ℓ) where
 -- the CommRing version of uaCompEquiv
 module CommRingUAFunctoriality where
  open CommRingStr
- open CommRingEquivs
 
  CommRing≡ : (A B : CommRing ℓ) → (
    Σ[ p ∈ ⟨ A ⟩ ≡ ⟨ B ⟩ ]
@@ -369,7 +368,6 @@ module CommRingUAFunctoriality where
 
 
 
-open CommRingEquivs
 open CommRingUAFunctoriality
 recPT→CommRing : {A : Type ℓ'} (𝓕  : A → CommRing ℓ)
            → (σ : ∀ x y → CommRingEquiv (𝓕 x) (𝓕 y))

diff --git a/Cubical/Data/FinData/Base.agda b/Cubical/Data/FinData/Base.agda
@@ -76,6 +76,9 @@ rec a0 aS (suc x) = aS
 FinVec : (A : Type ℓ) (n : ℕ) → Type ℓ
 FinVec A n = Fin n → A
 
+emptyFinVec : (A : Type ℓ) → FinVec A 0
+emptyFinVec A ()
+
 replicateFinVec : (n : ℕ) → A → FinVec A n
 replicateFinVec _ a _ = a