Localization algebra (#1007)

* Add more level polymorphism for rings and algebras.

* Proper universe levels for the CommAlgebra category.

* use commAlgebraFromCommRing in toCommAlg

* Add uninferred arguments to algebra localisation.

* commAlgebraFromCommRing→CommRing

* General localisation of algebras using ring localisation.

* Add submonoids.

* Add subalgebras.

* Add induction for the localisation.

---------

Co-authored-by: Matthias Hutzler <matthias-hutzler@posteo.net>

Cubical/Algebra/Algebra/Subalgebra.agda

@@ -0,0 +1,93 @@
+{-# OPTIONS --safe #-}
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Powerset
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Structure
+
+open import Cubical.Data.Sigma
+
+open import Cubical.Algebra.Algebra
+open import Cubical.Algebra.Module.Submodule
+open import Cubical.Algebra.Monoid.Submonoid
+open import Cubical.Algebra.Ring
+
+module Cubical.Algebra.Algebra.Subalgebra
+  {ℓ ℓ' : Level}
+  (R : Ring ℓ) (A : Algebra R ℓ')
+  where
+
+open AlgebraStr (str A)
+
+record isSubalgebra (S : ℙ ⟨ A ⟩) : Type (ℓ-max ℓ ℓ') where
+  field
+    submodule : isSubmodule R (Algebra→Module A) S
+    submonoid : isSubmonoid (Algebra→MultMonoid A) S
+  open isSubmodule submodule public
+    renaming ( 0r-closed to 0a-closed )
+  open isSubmonoid submonoid public
+    renaming (ε-closed to 1a-closed)
+
+module _
+  (S : ℙ ⟨ A ⟩)
+  (+-closed : {x y : ⟨ A ⟩} → x ∈ S → y ∈ S → x + y ∈ S)
+  (0a-closed : 0a ∈ S)
+  (⋆-closed :  {x : ⟨ A ⟩} (r : ⟨ R ⟩) → x ∈ S → r ⋆ x ∈ S)
+  (1a-closed : 1a ∈ S)
+  (·-closed : {x y : ⟨ A ⟩} → (x ∈ S) → (y ∈ S) → (x · y) ∈ S)
+  where
+  private
+    module sAlg = isSubalgebra
+    module sMod = isSubmodule
+    module sMon = isSubmonoid
+
+  makeSubalgebra : isSubalgebra S
+  makeSubalgebra .sAlg.submodule .sMod.+-closed = +-closed
+  makeSubalgebra .sAlg.submodule .sMod.0r-closed = 0a-closed
+  makeSubalgebra .sAlg.submodule .sMod.⋆-closed = ⋆-closed
+  makeSubalgebra .sAlg.submonoid .sMon.ε-closed = 1a-closed
+  makeSubalgebra .sAlg.submonoid .sMon.·-closed = ·-closed
+
+Subalgebra : Type (ℓ-max ℓ (ℓ-suc ℓ'))
+Subalgebra = Σ[ S ∈ ℙ ⟨ A ⟩ ] isSubalgebra S
+
+module _ ((S , isSubalgebra) : Subalgebra) where
+  open isSubalgebra isSubalgebra
+  private module algStr = AlgebraStr
+
+  Subalgebra→Algebra≡ : {x y : Σ[ a ∈ ⟨ A ⟩ ] a ∈ S} → fst x ≡ fst y → x ≡ y
+  Subalgebra→Algebra≡ eq = Σ≡Prop (∈-isProp S) eq
+
+  Subalgebra→Algebra : Algebra R ℓ'
+  Subalgebra→Algebra .fst = Σ[ a ∈ ⟨ A ⟩ ] a ∈ S
+  Subalgebra→Algebra .snd .algStr.0a = 0a , 0a-closed
+  Subalgebra→Algebra .snd .algStr.1a = 1a , 1a-closed
+  Subalgebra→Algebra .snd .algStr._+_ (a , a∈) (b , b∈) = a + b , +-closed a∈ b∈
+  Subalgebra→Algebra .snd .algStr._·_ (a , a∈) (b , b∈) = a · b , ·-closed a∈ b∈
+  Subalgebra→Algebra .snd .algStr.-_ (a , a∈) = - a , -closed a∈
+  Subalgebra→Algebra .snd .algStr._⋆_ r (a , a∈) = r ⋆ a , ⋆-closed r a∈
+  Subalgebra→Algebra .snd .algStr.isAlgebra =
+    let
+      isSet-A' = isSetΣSndProp (isSetAlgebra A) (∈-isProp S)
+      +Assoc' = λ x y z → Subalgebra→Algebra≡ (+Assoc (fst x) (fst y) (fst z))
+      +IdR' = λ x → Subalgebra→Algebra≡ (+IdR (fst x))
+      +InvR' = λ x → Subalgebra→Algebra≡ (+InvR (fst x))
+      +Comm' = λ x y → Subalgebra→Algebra≡ (+Comm (fst x) (fst y))
+      ·Assoc' = λ x y z → Subalgebra→Algebra≡ (·Assoc (fst x) (fst y) (fst z))
+      ·IdR' = λ x → Subalgebra→Algebra≡ (·IdR (fst x))
+      ·IdL' = λ x → Subalgebra→Algebra≡ (·IdL (fst x))
+      ·DistR+' = λ x y z → Subalgebra→Algebra≡ (·DistR+ (fst x) (fst y) (fst z))
+      ·DistL+' = λ x y z → Subalgebra→Algebra≡ (·DistL+ (fst x) (fst y) (fst z))
+      ⋆Assoc' = λ r s x → Subalgebra→Algebra≡ (⋆Assoc r s (fst x))
+      ⋆DistR+' = λ r x y → Subalgebra→Algebra≡ (⋆DistR+ r (fst x) (fst y))
+      ⋆DistL+' = λ r s y → Subalgebra→Algebra≡ (⋆DistL+ r s (fst y))
+      ⋆IdL' = λ x → Subalgebra→Algebra≡ (⋆IdL (fst x))
+      ⋆AssocR' = λ r x y → Subalgebra→Algebra≡ (⋆AssocR r (fst x) (fst y))
+      ⋆AssocL' = λ r x y → Subalgebra→Algebra≡ (⋆AssocL r (fst x) (fst y))
+    in makeIsAlgebra isSet-A'
+         +Assoc' +IdR' +InvR' +Comm' ·Assoc' ·IdR' ·IdL' ·DistR+' ·DistL+'
+         ⋆Assoc' ⋆DistR+' ⋆DistL+' ⋆IdL' ⋆AssocR' ⋆AssocL'
+
+  Subalgebra→AlgebraHom : AlgebraHom Subalgebra→Algebra A
+  Subalgebra→AlgebraHom =
+    fst , makeIsAlgebraHom refl (λ x y → refl) (λ x y → refl) (λ x y → refl)

Cubical/Algebra/CommAlgebra/Base.agda

@@ -152,6 +152,20 @@ module _ {R : CommRing ℓ} where
         makeIsCommAlgebra is-set +Assoc +IdR +InvR +Comm ·Assoc ·IdL ·DistL+ ·Comm
                                     ·Assoc⋆ ⋆DistR+ ⋆DistL+ ⋆IdL ⋆AssocL
 
+      commAlgebraFromCommRing→CommRing : CommAlgebra→CommRing commAlgebraFromCommRing ≡ S
+      -- Note that this is not definitional: the proofs of the axioms might differ.
+      commAlgebraFromCommRing→CommRing i .fst  = ⟨ S ⟩
+      commAlgebraFromCommRing→CommRing i .snd .CommRingStr.0r = 0r
+      commAlgebraFromCommRing→CommRing i .snd .CommRingStr.1r = 1S
+      commAlgebraFromCommRing→CommRing i .snd .CommRingStr._+_ = _+_
+      commAlgebraFromCommRing→CommRing i .snd .CommRingStr._·_ = _·_
+      commAlgebraFromCommRing→CommRing i .snd .CommRingStr.-_ = -_
+      commAlgebraFromCommRing→CommRing i .snd .CommRingStr.isCommRing =
+        isProp→PathP (λ i → isPropIsCommRing _ _ _ _ _)
+          (CommRingStr.isCommRing (snd (CommAlgebra→CommRing commAlgebraFromCommRing)))
+          isCommRing
+          i
+
   IsCommAlgebraEquiv : {A : Type ℓ'} {B : Type ℓ''}
     (M : CommAlgebraStr R A) (e : A ≃ B) (N : CommAlgebraStr R B)
     → Type _

Cubical/Algebra/CommAlgebra/Localisation.agda

@@ -136,7 +136,7 @@ module AlgLoc (R' : CommRing ℓ)
  S⁻¹RAlgCharEquiv : (A' : CommRing ℓ) (φ : CommRingHom R' A')
                   → PathToS⁻¹R  R' S' SMultClosedSubset A' φ
                   → CommAlgebraEquiv S⁻¹RAsCommAlg (toCommAlg (A' , φ))
- S⁻¹RAlgCharEquiv A' φ cond = toCommAlgebraEquiv _ _
+ S⁻¹RAlgCharEquiv A' φ cond = toCommAlgebraEquiv (S⁻¹RAsCommRing , /1AsCommRingHom) (A' , φ)
                                 (S⁻¹RCharEquiv R' S' SMultClosedSubset A' φ cond)
                                 (RingHom≡ (S⁻¹RHasUniversalProp A' φ (cond .φS⊆Aˣ) .fst .snd))
   where open PathToS⁻¹R