From 704bf91538c8ce26ff3e2481e5686fd514d1e6d9 Mon Sep 17 00:00:00 2001 From: thomas-lamiaux Date: Mon, 28 Mar 2022 14:16:05 +0200 Subject: [PATCH 1/2] Add direct sum --- Cubical/Algebra/Direct-Sum/Base.agda | 122 +++++++++++++++++++++ Cubical/Algebra/Direct-Sum/Properties.agda | 90 +++++++++++++++ 2 files changed, 212 insertions(+) create mode 100644 Cubical/Algebra/Direct-Sum/Base.agda create mode 100644 Cubical/Algebra/Direct-Sum/Properties.agda diff --git a/Cubical/Algebra/Direct-Sum/Base.agda b/Cubical/Algebra/Direct-Sum/Base.agda new file mode 100644 index 0000000000..d8cd38fd0e --- /dev/null +++ b/Cubical/Algebra/Direct-Sum/Base.agda @@ -0,0 +1,122 @@ +{-# OPTIONS --safe #-} +module Cubical.Algebra.Direct-Sum.Base where + +open import Cubical.Foundations.Everything +open import Cubical.Data.Nat renaming(_+_ to _+n_) +open import Cubical.Foundations.HLevels +open import Cubical.Algebra.Group +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 + l l' : Level + + +data ⊕ (I : Type l) (P : I → Type l) (AGP : (r : I) → AbGroupStr (P r)) : Type l where + -- elements + neutral : ⊕ I P AGP + base : (r : I) → (P r) → ⊕ I P AGP + _add_ : ⊕ I P AGP → ⊕ I P AGP → ⊕ I P AGP + -- eq group + add-assoc : (x y z : ⊕ I P AGP) → x add (y add z) ≡ (x add y) add z + add-neutral : (x : ⊕ I P AGP) → x add neutral ≡ x + add-com : (x y : ⊕ I P AGP) → x add y ≡ y add x + -- eq base + base-neutral : (r : I) → base r (AbGroupStr.0g (AGP r)) ≡ neutral + base-add : (r : I) → (a b : P r) → (base r a) add (base r b) ≡ base r (AbGroupStr._+_ (AGP r) a b) + -- set + trunc : isSet (⊕ I P AGP) + + + +module _ (I : Type l) (P : I → Type l) (AGP : (r : I) → AbGroupStr (P r)) where + + module DS-Ind-Set + (Q : (x : ⊕ I P AGP) → Type l') + (issd : (x : ⊕ I P AGP) → isSet (Q x)) + -- elements + (ne : Q neutral) + (nb : (r : I) → (a : P r) → Q (base r a)) + (_na_ : {x y : ⊕ I P AGP} → Q x → Q y → Q (x add y)) + -- eq group + (add-assoc* : {x y z : ⊕ I P AGP} → (xs : Q x) → (ys : Q y) → (zs : Q z) + → PathP ( λ i → Q ( add-assoc x y z i)) (xs na (ys na zs)) ((xs na ys) na zs)) + (add-neutral* : {x : ⊕ I P AGP} → (xs : Q x) → + PathP (λ i → Q (add-neutral x i)) (xs na ne) xs ) + (add-com* : {x y : ⊕ I P AGP} → (xs : Q x) → (ys : Q y) + → PathP (λ i → Q (add-com x y i)) (xs na ys) (ys na xs)) + -- -- eq base + (base-neutral* : (r : I) → + PathP (λ i → Q (base-neutral r i)) (nb r (AbGroupStr.0g (AGP r))) ne) + (base-add* : (r : I) → (a b : P r) → + PathP (λ i → Q (base-add r a b i)) ((nb r a) na (nb r b)) (nb r (AbGroupStr._+_ (AGP r) a b))) + where + + f : (x : ⊕ I P AGP) → Q x + f neutral = ne + f (base r a) = nb r a + f (x add y) = (f x) na (f y) + f (add-assoc x y z i) = add-assoc* (f x) (f y) (f z) i + f (add-neutral x i) = add-neutral* (f x) i + f (add-com x y i) = add-com* (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 l') + (iss : isSet(B)) + (ne : B) + (nb : (r : I) → P r → B) + (_na_ : B → B → B) + (add-assoc* : (xs ys zs : B) → (xs na (ys na zs)) ≡ ((xs na ys) na zs)) + (add-neutral* : (xs : B) → xs na ne ≡ xs) + (add-com* : (xs ys : B) → xs na ys ≡ ys na xs) + (base-neutral* : (r : I) → nb r (AbGroupStr.0g (AGP r)) ≡ ne) + (base-add* : (r : I) → (a b : P r) → (nb r a) na (nb r b) ≡ nb r (AbGroupStr._+_ (AGP r) a b)) + where + + f : ⊕ I P AGP → B + f z = DS-Ind-Set.f (λ _ → B) (λ _ → iss) ne nb _na_ add-assoc* add-neutral* add-com* base-neutral* base-add* z + + + + module DS-Ind-Prop + (Q : (x : ⊕ I P AGP) → Type l') + (ispd : (x : ⊕ I P AGP) → isProp (Q x)) + -- elements + (ne : Q neutral) + (nb : (r : I) → (a : P r) → Q (base r a)) + (_na_ : {x y : ⊕ I P AGP} → Q x → Q y → Q (x add y)) + where + + f : (x : ⊕ I P AGP) → Q x + f x = DS-Ind-Set.f Q (λ x → isProp→isSet (ispd x)) ne nb _na_ + (λ {x} {y} {z} xs ys zs → toPathP (ispd _ (transport (λ i → Q (add-assoc x y z i)) (xs na (ys na zs))) ((xs na ys) na zs))) + (λ {x} xs → toPathP (ispd _ (transport (λ i → Q (add-neutral x i)) (xs na ne)) xs)) + (λ {x} {y} xs ys → toPathP (ispd _ (transport (λ i → Q (add-com x y i)) (xs na ys)) (ys na xs))) + (λ r → toPathP (ispd _ (transport (λ i → Q (base-neutral r i)) (nb r (AbGroupStr.0g (AGP r)))) ne)) + (λ r a b → toPathP (ispd _ (transport (λ i → Q (base-add r a b i)) ((nb r a) na (nb r b))) (nb r (AbGroupStr._+_ (AGP r) a b) ))) + x + + + module DS-Rec-Prop + (B : Type l') + (isp : isProp B) + (ne : B) + (nb : (r : I) → P r → B) + (_na_ : B → B → B) + where + + f : ⊕ I P AGP → B + f x = DS-Ind-Prop.f (λ _ → B) (λ _ → isp) ne nb _na_ x + + diff --git a/Cubical/Algebra/Direct-Sum/Properties.agda b/Cubical/Algebra/Direct-Sum/Properties.agda new file mode 100644 index 0000000000..cd328eaf05 --- /dev/null +++ b/Cubical/Algebra/Direct-Sum/Properties.agda @@ -0,0 +1,90 @@ +{-# OPTIONS --safe #-} +module Cubical.Algebra.Direct-Sum.Properties where + +open import Cubical.Foundations.Everything +open import Cubical.Data.Nat renaming(_+_ to _+n_) +open import Cubical.Data.Int renaming(_+_ to _+z_; -_ to -z; _·_ to _·z_ ) +open import Cubical.Foundations.HLevels +open import Cubical.Algebra.Semigroup +open import Cubical.Algebra.Monoid +open import Cubical.Algebra.Group +open import Cubical.Algebra.AbGroup +open import Cubical.Algebra.CommRing + + + +open import Cubical.Algebra.Direct-Sum.Base + +private variable + l l' : Level + +module _ (I : Type l) (P : I → Type l) (AGP : (r : I) → AbGroupStr (P r)) where + + inv : ⊕ I P AGP → ⊕ I P AGP + inv = DS-Rec-Set.f I P AGP (⊕ I P AGP) trunc + -- elements + neutral + (λ r a → base r (AbGroupStr.-_ (AGP r) a)) + (λ xs ys → xs add ys) + -- eq group + (λ xs ys zs → add-assoc xs ys zs) + (λ xs → add-neutral xs) + (λ xs ys → add-com 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 : ⊕ I P AGP) → z add (inv z) ≡ neutral + rinv = DS-Ind-Prop.f I P AGP (λ z → z add (inv z) ≡ neutral) (λ _ → trunc _ _) + -- elements + (add-neutral 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))) (add-com x y) ⟩ + ((y add x) add (inv x add inv y)) ≡⟨ sym (add-assoc y x (inv x add inv y)) ⟩ + (y add (x add (inv x add inv y))) ≡⟨ cong (λ X → y add X) (add-assoc 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) (add-com neutral (inv y)) ⟩ + (y add (inv y add neutral)) ≡⟨ cong (λ X → y add X) (add-neutral (inv y)) ⟩ + (y add inv y) ≡⟨ q ⟩ + neutral ∎)) + + + DS-com-adv : (x y z w : ⊕ I P AGP) → ((x add y) add (z add w) ≡ (x add z) add (y add w)) + DS-com-adv x y z w = ((x add y) add (z add w) ≡⟨ add-assoc (x add y) z w ⟩ + (((x add y) add z) add w) ≡⟨ cong (λ X → X add w) (sym (add-assoc x y z)) ⟩ + ((x add (y add z)) add w) ≡⟨ cong (λ X → (x add X) add w) (add-com y z) ⟩ + ((x add (z add y)) add w) ≡⟨ cong (λ X → X add w) (add-assoc x z y) ⟩ + (((x add z) add y) add w) ≡⟨ sym (add-assoc (x add z) y w) ⟩ + ((x add z) add (y add w)) ∎) + + + open AbGroupStr + open IsAbGroup + open IsGroup + open IsMonoid + open IsSemigroup + -- open isAbGroup + + ⊕-AbGr : AbGroup l + fst ⊕-AbGr = ⊕ I P AGP + 0g (snd ⊕-AbGr) = neutral + _+_ (snd ⊕-AbGr) = _add_ + - snd ⊕-AbGr = inv + isAbGroup (snd ⊕-AbGr) = makeIsAbGroup trunc add-assoc add-neutral rinv add-com + + + From bc0612d646faef37dfcd3f06a7af9681b08846c7 Mon Sep 17 00:00:00 2001 From: thomas-lamiaux Date: Sat, 2 Apr 2022 04:21:34 +0200 Subject: [PATCH 2/2] Pull request fix --- .../Algebra/AbGroup/Instances/Direct-Sum.agda | 23 +++ Cubical/Algebra/Direct-Sum/Base.agda | 145 +++++++++--------- Cubical/Algebra/Direct-Sum/Properties.agda | 70 +++------ 3 files changed, 112 insertions(+), 126 deletions(-) create mode 100644 Cubical/Algebra/AbGroup/Instances/Direct-Sum.agda diff --git a/Cubical/Algebra/AbGroup/Instances/Direct-Sum.agda b/Cubical/Algebra/AbGroup/Instances/Direct-Sum.agda new file mode 100644 index 0000000000..3b269cd3b3 --- /dev/null +++ b/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 diff --git a/Cubical/Algebra/Direct-Sum/Base.agda b/Cubical/Algebra/Direct-Sum/Base.agda index d8cd38fd0e..1c3a377e5a 100644 --- a/Cubical/Algebra/Direct-Sum/Base.agda +++ b/Cubical/Algebra/Direct-Sum/Base.agda @@ -1,10 +1,9 @@ {-# OPTIONS --safe #-} module Cubical.Algebra.Direct-Sum.Base where -open import Cubical.Foundations.Everything -open import Cubical.Data.Nat renaming(_+_ to _+n_) +open import Cubical.Foundations.Prelude open import Cubical.Foundations.HLevels -open import Cubical.Algebra.Group + open import Cubical.Algebra.AbGroup @@ -16,107 +15,105 @@ open import Cubical.Algebra.AbGroup private variable - l l' : Level + ℓ ℓ' : Level -data ⊕ (I : Type l) (P : I → Type l) (AGP : (r : I) → AbGroupStr (P r)) : Type l where +data ⊕ (Idx : Type ℓ) (P : Idx → Type ℓ) (AGP : (r : Idx) → AbGroupStr (P r)) : Type ℓ where -- elements - neutral : ⊕ I P AGP - base : (r : I) → (P r) → ⊕ I P AGP - _add_ : ⊕ I P AGP → ⊕ I P AGP → ⊕ I P AGP + neutral : ⊕ Idx P AGP + base : (r : Idx) → (P r) → ⊕ Idx P AGP + _add_ : ⊕ Idx P AGP → ⊕ Idx P AGP → ⊕ Idx P AGP -- eq group - add-assoc : (x y z : ⊕ I P AGP) → x add (y add z) ≡ (x add y) add z - add-neutral : (x : ⊕ I P AGP) → x add neutral ≡ x - add-com : (x y : ⊕ I P AGP) → x add y ≡ y add x - -- eq base - base-neutral : (r : I) → base r (AbGroupStr.0g (AGP r)) ≡ neutral - base-add : (r : I) → (a b : P r) → (base r a) add (base r b) ≡ base r (AbGroupStr._+_ (AGP r) a b) + 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 (⊕ I P AGP) + trunc : isSet (⊕ Idx P AGP) + - -module _ (I : Type l) (P : I → Type l) (AGP : (r : I) → AbGroupStr (P r)) where +module _ (Idx : Type ℓ) (P : Idx → Type ℓ) (AGP : (r : Idx) → AbGroupStr (P r)) where - module DS-Ind-Set - (Q : (x : ⊕ I P AGP) → Type l') - (issd : (x : ⊕ I P AGP) → isSet (Q x)) + module DS-Ind-Set + (Q : (x : ⊕ Idx P AGP) → Type ℓ') + (issd : (x : ⊕ Idx P AGP) → isSet (Q x)) -- elements - (ne : Q neutral) - (nb : (r : I) → (a : P r) → Q (base r a)) - (_na_ : {x y : ⊕ I P AGP} → Q x → Q y → Q (x add y)) + (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 - (add-assoc* : {x y z : ⊕ I P AGP} → (xs : Q x) → (ys : Q y) → (zs : Q z) - → PathP ( λ i → Q ( add-assoc x y z i)) (xs na (ys na zs)) ((xs na ys) na zs)) - (add-neutral* : {x : ⊕ I P AGP} → (xs : Q x) → - PathP (λ i → Q (add-neutral x i)) (xs na ne) xs ) - (add-com* : {x y : ⊕ I P AGP} → (xs : Q x) → (ys : Q y) - → PathP (λ i → Q (add-com x y i)) (xs na ys) (ys na xs)) + (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 : I) → - PathP (λ i → Q (base-neutral r i)) (nb r (AbGroupStr.0g (AGP r))) ne) - (base-add* : (r : I) → (a b : P r) → - PathP (λ i → Q (base-add r a b i)) ((nb r a) na (nb r b)) (nb r (AbGroupStr._+_ (AGP r) a b))) + (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 : ⊕ I P AGP) → Q x - f neutral = ne - f (base r a) = nb r a - f (x add y) = (f x) na (f y) - f (add-assoc x y z i) = add-assoc* (f x) (f y) (f z) i - f (add-neutral x i) = add-neutral* (f x) i - f (add-com x y i) = add-com* (f x) (f y) i + 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 l') + (B : Type ℓ') (iss : isSet(B)) - (ne : B) - (nb : (r : I) → P r → B) - (_na_ : B → B → B) - (add-assoc* : (xs ys zs : B) → (xs na (ys na zs)) ≡ ((xs na ys) na zs)) - (add-neutral* : (xs : B) → xs na ne ≡ xs) - (add-com* : (xs ys : B) → xs na ys ≡ ys na xs) - (base-neutral* : (r : I) → nb r (AbGroupStr.0g (AGP r)) ≡ ne) - (base-add* : (r : I) → (a b : P r) → (nb r a) na (nb r b) ≡ nb r (AbGroupStr._+_ (AGP r) a 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 : ⊕ I P AGP → B - f z = DS-Ind-Set.f (λ _ → B) (λ _ → iss) ne nb _na_ add-assoc* add-neutral* add-com* base-neutral* base-add* z + 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 : ⊕ I P AGP) → Type l') - (ispd : (x : ⊕ I P AGP) → isProp (Q x)) + module DS-Ind-Prop + (Q : (x : ⊕ Idx P AGP) → Type ℓ') + (ispd : (x : ⊕ Idx P AGP) → isProp (Q x)) -- elements - (ne : Q neutral) - (nb : (r : I) → (a : P r) → Q (base r a)) - (_na_ : {x y : ⊕ I P AGP} → Q x → Q y → Q (x add y)) + (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 : ⊕ I P AGP) → Q x - f x = DS-Ind-Set.f Q (λ x → isProp→isSet (ispd x)) ne nb _na_ - (λ {x} {y} {z} xs ys zs → toPathP (ispd _ (transport (λ i → Q (add-assoc x y z i)) (xs na (ys na zs))) ((xs na ys) na zs))) - (λ {x} xs → toPathP (ispd _ (transport (λ i → Q (add-neutral x i)) (xs na ne)) xs)) - (λ {x} {y} xs ys → toPathP (ispd _ (transport (λ i → Q (add-com x y i)) (xs na ys)) (ys na xs))) - (λ r → toPathP (ispd _ (transport (λ i → Q (base-neutral r i)) (nb r (AbGroupStr.0g (AGP r)))) ne)) - (λ r a b → toPathP (ispd _ (transport (λ i → Q (base-add r a b i)) ((nb r a) na (nb r b))) (nb r (AbGroupStr._+_ (AGP r) a b) ))) + 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 l') - (isp : isProp B) - (ne : B) - (nb : (r : I) → P r → B) - (_na_ : B → B → B) + module DS-Rec-Prop + (B : Type ℓ') + (isp : isProp B) + (neutral* : B) + (base* : (r : Idx) → P r → B) + (_add*_ : B → B → B) where - f : ⊕ I P AGP → B - f x = DS-Ind-Prop.f (λ _ → B) (λ _ → isp) ne nb _na_ x - - + f : ⊕ Idx P AGP → B + f x = DS-Ind-Prop.f (λ _ → B) (λ _ → isp) neutral* base* _add*_ x diff --git a/Cubical/Algebra/Direct-Sum/Properties.agda b/Cubical/Algebra/Direct-Sum/Properties.agda index cd328eaf05..5d143178a6 100644 --- a/Cubical/Algebra/Direct-Sum/Properties.agda +++ b/Cubical/Algebra/Direct-Sum/Properties.agda @@ -1,35 +1,28 @@ {-# OPTIONS --safe #-} module Cubical.Algebra.Direct-Sum.Properties where -open import Cubical.Foundations.Everything -open import Cubical.Data.Nat renaming(_+_ to _+n_) -open import Cubical.Data.Int renaming(_+_ to _+z_; -_ to -z; _·_ to _·z_ ) -open import Cubical.Foundations.HLevels -open import Cubical.Algebra.Semigroup -open import Cubical.Algebra.Monoid +open import Cubical.Foundations.Prelude + open import Cubical.Algebra.Group open import Cubical.Algebra.AbGroup -open import Cubical.Algebra.CommRing - - open import Cubical.Algebra.Direct-Sum.Base private variable - l l' : Level + ℓ : Level -module _ (I : Type l) (P : I → Type l) (AGP : (r : I) → AbGroupStr (P r)) where - - inv : ⊕ I P AGP → ⊕ I P AGP - inv = DS-Rec-Set.f I P AGP (⊕ I P AGP) trunc +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 → add-assoc xs ys zs) - (λ xs → add-neutral xs) - (λ xs ys → add-com xs ys) + (λ 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 @@ -43,48 +36,21 @@ module _ (I : Type l) (P : I → Type l) (AGP : (r : I) → AbGroupStr (P r)) wh - rinv : (z : ⊕ I P AGP) → z add (inv z) ≡ neutral - rinv = DS-Ind-Prop.f I P AGP (λ z → z add (inv z) ≡ neutral) (λ _ → trunc _ _) + 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 - (add-neutral neutral) + (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))) (add-com x y) ⟩ - ((y add x) add (inv x add inv y)) ≡⟨ sym (add-assoc y x (inv x add inv y)) ⟩ - (y add (x add (inv x add inv y))) ≡⟨ cong (λ X → y add X) (add-assoc x (inv x) (inv y)) ⟩ + (((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) (add-com neutral (inv y)) ⟩ - (y add (inv y add neutral)) ≡⟨ cong (λ X → y add X) (add-neutral (inv y)) ⟩ + (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 ∎)) - - - DS-com-adv : (x y z w : ⊕ I P AGP) → ((x add y) add (z add w) ≡ (x add z) add (y add w)) - DS-com-adv x y z w = ((x add y) add (z add w) ≡⟨ add-assoc (x add y) z w ⟩ - (((x add y) add z) add w) ≡⟨ cong (λ X → X add w) (sym (add-assoc x y z)) ⟩ - ((x add (y add z)) add w) ≡⟨ cong (λ X → (x add X) add w) (add-com y z) ⟩ - ((x add (z add y)) add w) ≡⟨ cong (λ X → X add w) (add-assoc x z y) ⟩ - (((x add z) add y) add w) ≡⟨ sym (add-assoc (x add z) y w) ⟩ - ((x add z) add (y add w)) ∎) - - - open AbGroupStr - open IsAbGroup - open IsGroup - open IsMonoid - open IsSemigroup - -- open isAbGroup - - ⊕-AbGr : AbGroup l - fst ⊕-AbGr = ⊕ I P AGP - 0g (snd ⊕-AbGr) = neutral - _+_ (snd ⊕-AbGr) = _add_ - - snd ⊕-AbGr = inv - isAbGroup (snd ⊕-AbGr) = makeIsAbGroup trunc add-assoc add-neutral rinv add-com - - -