Add direct sum

Cubical/Algebra/AbGroup/Instances/Direct-Sum.agda

@@ -0,0 +1,23 @@
+{-# OPTIONS --safe #-}
+module Cubical.Algebra.AbGroup.Instances.Direct-Sum where
+
+open import Cubical.Foundations.Prelude
+
+open import Cubical.Algebra.AbGroup
+
+open import Cubical.Algebra.Direct-Sum.Base
+open import Cubical.Algebra.Direct-Sum.Properties
+
+private variable
+  ℓ : Level
+
+module _ (Idx : Type ℓ) (P : Idx → Type ℓ) (AGP : (r : Idx) → AbGroupStr (P r)) where
+
+  open AbGroupStr
+
+  ⊕-AbGr : AbGroup ℓ
+  fst ⊕-AbGr = ⊕ Idx P AGP
+  0g (snd ⊕-AbGr) = neutral
+  _+_ (snd ⊕-AbGr) = _add_
+  - snd ⊕-AbGr = inv Idx P AGP
+  isAbGroup (snd ⊕-AbGr) = makeIsAbGroup trunc addAssoc addRid (rinv Idx P AGP) addComm

Cubical/Algebra/Direct-Sum/Base.agda

@@ -0,0 +1,119 @@
+{-# OPTIONS --safe #-}
+module Cubical.Algebra.Direct-Sum.Base where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+
+open import Cubical.Algebra.AbGroup
+
+
+-- Conventions :
+-- Elements of the index are named r, s, t...
+-- Elements of the groups are called a, b, c...
+-- Elements of the direct sum are named x, y, z...
+-- Elements in the fiber of Q x, Q y are called xs, ys...
+
+
+private variable
+  ℓ ℓ' : Level
+
+
+data ⊕ (Idx : Type ℓ) (P : Idx → Type ℓ) (AGP : (r : Idx) → AbGroupStr (P r)) : Type ℓ  where
+  -- elements
+  neutral      : ⊕ Idx P AGP
+  base         : (r : Idx) → (P r) → ⊕ Idx P AGP
+  _add_        : ⊕ Idx P AGP → ⊕ Idx P AGP → ⊕ Idx P AGP
+  -- eq group
+  addAssoc     : (x y z : ⊕ Idx P AGP) → x add (y add z) ≡ (x add y) add z
+  addRid       : (x : ⊕ Idx P AGP)     → x add neutral ≡ x
+  addComm      : (x y : ⊕ Idx P AGP)   → x add y ≡ y add x
+  -- eq base
+  base-neutral : (r : Idx)                → base r (AbGroupStr.0g (AGP r)) ≡ neutral
+  base-add     : (r : Idx) → (a b : P r) → (base r a) add (base r b) ≡ base r (AbGroupStr._+_ (AGP r) a b)
+  -- set
+  trunc        : isSet (⊕ Idx P AGP)
+
+
+
+module _ (Idx : Type ℓ) (P : Idx → Type ℓ) (AGP : (r : Idx) → AbGroupStr (P r)) where
+
+  module DS-Ind-Set
+    (Q            : (x : ⊕ Idx P AGP) → Type ℓ')
+    (issd         : (x : ⊕ Idx P AGP) → isSet (Q x))
+    -- elements
+    (neutral*     : Q neutral)
+    (base*        : (r : Idx) → (a : P r) → Q (base r a))
+    (_add*_       : {x y : ⊕ Idx P AGP} → Q x → Q y → Q (x add y))
+    -- eq group
+    (addAssoc*    : {x y z : ⊕ Idx P AGP} → (xs : Q x) → (ys : Q y) → (zs : Q z)
+                    → PathP ( λ i →  Q ( addAssoc x y z i)) (xs add* (ys add* zs)) ((xs add* ys) add* zs))
+    (addRid*      : {x : ⊕ Idx P AGP} → (xs : Q x)
+                    → PathP (λ i → Q (addRid x i)) (xs add* neutral*) xs )
+    (addComm*     : {x y : ⊕ Idx P AGP} → (xs : Q x) → (ys : Q y)
+                    → PathP (λ i → Q (addComm x y i)) (xs add* ys) (ys add* xs))
+    -- -- eq base
+    (base-neutral* : (r : Idx)
+                     → PathP (λ i → Q (base-neutral r i)) (base* r (AbGroupStr.0g (AGP r))) neutral*)
+    (base-add*     : (r : Idx) → (a b : P r)
+                     → PathP (λ i → Q (base-add r a b i)) ((base* r a) add* (base* r b)) (base* r (AbGroupStr._+_ (AGP r) a b)))
+    where
+
+    f : (x : ⊕ Idx P AGP) → Q x
+    f neutral    = neutral*
+    f (base r a) = base* r a
+    f (x add y)  = (f x) add* (f y)
+    f (addAssoc x y z i)  = addAssoc* (f x) (f y) (f z) i
+    f (addRid x i)        = addRid* (f x) i
+    f (addComm x y i)     = addComm* (f x) (f y) i
+    f (base-neutral r i)  = base-neutral* r i
+    f (base-add r a b i)  = base-add* r a b i
+    f (trunc x y p q i j) = isOfHLevel→isOfHLevelDep 2 (issd)  (f x) (f y) (cong f p) (cong f q) (trunc x y p q) i j
+
+
+  module DS-Rec-Set
+    (B : Type ℓ')
+    (iss : isSet(B))
+    (neutral* : B)
+    (base*    : (r : Idx) → P r → B)
+    (_add*_   : B → B → B)
+    (addAssoc*     : (xs ys zs : B) → (xs add* (ys add* zs)) ≡ ((xs add* ys) add* zs))
+    (addRid*       : (xs : B)       → xs add* neutral* ≡ xs)
+    (addComm*      : (xs ys : B)    → xs add* ys ≡ ys add* xs)
+    (base-neutral* : (r : Idx)                → base* r (AbGroupStr.0g (AGP r)) ≡ neutral*)
+    (base-add*     : (r : Idx) → (a b : P r) → (base* r a) add* (base* r b) ≡ base* r (AbGroupStr._+_ (AGP r) a b))
+    where
+
+    f : ⊕ Idx P AGP → B
+    f z = DS-Ind-Set.f (λ _ → B) (λ _ → iss) neutral* base* _add*_ addAssoc* addRid* addComm* base-neutral* base-add* z
+
+
+
+  module DS-Ind-Prop
+    (Q            : (x : ⊕ Idx P AGP) → Type ℓ')
+    (ispd         : (x : ⊕ Idx P AGP) → isProp (Q x))
+    -- elements
+    (neutral*     : Q neutral)
+    (base*        : (r : Idx) → (a : P r) → Q (base r a))
+    (_add*_       : {x y : ⊕ Idx P AGP} → Q x → Q y → Q (x add y))
+    where
+
+    f : (x : ⊕ Idx P AGP) → Q x
+    f x = DS-Ind-Set.f Q (λ x → isProp→isSet (ispd x)) neutral* base* _add*_
+          (λ {x} {y} {z} xs ys zs → toPathP (ispd _ (transport (λ i → Q (addAssoc x y z i)) (xs add* (ys add* zs))) ((xs add* ys) add* zs)))
+          (λ {x} xs               → toPathP (ispd _ (transport (λ i → Q (addRid x i))       (xs add* neutral*)) xs))
+          (λ {x} {y} xs ys        → toPathP (ispd _ (transport (λ i → Q (addComm x y i))    (xs add* ys)) (ys add* xs)))
+          (λ r                    → toPathP (ispd _ (transport (λ i → Q (base-neutral r i)) (base* r (AbGroupStr.0g (AGP r)))) neutral*))
+          (λ r a b                → toPathP (ispd _ (transport (λ i → Q (base-add r a b i)) ((base* r a) add* (base* r b))) (base* r (AbGroupStr._+_ (AGP r) a b)  )))
+          x
+
+
+  module DS-Rec-Prop
+    (B        : Type ℓ')
+    (isp      : isProp B)
+    (neutral* : B)
+    (base*    : (r : Idx) → P r → B)
+    (_add*_   : B → B → B)
+    where
+
+    f : ⊕ Idx P AGP → B
+    f x = DS-Ind-Prop.f (λ _ → B) (λ _ → isp) neutral* base* _add*_ x

Cubical/Algebra/Direct-Sum/Properties.agda

@@ -0,0 +1,56 @@
+{-# OPTIONS --safe #-}
+module Cubical.Algebra.Direct-Sum.Properties where
+
+open import Cubical.Foundations.Prelude
+
+open import Cubical.Algebra.Group
+open import Cubical.Algebra.AbGroup
+
+open import Cubical.Algebra.Direct-Sum.Base
+
+private variable
+  ℓ : Level
+
+module _ (Idx : Type ℓ) (P : Idx → Type ℓ) (AGP : (r : Idx) → AbGroupStr (P r)) where
+
+  inv : ⊕ Idx P AGP → ⊕ Idx P AGP
+  inv = DS-Rec-Set.f Idx P AGP (⊕ Idx P AGP) trunc
+           -- elements
+           neutral
+           (λ r a → base r (AbGroupStr.-_ (AGP r) a))
+           (λ xs ys → xs add ys)
+           -- eq group
+           (λ xs ys zs → addAssoc xs ys zs)
+           (λ xs → addRid xs)
+           (λ xs ys → addComm xs ys)
+           -- eq base
+           (λ r → let open AbGroupStr (AGP r) in
+                   let open GroupTheory (P r , AbGroupStr→GroupStr (AGP r)) in
+                   (cong (base r) inv1g) ∙ (base-neutral r))
+           (λ r a b → let open AbGroupStr (AGP r) in
+                       let open GroupTheory (P r , AbGroupStr→GroupStr (AGP r)) in
+                       ((base r (- a) add base r (- b))   ≡⟨ (base-add r (- a) (- b)) ⟩
+                       base r ((- a) + (- b))             ≡⟨ (cong (base r) (sym (invDistr b a))) ⟩
+                       base r (- (b + a))                 ≡⟨ cong (base r) (cong (-_) (comm b a)) ⟩
+                       base r (- (a + b)) ∎))
+
+
+
+  rinv : (z : ⊕ Idx P AGP) → z add (inv z) ≡ neutral
+  rinv = DS-Ind-Prop.f Idx P AGP (λ z → z add (inv z) ≡ neutral) (λ _ → trunc _ _)
+         -- elements
+         (addRid neutral)
+         (λ r a → let open AbGroupStr (AGP r) in
+                        ((base r a add base r (- a)) ≡⟨ base-add r a (- a) ⟩
+                        base r (a + - a)             ≡⟨ cong (base r) (invr a) ⟩
+                        base r 0g                    ≡⟨ base-neutral r ⟩
+                        neutral ∎))
+         (λ {x} {y} p q →
+                        (((x add y) add ((inv x) add (inv y)))   ≡⟨ cong (λ X → X add ((inv x) add (inv y))) (addComm x y) ⟩
+                        ((y add x) add (inv x add inv y))        ≡⟨ sym (addAssoc y x (inv x add inv y)) ⟩
+                        (y add (x add (inv x add inv y)))        ≡⟨ cong (λ X → y add X) (addAssoc x (inv x) (inv y)) ⟩
+                        (y add ((x add inv x) add inv y))        ≡⟨ cong (λ X → y add (X add (inv y))) (p) ⟩
+                        (y add (neutral add inv y))              ≡⟨ cong (λ X → y add X) (addComm neutral (inv y)) ⟩
+                        (y add (inv y add neutral))              ≡⟨ cong (λ X → y add X) (addRid (inv y)) ⟩
+                        (y add inv y)                            ≡⟨ q ⟩
+                        neutral ∎))