diff --git a/Cubical/Algebra/AbGroup/Base.agda b/Cubical/Algebra/AbGroup/Base.agda index 2ce06d9d0..ba252daf5 100644 --- a/Cubical/Algebra/AbGroup/Base.agda +++ b/Cubical/Algebra/AbGroup/Base.agda @@ -195,3 +195,82 @@ assoc (isSemigroup (isMonoid (isGroup (isAbGroup (snd trivialAbGroup))))) _ _ _ identity (isMonoid (isGroup (isAbGroup (snd trivialAbGroup)))) _ = refl , refl inverse (isGroup (isAbGroup (snd trivialAbGroup))) _ = refl , refl comm (isAbGroup (snd trivialAbGroup)) _ _ = refl + +-- useful lemma +move4 : ∀ {ℓ} {A : Type ℓ} (x y z w : A) (_+_ : A → A → A) + → ((x y z : A) → x + (y + z) ≡ (x + y) + z) + → ((x y : A) → x + y ≡ y + x) + → (x + y) + (z + w) ≡ ((x + z) + (y + w)) +move4 x y z w _+_ assoc comm = + sym (assoc x y (z + w)) + ∙∙ cong (x +_) (assoc y z w ∙∙ cong (_+ w) (comm y z) ∙∙ sym (assoc z y w)) + ∙∙ assoc x z (y + w) + +---- The type of homomorphisms A → B is an AbGroup if B is ----- +module _ {ℓ ℓ' : Level} (AGr : Group ℓ) (BGr : AbGroup ℓ') where + private + strA = snd AGr + strB = snd BGr + + _* = AbGroup→Group + + A = fst AGr + B = fst BGr + open IsGroupHom + + open AbGroupStr strB + renaming (_+_ to _+B_ ; -_ to -B_ ; 0g to 0B + ; rid to ridB ; lid to lidB + ; assoc to assocB ; comm to commB + ; invr to invrB ; invl to invlB) + open GroupStr strA + renaming (_·_ to _∙A_ ; inv to -A_ + ; 1g to 1A ; rid to ridA) + + trivGroupHom : GroupHom AGr (BGr *) + fst trivGroupHom x = 0B + snd trivGroupHom = makeIsGroupHom λ _ _ → sym (ridB 0B) + + compHom : GroupHom AGr (BGr *) → GroupHom AGr (BGr *) → GroupHom AGr (BGr *) + fst (compHom f g) x = fst f x +B fst g x + snd (compHom f g) = + makeIsGroupHom λ x y + → cong₂ _+B_ (pres· (snd f) x y) (pres· (snd g) x y) + ∙ move4 (fst f x) (fst f y) (fst g x) (fst g y) + _+B_ assocB commB + + invHom : GroupHom AGr (BGr *) → GroupHom AGr (BGr *) + fst (invHom (f , p)) x = -B f x + snd (invHom (f , p)) = + makeIsGroupHom + λ x y → cong -B_ (pres· p x y) + ∙∙ GroupTheory.invDistr (BGr *) (f x) (f y) + ∙∙ commB _ _ + + open AbGroupStr + open IsAbGroup + open IsGroup + open IsMonoid + open IsSemigroup + + HomGroup : AbGroup (ℓ-max ℓ ℓ') + fst HomGroup = GroupHom AGr (BGr *) + 0g (snd HomGroup) = trivGroupHom + AbGroupStr._+_ (snd HomGroup) = compHom + AbGroupStr.- snd HomGroup = invHom + is-set (isSemigroup (isMonoid (isGroup (isAbGroup (snd HomGroup))))) = + isSetGroupHom + assoc (isSemigroup (isMonoid (isGroup (isAbGroup (snd HomGroup))))) (f , p) (g , q) (h , r) = + Σ≡Prop (λ _ → isPropIsGroupHom _ _) + (funExt λ x → assocB _ _ _) + fst (identity (isMonoid (isGroup (isAbGroup (snd HomGroup)))) (f , p)) = + Σ≡Prop (λ _ → isPropIsGroupHom _ _) (funExt λ y → ridB _) + snd (identity (isMonoid (isGroup (isAbGroup (snd HomGroup)))) (f , p)) = + Σ≡Prop (λ _ → isPropIsGroupHom _ _) (funExt λ x → lidB _) + fst (inverse (isGroup (isAbGroup (snd HomGroup))) (f , p)) = + Σ≡Prop (λ _ → isPropIsGroupHom _ _) (funExt λ x → invrB (f x)) + snd (inverse (isGroup (isAbGroup (snd HomGroup))) (f , p)) = + Σ≡Prop (λ _ → isPropIsGroupHom _ _) (funExt λ x → invlB (f x)) + comm (isAbGroup (snd HomGroup)) (f , p) (g , q) = + Σ≡Prop (λ _ → isPropIsGroupHom _ _) + (funExt λ x → commB _ _) diff --git a/Cubical/Algebra/AbGroup/TensorProduct.agda b/Cubical/Algebra/AbGroup/TensorProduct.agda new file mode 100644 index 000000000..3ad6aa1ee --- /dev/null +++ b/Cubical/Algebra/AbGroup/TensorProduct.agda @@ -0,0 +1,507 @@ +{-# OPTIONS --safe --experimental-lossy-unification #-} +module Cubical.Algebra.AbGroup.TensorProduct where + +open import Cubical.Algebra.AbGroup.Base +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Univalence +open import Cubical.Foundations.Function hiding (flip) +open import Cubical.Foundations.Isomorphism + +open import Cubical.Relation.Binary + +open import Cubical.Data.Sigma + +open import Cubical.Data.List +open import Cubical.Data.Nat as ℕ +open import Cubical.Foundations.HLevels +open import Cubical.Data.Int +open import Cubical.Data.Sum hiding (map) + +open import Cubical.HITs.PropositionalTruncation + renaming (map to pMap ; rec to pRec ; elim to pElim ; elim2 to pElim2) + +open import Cubical.Algebra.Group hiding (ℤ) +open import Cubical.Algebra.Group.Morphisms +open import Cubical.Algebra.Group.MorphismProperties +open import Cubical.Algebra.Monoid +open import Cubical.Algebra.Semigroup + +private + variable + ℓ ℓ' : Level + + +module _ (AGr : AbGroup ℓ) (BGr : AbGroup ℓ') where + private + open AbGroupStr renaming (_+_ to _+G_ ; -_ to -G_) + + strA = snd AGr + strB = snd BGr + + A = fst AGr + B = fst BGr + + 0A = 0g strA + 0B = 0g strB + + _+A_ = _+G_ strA + _+B_ = _+G_ strB + + -A_ = -G_ strA + -B_ = -G_ strB + + data _⨂₁_ : Type (ℓ-max ℓ ℓ') where + _⊗_ : (a : A) → (b : B) → _⨂₁_ + _+⊗_ : (w : _⨂₁_) → (u : _⨂₁_) → _⨂₁_ + + ⊗comm : (x y : _) → x +⊗ y ≡ y +⊗ x + ⊗assoc : (x y z : _) → x +⊗ (y +⊗ z) ≡ (x +⊗ y) +⊗ z + ⊗lUnit : (x : _) → (0A ⊗ 0B) +⊗ x ≡ x + + linl : (x y : A) (z : B) → (x +A y) ⊗ z ≡ ((x ⊗ z) +⊗ (y ⊗ z)) + linr : (x : A) (y z : B) → x ⊗ (y +B z) ≡ ((x ⊗ y) +⊗ (x ⊗ z)) + + ⊗squash : isSet _⨂₁_ + +module _ {AGr : AbGroup ℓ} {BGr : AbGroup ℓ'} where + private + open AbGroupStr renaming (_+_ to _+G_ ; -_ to -G_) + + strA = snd AGr + strB = snd BGr + + A = fst AGr + B = fst BGr + + 0A = 0g strA + 0B = 0g strB + + _+A_ = _+G_ strA + _+B_ = _+G_ strB + + -A_ = -G_ strA + -B_ = -G_ strB + + A⊗B = AGr ⨂₁ BGr + + ⊗elimProp : ∀ {ℓ} {C : AGr ⨂₁ BGr → Type ℓ} + → ((x : _) → isProp (C x)) + → (f : (x : A) (b : B) → C (x ⊗ b)) + → (g : ((x y : _) → C x → C y → C (x +⊗ y))) + → (x : _) → C x + ⊗elimProp p f g (a ⊗ b) = f a b + ⊗elimProp p f g (x +⊗ y) = g x y (⊗elimProp p f g x) (⊗elimProp p f g y) + ⊗elimProp {C = C} p f g (⊗comm x y j) = + isOfHLevel→isOfHLevelDep 1 {B = C} p + (g x y (⊗elimProp p f g x) (⊗elimProp p f g y)) + (g y x (⊗elimProp p f g y) (⊗elimProp p f g x)) (⊗comm x y) j + ⊗elimProp {C = C} p f g (⊗assoc x y z j) = + isOfHLevel→isOfHLevelDep 1 {B = C} p + (g x (y +⊗ z) (⊗elimProp p f g x) + (g y z (⊗elimProp p f g y) (⊗elimProp p f g z))) + (g (x +⊗ y) z (g x y (⊗elimProp p f g x) + (⊗elimProp p f g y)) (⊗elimProp p f g z)) (⊗assoc x y z) j + ⊗elimProp {C = C} p f g (⊗lUnit x i) = + isOfHLevel→isOfHLevelDep 1 {B = C} p + (g (0A ⊗ 0B) x (f 0A 0B) (⊗elimProp p f g x)) + (⊗elimProp p f g x) + (⊗lUnit x) i + ⊗elimProp {C = C} p f g (linl x y z i) = + isOfHLevel→isOfHLevelDep 1 {B = C} p + (f (x +A y) z) (g (x ⊗ z) (y ⊗ z) (f x z) (f y z)) (linl x y z) i + ⊗elimProp {C = C} p f g (linr x y z i) = + isOfHLevel→isOfHLevelDep 1 {B = C} p + (f x (y +B z)) (g (x ⊗ y) (x ⊗ z) (f x y) (f x z)) (linr x y z) i + ⊗elimProp {C = C} p f g (⊗squash x y q r i j) = + isOfHLevel→isOfHLevelDep 2 {B = C} (λ x → isProp→isSet (p x)) + _ _ (λ j → ⊗elimProp p f g (q j)) (λ j → ⊗elimProp p f g (r j)) + (⊗squash x y q r) i j + + -- Group structure + 0⊗ : AGr ⨂₁ BGr + 0⊗ = 0A ⊗ 0B + + -⊗ : AGr ⨂₁ BGr → AGr ⨂₁ BGr + -⊗ (a ⊗ b) = (-A a) ⊗ b + -⊗ (x +⊗ x₁) = -⊗ x +⊗ -⊗ x₁ + -⊗ (⊗comm x y i) = ⊗comm (-⊗ x) (-⊗ y) i + -⊗ (⊗assoc x y z i) = ⊗assoc (-⊗ x) (-⊗ y) (-⊗ z) i + -⊗ (⊗lUnit x i) = + ((λ i → (GroupTheory.inv1g (AbGroup→Group AGr) i ⊗ 0B) +⊗ -⊗ x) + ∙ ⊗lUnit (-⊗ x)) i + -⊗ (linl x y z i) = + ((λ i → (GroupTheory.invDistr (AbGroup→Group AGr) x y + ∙ comm strA (-A y) (-A x)) i ⊗ z) + ∙ linl (-A x) (-A y) z) i + -⊗ (linr x y z i) = linr (-A x) y z i + -⊗ (⊗squash x y p q i j) = + ⊗squash _ _ (λ j → -⊗ (p j)) (λ j → -⊗ (q j)) i j + + ⊗rUnit : (x : A⊗B) → x +⊗ 0⊗ ≡ x + ⊗rUnit x = ⊗comm x 0⊗ ∙ ⊗lUnit x + + ------------------------------------------------------------------------------- + -- Useful induction principle, which lets us view elements of A ⨂ B as lists + -- over (A × B). Used for the right cancellation law + unlist : List (A × B) → AGr ⨂₁ BGr + unlist [] = 0A ⊗ 0B + unlist (x ∷ x₁) = (fst x ⊗ snd x) +⊗ unlist x₁ + + unlist++ : (x y : List (A × B)) + → unlist (x ++ y) ≡ (unlist x +⊗ unlist y) + unlist++ [] y = sym (⊗lUnit (unlist y)) + unlist++ (x ∷ x₁) y = + (λ i → (fst x ⊗ snd x) +⊗ (unlist++ x₁ y i)) + ∙ ⊗assoc (fst x ⊗ snd x) (unlist x₁) (unlist y) + + ∃List : (x : AGr ⨂₁ BGr) → ∃[ l ∈ List (A × B) ] (unlist l ≡ x) + ∃List = + ⊗elimProp (λ _ → squash) + (λ a b → ∣ [ a , b ] , ⊗rUnit (a ⊗ b) ∣) + λ x y → rec2 squash λ {(l1 , p) (l2 , q) + → ∣ (l1 ++ l2) , unlist++ l1 l2 ∙ cong₂ _+⊗_ p q ∣} + + ⊗elimPropUnlist : ∀ {ℓ} {C : AGr ⨂₁ BGr → Type ℓ} + → ((x : _) → isProp (C x)) + → ((x : _) → C (unlist x)) + → (x : _) → C x + ⊗elimPropUnlist {C = C} p f = + ⊗elimProp p (λ x y → subst C (⊗rUnit (x ⊗ y)) (f [ x , y ])) + λ x y → pRec (isPropΠ2 λ _ _ → p _) + (pRec (isPropΠ3 λ _ _ _ → p _) + (λ {(l1 , p) (l2 , q) ind1 ind2 + → subst C (unlist++ l2 l1 ∙ cong₂ _+⊗_ q p) (f (l2 ++ l1))}) + (∃List y)) + (∃List x) + ----------------------------------------------------------------------------------- + + lCancelPrim : (x : B) → (0A ⊗ x) ≡ 0⊗ + lCancelPrim x = + sym (⊗rUnit _) + ∙∙ cong ((0A ⊗ x) +⊗_) (sym cancelLem) + ∙∙ ⊗assoc (0A ⊗ x) (0A ⊗ x) (0A ⊗ (-B x)) + ∙∙ cong (_+⊗ (0A ⊗ (-B x))) inner + ∙∙ cancelLem + where + cancelLem : (0A ⊗ x) +⊗ (0A ⊗ (-B x)) ≡ 0⊗ + cancelLem = sym (linr 0A x (-B x)) ∙ (λ i → 0A ⊗ invr strB x i) + + inner : (0A ⊗ x) +⊗ (0A ⊗ x) ≡ 0A ⊗ x + inner = sym (linl 0A 0A x) ∙ (λ i → rid strA 0A i ⊗ x) + + rCancelPrim : (x : A) → (x ⊗ 0B) ≡ 0⊗ + rCancelPrim x = + sym (⊗rUnit _) + ∙∙ cong ((x ⊗ 0B) +⊗_) (sym cancelLem) + ∙∙ ⊗assoc (x ⊗ 0B) (x ⊗ 0B) ((-A x) ⊗ 0B) + ∙∙ cong (_+⊗ ((-A x) ⊗ 0B)) inner + ∙∙ cancelLem + where + cancelLem : (x ⊗ 0B) +⊗ ((-A x) ⊗ 0B) ≡ 0⊗ + cancelLem = sym (linl x (-A x) 0B) ∙ (λ i → invr strA x i ⊗ 0B) + + inner : (x ⊗ 0B) +⊗ (x ⊗ 0B) ≡ x ⊗ 0B + inner = sym (linr x 0B 0B) ∙ (λ i → x ⊗ rid strB 0B i) + + flip : (x : A) (b : B) → x ⊗ (-B b) ≡ ((-A x) ⊗ b) + flip x b = + sym (⊗rUnit _) + ∙ cong ((x ⊗ (-B b)) +⊗_) (sym cancelLemA) + ∙ ⊗assoc (x ⊗ (-B b)) (x ⊗ b) ((-A x) ⊗ b) + ∙ cong (_+⊗ ((-A x) ⊗ b)) cancelLemB + ∙ ⊗lUnit _ + where + cancelLemA : (x ⊗ b) +⊗ ((-A x) ⊗ b) ≡ 0⊗ + cancelLemA = sym (linl x (-A x) b) ∙ (λ i → invr strA x i ⊗ b) ∙ lCancelPrim b + + cancelLemB : (x ⊗ (-B b)) +⊗ (x ⊗ b) ≡ 0⊗ + cancelLemB = sym (linr x (-B b) b) ∙ (λ i → x ⊗ invl strB b i) ∙ rCancelPrim x + + ⊗rCancel : (x : AGr ⨂₁ BGr) → (x +⊗ -⊗ x) ≡ 0⊗ + ⊗rCancel = + ⊗elimPropUnlist (λ _ → ⊗squash _ _) h + where + h : (x : List (A × B)) → (unlist x +⊗ -⊗ (unlist x)) ≡ 0⊗ + h [] = sym (linl 0A (-A 0A) (0B)) + ∙ cong (λ x → _⊗_ {AGr = AGr} {BGr = BGr} x 0B) (invr strA 0A) + h (x ∷ x₁) = + move4 (fst x ⊗ snd x) (unlist x₁) ((-A fst x) ⊗ snd x) (-⊗ (unlist x₁)) + _+⊗_ ⊗assoc ⊗comm + ∙∙ cong₂ _+⊗_ (sym (linl (fst x) (-A (fst x)) (snd x)) + ∙∙ (λ i → invr strA (fst x) i ⊗ (snd x)) + ∙∙ lCancelPrim (snd x)) + (h x₁) + ∙∙ ⊗rUnit 0⊗ + + ⊗lCancel : (x : AGr ⨂₁ BGr) → (-⊗ x +⊗ x) ≡ 0⊗ + ⊗lCancel x = ⊗comm _ _ ∙ ⊗rCancel x + +module _ where + open AbGroupStr + open IsAbGroup + open IsGroup + open IsMonoid + open IsSemigroup + + _⨂_ : AbGroup ℓ → AbGroup ℓ' → AbGroup (ℓ-max ℓ ℓ') + fst (A ⨂ B) = A ⨂₁ B + 0g (snd (A ⨂ B)) = 0⊗ + AbGroupStr._+_ (snd (A ⨂ B)) = _+⊗_ + AbGroupStr.- snd (A ⨂ B) = -⊗ + is-set (isSemigroup (isMonoid (isGroup (isAbGroup (snd (A ⨂ B)))))) = ⊗squash + assoc (isSemigroup (isMonoid (isGroup (isAbGroup (snd (A ⨂ B)))))) = ⊗assoc + fst (identity (isMonoid (isGroup (isAbGroup (snd (A ⨂ B))))) x) = ⊗rUnit x + snd (identity (isMonoid (isGroup (isAbGroup (snd (A ⨂ B))))) x) = ⊗lUnit x + fst (inverse (isGroup (isAbGroup (snd (A ⨂ B)))) x) = ⊗rCancel x + snd (inverse (isGroup (isAbGroup (snd (A ⨂ B)))) x) = ⊗lCancel x + comm (isAbGroup (snd (A ⨂ B))) = ⊗comm + +-------------- Elimination principle into AbGroups -------------- +module _ {ℓ ℓ' : Level} {A : AbGroup ℓ} {B : AbGroup ℓ'} where + private + open AbGroupStr renaming (_+_ to _+G_ ; -_ to -G) + _+A_ = _+G_ (snd A) + _+B_ = _+G_ (snd B) + + 0A = 0g (snd A) + 0B = 0g (snd B) + + ⨂→AbGroup-elim : ∀ {ℓ} (C : AbGroup ℓ) + → (f : (fst A × fst B) → fst C) + → (f (0A , 0B) ≡ 0g (snd C)) + → (linL : (x y : fst A) (b : fst B) + → f (x +A y , b) ≡ _+G_ (snd C) (f (x , b)) (f (y , b))) + → (linR : (a : fst A) (x y : fst B) + → f (a , x +B y) ≡ _+G_ (snd C) (f (a , x)) (f (a , y))) + → A ⨂₁ B → fst C + ⨂→AbGroup-elim C f p linL linR (a ⊗ b) = f (a , b) + ⨂→AbGroup-elim C f p linL linR (x +⊗ x₁) = + _+G_ (snd C) (⨂→AbGroup-elim C f p linL linR x) + (⨂→AbGroup-elim C f p linL linR x₁) + ⨂→AbGroup-elim C f p linL linR (⊗comm x x₁ i) = + comm (snd C) (⨂→AbGroup-elim C f p linL linR x) + (⨂→AbGroup-elim C f p linL linR x₁) i + ⨂→AbGroup-elim C f p linL linR (⊗assoc x x₁ x₂ i) = + assoc (snd C) (⨂→AbGroup-elim C f p linL linR x) + (⨂→AbGroup-elim C f p linL linR x₁) + (⨂→AbGroup-elim C f p linL linR x₂) i + ⨂→AbGroup-elim C f p linL linR (⊗lUnit x i) = + (cong (λ y → (snd C +G y) (⨂→AbGroup-elim C f p linL linR x)) p + ∙ (lid (snd C) (⨂→AbGroup-elim C f p linL linR x))) i + ⨂→AbGroup-elim C f p linL linR (linl x y z i) = linL x y z i + ⨂→AbGroup-elim C f p linL linR (linr x y z i) = linR x y z i + ⨂→AbGroup-elim C f p linL linR (⊗squash x x₁ x₂ y i i₁) = + is-set (snd C) _ _ + (λ i → ⨂→AbGroup-elim C f p linL linR (x₂ i)) + (λ i → ⨂→AbGroup-elim C f p linL linR (y i)) i i₁ + + ⨂→AbGroup-elim-hom : ∀ {ℓ} (C : AbGroup ℓ) + → (f : (fst A × fst B) → fst C) (linL : _) (linR : _) (p : _) + → AbGroupHom (A ⨂ B) C + fst (⨂→AbGroup-elim-hom C f linL linR p) = ⨂→AbGroup-elim C f p linL linR + snd (⨂→AbGroup-elim-hom C f linL linR p) = + makeIsGroupHom + (λ x y → refl) + +private + _* = AbGroup→Group + + +----------- Definition of universal property ------------ +tensorFun : (A : Group ℓ) (B : Group ℓ') (T C : AbGroup (ℓ-max ℓ ℓ')) + (f : GroupHom A (HomGroup B T *)) + → GroupHom (T *) (C *) + → GroupHom A (HomGroup B C *) +fst (fst (tensorFun A B T C (f , p) (g , q)) a) b = g (fst (f a) b) +snd (fst (tensorFun A B T C (f , p) (g , q)) a) = + makeIsGroupHom λ x y + → cong g (IsGroupHom.pres· (snd (f a)) x y) + ∙ IsGroupHom.pres· q _ _ +snd (tensorFun A B T C (f , p) (g , q)) = + makeIsGroupHom λ x y + → Σ≡Prop (λ _ → isPropIsGroupHom _ _) + (funExt λ b + → cong g (funExt⁻ (cong fst (IsGroupHom.pres· p x y)) b) + ∙ IsGroupHom.pres· q _ _) + +isTensorProductOf_and_ : AbGroup ℓ → AbGroup ℓ' → AbGroup (ℓ-max ℓ ℓ')→ Type _ +isTensorProductOf_and_ {ℓ} {ℓ'} A B T = + Σ[ f ∈ GroupHom (A *) ((HomGroup (B *) T) *) ] + ((C : AbGroup (ℓ-max ℓ ℓ')) + → isEquiv {A = GroupHom (T *) (C *)} + {B = GroupHom (A *) ((HomGroup (B *) C) *)} + (tensorFun (A *) (B *) T C f)) + +------ _⨂_ satisfies the universal property -------- +module UP (AGr : AbGroup ℓ) (BGr : AbGroup ℓ') where + private + open AbGroupStr renaming (_+_ to _+G_ ; -_ to -G_) + + strA = snd AGr + strB = snd BGr + + A = fst AGr + B = fst BGr + + 0A = 0g strA + 0B = 0g strB + + _+A_ = _+G_ strA + _+B_ = _+G_ strB + + -A_ = -G_ strA + -B_ = -G_ strB + + mainF : GroupHom (AGr *) (HomGroup (BGr *) (AGr ⨂ BGr) *) + fst (fst mainF a) b = a ⊗ b + snd (fst mainF a) = + makeIsGroupHom (linr a) + snd mainF = + makeIsGroupHom λ x y → Σ≡Prop (λ _ → isPropIsGroupHom _ _) + (funExt (linl x y)) + + isTensorProduct⨂ : (isTensorProductOf AGr and BGr) (AGr ⨂ BGr) + fst isTensorProduct⨂ = mainF + snd isTensorProduct⨂ C = isoToIsEquiv mainIso + where + invF : GroupHom (AGr *) (HomGroup (BGr *) C *) → GroupHom ((AGr ⨂ BGr) *) (C *) + fst (invF (f , p)) = F + where + lem : f (0g (snd AGr)) .fst (0g (snd BGr)) ≡ 0g (snd C) + lem = funExt⁻ (cong fst (IsGroupHom.pres1 p)) (0g (snd BGr)) + F : ((AGr ⨂ BGr) *) .fst → (C *) .fst + F (a ⊗ b) = f a .fst b + F (x +⊗ x₁) = _+G_ (snd C) (F x) (F x₁) + F (⊗comm x x₁ i) = comm (snd C) (F x) (F x₁) i + F (⊗assoc x y z i) = assoc (snd C) (F x) (F y) (F z) i + F (⊗lUnit x i) = (cong (λ y → _+G_ (snd C) y (F x)) lem ∙ lid (snd C) (F x)) i + F (linl x y z i) = fst (IsGroupHom.pres· p x y i) z + F (linr x y z i) = IsGroupHom.pres· (f x .snd) y z i + F (⊗squash x x₁ x₂ y i i₁) = + is-set (snd C) (F x) (F x₁) + (λ i → F (x₂ i)) (λ i → F (y i)) i i₁ + snd (invF (f , p)) = + makeIsGroupHom λ x y → refl + + mainIso : Iso (GroupHom ((AGr ⨂ BGr) *) (C *)) + (GroupHom (AGr *) (HomGroup (BGr *) C *)) + Iso.fun mainIso = _ + Iso.inv mainIso = invF + Iso.rightInv mainIso (f , p) = + Σ≡Prop (λ _ → isPropIsGroupHom _ _) + (funExt λ a → Σ≡Prop (λ _ → isPropIsGroupHom _ _) refl) + Iso.leftInv mainIso (f , p) = + Σ≡Prop (λ _ → isPropIsGroupHom _ _) + (funExt (⊗elimProp (λ _ → is-set (snd C) _ _) + (λ _ _ → refl) + λ x y ind1 ind2 → cong₂ (_+G_ (snd C)) ind1 ind2 ∙ sym (IsGroupHom.pres· p x y))) + +-------------------- Commutativity ------------------------ +commFun : ∀ {ℓ ℓ'} {A : AbGroup ℓ} {B : AbGroup ℓ'} → A ⨂₁ B → B ⨂₁ A +commFun (a ⊗ b) = b ⊗ a +commFun (x +⊗ x₁) = commFun x +⊗ commFun x₁ +commFun (⊗comm x x₁ i) = ⊗comm (commFun x) (commFun x₁) i +commFun (⊗assoc x x₁ x₂ i) = ⊗assoc (commFun x) (commFun x₁) (commFun x₂) i +commFun (⊗lUnit x i) = ⊗lUnit (commFun x) i +commFun (linl x y z i) = linr z x y i +commFun (linr x y z i) = linl y z x i +commFun (⊗squash x x₁ x₂ y i i₁) = + ⊗squash (commFun x) (commFun x₁) + (λ i → commFun (x₂ i)) (λ i → commFun (y i)) i i₁ + +commFun²≡id : ∀ {ℓ ℓ'} {A : AbGroup ℓ} {B : AbGroup ℓ'} (x : A ⨂₁ B) + → commFun (commFun x) ≡ x +commFun²≡id = + ⊗elimProp (λ _ → ⊗squash _ _) + (λ _ _ → refl) + λ _ _ p q → cong₂ _+⊗_ p q + +⨂-commIso : ∀ {ℓ ℓ'} {A : AbGroup ℓ} {B : AbGroup ℓ'} + → GroupIso ((A ⨂ B) *) ((B ⨂ A) *) +Iso.fun (fst ⨂-commIso) = commFun +Iso.inv (fst ⨂-commIso) = commFun +Iso.rightInv (fst ⨂-commIso) = commFun²≡id +Iso.leftInv (fst ⨂-commIso) = commFun²≡id +snd ⨂-commIso = makeIsGroupHom λ x y → refl + +⨂-comm : ∀ {ℓ ℓ'} {A : AbGroup ℓ} {B : AbGroup ℓ'} → AbGroupEquiv (A ⨂ B) (B ⨂ A) +fst ⨂-comm = isoToEquiv (fst (⨂-commIso)) +snd ⨂-comm = snd ⨂-commIso + +open AbGroupStr + +-------------------- Associativity ------------------------ +module _ {ℓ ℓ' ℓ'' : Level} {A : AbGroup ℓ} {B : AbGroup ℓ'} {C : AbGroup ℓ''} where + private + f : (c : fst C) → AbGroupHom (A ⨂ B) (A ⨂ (B ⨂ C)) + f c = ⨂→AbGroup-elim-hom (A ⨂ (B ⨂ C)) ((λ ab → fst ab ⊗ (snd ab ⊗ c))) + (λ x y b → linl x y (b ⊗ c)) + (λ x y b → (λ i → x ⊗ (linl y b c i)) ∙ linr x (y ⊗ c) (b ⊗ c)) + (λ i → 0g (snd A) ⊗ (lCancelPrim c i)) + + assocHom : AbGroupHom ((A ⨂ B) ⨂ C) (A ⨂ (B ⨂ C)) + assocHom = + ⨂→AbGroup-elim-hom _ (λ x → f (snd x) .fst (fst x)) + (λ x y b → IsGroupHom.pres· (snd (f b)) x y) + (⊗elimProp (λ _ → isPropΠ2 λ _ _ → ⊗squash _ _) + (λ a b x y → (λ i → a ⊗ (linr b x y i)) + ∙∙ linr a (b ⊗ x) (b ⊗ y) + ∙∙ refl) + λ a b ind1 ind2 x y → cong₂ _+⊗_ (ind1 x y) (ind2 x y) + ∙∙ move4 (f x .fst a) (f y .fst a) (f x .fst b) (f y .fst b) + _+⊗_ ⊗assoc ⊗comm + ∙∙ cong₂ _+⊗_ (sym (IsGroupHom.pres· (snd (f x)) a b)) + (IsGroupHom.pres· (snd (f y)) a b)) + refl + +module _ {ℓ ℓ' ℓ'' : Level} {A : AbGroup ℓ} {B : AbGroup ℓ'} {C : AbGroup ℓ''} where + private + f' : (a : fst A) → AbGroupHom (B ⨂ C) ((A ⨂ B) ⨂ C) + f' a = + ⨂→AbGroup-elim-hom ((A ⨂ B) ⨂ C) + (λ bc → (a ⊗ fst bc) ⊗ snd bc) + (λ x y b → (λ i → (linr a x y i) ⊗ b) ∙ linl (a ⊗ x) (a ⊗ y) b) + (λ x y b → linr (a ⊗ x) y b) + λ i → rCancelPrim a i ⊗ (0g (snd C)) + + assocHom⁻ : AbGroupHom (A ⨂ (B ⨂ C)) ((A ⨂ B) ⨂ C) + assocHom⁻ = + ⨂→AbGroup-elim-hom _ (λ abc → f' (fst abc) .fst (snd abc)) + (λ x y → ⊗elimProp (λ _ → ⊗squash _ _) + (λ b c → (λ i → linl x y b i ⊗ c) ∙ linl (x ⊗ b) (y ⊗ b) c) + λ a b ind1 ind2 → cong₂ _+⊗_ ind1 ind2 + ∙∙ move4 _ _ _ _ _+⊗_ ⊗assoc ⊗comm + ∙∙ cong₂ _+⊗_ (IsGroupHom.pres· (snd (f' x)) a b) + (IsGroupHom.pres· (snd (f' y)) a b)) + (λ a → IsGroupHom.pres· (snd (f' a))) + refl + + ⨂assocIso : Iso (A ⨂₁ (B ⨂ C)) ((A ⨂ B) ⨂₁ C) + Iso.fun ⨂assocIso = fst assocHom⁻ + Iso.inv ⨂assocIso = fst assocHom + Iso.rightInv ⨂assocIso = + ⊗elimProp (λ _ → ⊗squash _ _) + (⊗elimProp (λ _ → isPropΠ (λ _ → ⊗squash _ _)) + (λ a b c → refl) + λ a b ind1 ind2 c → cong₂ _+⊗_ (ind1 c) (ind2 c) ∙ sym (linl a b c)) + λ x y p q → cong (fst assocHom⁻) (IsGroupHom.pres· (snd assocHom) x y) + ∙∙ IsGroupHom.pres· (snd assocHom⁻) (fst assocHom x) (fst assocHom y) + ∙∙ cong₂ _+⊗_ p q + Iso.leftInv ⨂assocIso = + ⊗elimProp (λ _ → ⊗squash _ _) + (λ a → ⊗elimProp (λ _ → ⊗squash _ _) + (λ b c → refl) + λ x y ind1 ind2 → + cong (fst assocHom ∘ fst assocHom⁻) (linr a x y) + ∙∙ cong (fst assocHom) (IsGroupHom.pres· (snd assocHom⁻) (a ⊗ x) (a ⊗ y)) + ∙∙ IsGroupHom.pres· (snd assocHom) (fst assocHom⁻ (a ⊗ x)) (fst assocHom⁻ (a ⊗ y)) + ∙∙ cong₂ _+⊗_ ind1 ind2 + ∙∙ sym (linr a x y)) + λ x y p q → cong (fst assocHom) (IsGroupHom.pres· (snd assocHom⁻) x y) + ∙∙ IsGroupHom.pres· (snd assocHom) (fst assocHom⁻ x) (fst assocHom⁻ y) + ∙∙ cong₂ _+⊗_ p q + + ⨂assoc : AbGroupEquiv (A ⨂ (B ⨂ C)) ((A ⨂ B) ⨂ C) + fst ⨂assoc = isoToEquiv ⨂assocIso + snd ⨂assoc = snd assocHom⁻ diff --git a/Cubical/Algebra/Group/EilenbergMacLane/Base.agda b/Cubical/Algebra/Group/EilenbergMacLane/Base.agda new file mode 100644 index 000000000..f4d56a499 --- /dev/null +++ b/Cubical/Algebra/Group/EilenbergMacLane/Base.agda @@ -0,0 +1,93 @@ +{-# OPTIONS --safe --experimental-lossy-unification #-} + +module Cubical.Algebra.Group.EilenbergMacLane.Base where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Equiv.HalfAdjoint +open import Cubical.Foundations.GroupoidLaws renaming (assoc to ∙assoc) +open import Cubical.Foundations.Path +open import Cubical.Foundations.HLevels +open import Cubical.Foundations.Univalence +open import Cubical.Foundations.Pointed +open import Cubical.Foundations.Transport + +open import Cubical.Data.Unit +open import Cubical.Data.Sigma +open import Cubical.Algebra.Group.Base +open import Cubical.Algebra.Group.Properties +open import Cubical.Homotopy.Connected +open import Cubical.HITs.Truncation as Trunc renaming (rec to trRec; elim to trElim) +open import Cubical.HITs.EilenbergMacLane1 hiding (elim) +open import Cubical.Algebra.AbGroup.Base +open import Cubical.Data.Empty + renaming (rec to ⊥-rec) hiding (elim) +open import Cubical.HITs.Truncation + renaming (elim to trElim ; rec to trRec ; rec2 to trRec2) +open import Cubical.Data.Nat hiding (_·_ ; elim) +open import Cubical.HITs.Susp +open import Cubical.Functions.Morphism +open import Cubical.Foundations.Path + +private + variable ℓ ℓ' : Level + + _* = AbGroup→Group + +EM-raw : (G : AbGroup ℓ) (n : ℕ) → Type ℓ +EM-raw G zero = fst G +EM-raw G (suc zero) = EM₁ (G *) +EM-raw G (suc (suc n)) = Susp (EM-raw G (suc n)) + +ptEM-raw : {n : ℕ} {G : AbGroup ℓ} → EM-raw G n +ptEM-raw {n = zero} {G = G} = AbGroupStr.0g (snd G) +ptEM-raw {n = suc zero} {G = G} = embase +ptEM-raw {n = suc (suc n)} {G = G} = north + +raw-elim : (G : AbGroup ℓ) (n : ℕ) {A : EM-raw G (suc n) → Type ℓ'} + → ((x : _) → isOfHLevel (suc n) (A x) ) + → A ptEM-raw + → (x : _) → A x +raw-elim G zero hlev b = elimProp _ hlev b +raw-elim G (suc n) hlev b north = b +raw-elim G (suc n) {A = A} hlev b south = subst A (merid ptEM-raw) b +raw-elim G (suc n) {A = A} hlev b (merid a i) = help a i + where + help : (a : _) → PathP (λ i → A (merid a i)) b (subst A (merid ptEM-raw) b) + help = raw-elim G n (λ _ → isOfHLevelPathP' (suc n) (hlev _) _ _) + λ i → transp (λ j → A (merid ptEM-raw (j ∧ i))) (~ i) b + +EM : (G : AbGroup ℓ) (n : ℕ) → Type ℓ +EM G zero = EM-raw G zero +EM G (suc zero) = EM-raw G 1 +EM G (suc (suc n)) = hLevelTrunc (4 + n) (EM-raw G (suc (suc n))) + +0ₖ : {G : AbGroup ℓ} (n : ℕ) → EM G n +0ₖ {G = G} zero = AbGroupStr.0g (snd G) +0ₖ (suc zero) = embase +0ₖ (suc (suc n)) = ∣ ptEM-raw ∣ + +EM∙ : (G : AbGroup ℓ) (n : ℕ) → Pointed ℓ +EM∙ G n = EM G n , (0ₖ n) + +EM-raw∙ : (G : AbGroup ℓ) (n : ℕ) → Pointed ℓ +EM-raw∙ G n = EM-raw G n , ptEM-raw + +hLevelEM : (G : AbGroup ℓ) (n : ℕ) → isOfHLevel (2 + n) (EM G n) +hLevelEM G zero = AbGroupStr.is-set (snd G) +hLevelEM G (suc zero) = emsquash +hLevelEM G (suc (suc n)) = isOfHLevelTrunc (4 + n) + +EM-raw→EM : (G : AbGroup ℓ) (n : ℕ) → EM-raw G n → EM G n +EM-raw→EM G zero x = x +EM-raw→EM G (suc zero) x = x +EM-raw→EM G (suc (suc n)) = ∣_∣ + +elim : {G : AbGroup ℓ} (n : ℕ) {A : EM G n → Type ℓ'} + → ((x : _) → isOfHLevel (2 + n) (A x)) + → ((x : EM-raw G n) → A (EM-raw→EM G n x)) + → (x : _) → A x +elim zero hlev hyp x = hyp x +elim (suc zero) hlev hyp x = hyp x +elim (suc (suc n)) hlev hyp = trElim (λ _ → hlev _) hyp diff --git a/Cubical/Algebra/Group/EilenbergMacLane/CupProduct.agda b/Cubical/Algebra/Group/EilenbergMacLane/CupProduct.agda new file mode 100644 index 000000000..f6339e928 --- /dev/null +++ b/Cubical/Algebra/Group/EilenbergMacLane/CupProduct.agda @@ -0,0 +1,405 @@ +{-# OPTIONS --safe --experimental-lossy-unification #-} + +module Cubical.Algebra.Group.EilenbergMacLane.CupProduct where + +open import Cubical.Algebra.Group.EilenbergMacLane.Base renaming (elim to EM-elim) +open import Cubical.Algebra.Group.EilenbergMacLane.WedgeConnectivity +open import Cubical.Algebra.Group.EilenbergMacLane.GroupStructure +open import Cubical.Algebra.Group.EilenbergMacLane.Properties +open import Cubical.Algebra.Group.Base +open import Cubical.Algebra.Group.Properties + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.GroupoidLaws renaming (assoc to ∙assoc) +open import Cubical.Foundations.Path +open import Cubical.Foundations.HLevels +open import Cubical.Foundations.Pointed +open import Cubical.Foundations.Transport + +open import Cubical.Foundations.Pointed.Homogeneous + +open import Cubical.Functions.Morphism + +open import Cubical.Homotopy.Loopspace + +open import Cubical.HITs.Truncation as Trunc renaming (rec to trRec; elim to trElim) +open import Cubical.HITs.EilenbergMacLane1 renaming (rec to EMrec) +open import Cubical.Algebra.AbGroup.Base +open import Cubical.Data.Empty + renaming (rec to ⊥-rec) +open import Cubical.HITs.Truncation + renaming (elim to trElim ; rec to trRec ; rec2 to trRec2) +open import Cubical.Data.Nat hiding (_·_) renaming (elim to ℕelim) +open import Cubical.HITs.Susp + +open import Cubical.Algebra.AbGroup.TensorProduct +open import Cubical.Algebra.Group + +open import Cubical.ZCohomology.RingStructure.CupProduct + using (_+'_ ; +'≡+ ; +'-comm) + +open AbGroupStr renaming (_+_ to _+Gr_ ; -_ to -Gr_) + +private + variable + ℓ ℓ' ℓ'' : Level + +-- Lemma for distributativity of cup product (used later) +pathType : ∀ {ℓ} {G : AbGroup ℓ} (n : ℕ) (x : EM G (2 + n)) (p : 0ₖ (2 + n) ≡ x) → Type ℓ +pathType n x p = sym (rUnitₖ (2 + n) x) ∙ (λ i → x +ₖ p i) + ≡ sym (lUnitₖ (2 + n) x) ∙ λ i → p i +ₖ x + +pathTypeMake : ∀ {ℓ} {G : AbGroup ℓ} (n : ℕ) (x : EM G (2 + n)) (p : 0ₖ (2 + n) ≡ x) + → pathType n x p +pathTypeMake n x = J (λ x p → pathType n x p) refl + + +-- Definition of cup product (⌣ₖ, given by ·₀ when first argument is in K(G,0)) +module _ {G' : AbGroup ℓ} {H' : AbGroup ℓ'} where + private + G = fst G' + H = fst H' + + strG = snd G' + strH = snd H' + + 0G = 0g strG + 0H = 0g strH + + _+G_ = _+Gr_ strG + _+H_ = _+Gr_ strH + + -H_ = -Gr_ strH + -G_ = -Gr_ strG + + ·₀' : H → (m : ℕ) → EM G' m → EM (G' ⨂ H') m + ·₀' h = + elim+2 + (_⊗ h) + (elimGroupoid _ (λ _ → emsquash) + embase + (λ g → emloop (g ⊗ h)) + λ g l → + compPathR→PathP + (sym (∙assoc _ _ _ + ∙∙ cong₂ _∙_ (sym (emloop-comp _ _ _) + ∙ cong emloop (sym (linl g l h))) refl + ∙∙ rCancel _))) + λ n f → trRec (isOfHLevelTrunc (4 + n)) + λ { north → 0ₖ (suc (suc n)) + ; south → 0ₖ (suc (suc n)) + ; (merid a i) → EM→ΩEM+1 (suc n) (f (EM-raw→EM _ _ a)) i} + + ·₀ : G → (m : ℕ) → EM H' m → EM (G' ⨂ H') m + ·₀ g = + elim+2 (λ h → g ⊗ h) + (elimGroupoid _ (λ _ → emsquash) + embase + (λ h → emloop (g ⊗ h)) + λ h l → compPathR→PathP + (sym (∙assoc _ _ _ + ∙∙ cong₂ _∙_ (sym (emloop-comp _ _ _) ∙ cong emloop (sym (linr g h l))) refl + ∙∙ rCancel _))) + λ n f + → trRec (isOfHLevelTrunc (4 + n)) + λ { north → 0ₖ (suc (suc n)) + ; south → 0ₖ (suc (suc n)) + ; (merid a i) → EM→ΩEM+1 (suc n) (f (EM-raw→EM _ _ a)) i} + + ·₀-distr : (g h : G) → (m : ℕ) (x : EM H' m) → ·₀ (g +G h) m x ≡ ·₀ g m x +ₖ ·₀ h m x + ·₀-distr g h = + elim+2 + (linl g h) + (elimSet _ (λ _ → emsquash _ _) + refl + (λ w → compPathR→PathP (sym ((λ i → emloop (linl g h w i) + ∙ (lUnit (sym (cong₂+₁ (emloop (g ⊗ w)) (emloop (h ⊗ w)) i)) (~ i))) + ∙∙ cong₂ _∙_ (emloop-comp _ (g ⊗ w) (h ⊗ w)) refl + ∙∙ rCancel _)))) + λ m ind → + trElim (λ _ → isOfHLevelTruncPath) + λ { north → refl + ; south → refl + ; (merid a i) k → z m ind a k i} + + where + z : (m : ℕ) → ((x : EM H' (suc m)) + → ·₀ (g +G h) (suc m) x + ≡ ·₀ g (suc m) x +ₖ ·₀ h (suc m) x) → (a : EM-raw H' (suc m)) + → cong (·₀ (g +G h) (suc (suc m))) (cong ∣_∣ₕ (merid a)) ≡ + cong₂ _+ₖ_ + (cong (·₀ g (suc (suc m))) (cong ∣_∣ₕ (merid a))) + (cong (·₀ h (suc (suc m))) (cong ∣_∣ₕ (merid a))) + z m ind a = (λ i → EM→ΩEM+1 _ (ind (EM-raw→EM _ _ a) i)) + ∙∙ EM→ΩEM+1-hom _ (·₀ g (suc m) (EM-raw→EM H' (suc m) a)) + (·₀ h (suc m) (EM-raw→EM H' (suc m) a)) + ∙∙ sym (cong₂+₂ m (cong (·₀ g (suc (suc m))) (cong ∣_∣ₕ (merid a))) + (cong (·₀ h (suc (suc m))) (cong ∣_∣ₕ (merid a)))) + + ·₀0 : (m : ℕ) → (g : G) → ·₀ g m (0ₖ m) ≡ 0ₖ m + ·₀0 zero = rCancelPrim + ·₀0 (suc zero) g = refl + ·₀0 (suc (suc m)) g = refl + + ·₀'0 : (m : ℕ) (h : H) → ·₀' h m (0ₖ m) ≡ 0ₖ m + ·₀'0 zero = lCancelPrim + ·₀'0 (suc zero) g = refl + ·₀'0 (suc (suc m)) g = refl + + 0·₀ : (m : ℕ) → (x : _) → ·₀ 0G m x ≡ 0ₖ m + 0·₀ = + elim+2 lCancelPrim + (elimSet _ (λ _ → emsquash _ _) + refl + λ g → compPathR→PathP ((sym (emloop-1g _) + ∙ cong emloop (sym (lCancelPrim g))) + ∙∙ (λ i → rUnit (rUnit (cong (·₀ 0G 1) (emloop g)) i) i) + ∙∙ sym (∙assoc _ _ _))) + λ n f → trElim (λ _ → isOfHLevelTruncPath) + λ { north → refl + ; south → refl + ; (merid a i) j → (cong (EM→ΩEM+1 (suc n)) (f (EM-raw→EM _ _ a)) + ∙ EM→ΩEM+1-0ₖ _) j i} + + 0·₀' : (m : ℕ) (g : _) → ·₀' 0H m g ≡ 0ₖ m + 0·₀' = + elim+2 + rCancelPrim + (elimSet _ (λ _ → emsquash _ _) + refl + λ g → compPathR→PathP (sym (∙assoc _ _ _ + ∙∙ sym (rUnit _) ∙ sym (rUnit _) + ∙∙ (cong emloop (rCancelPrim g) + ∙ emloop-1g _)))) + λ n f → trElim (λ _ → isOfHLevelTruncPath) + λ { north → refl + ; south → refl + ; (merid a i) j → (cong (EM→ΩEM+1 (suc n)) (f (EM-raw→EM _ _ a)) + ∙ EM→ΩEM+1-0ₖ _) j i} + + +-- Definition of the cup product + cup∙ : ∀ n m → EM G' n → EM∙ H' m →∙ EM∙ (G' ⨂ H') (n +' m) + cup∙ = + ℕelim + (λ m g → (·₀ g m) , ·₀0 m g) + λ n f → + ℕelim + (λ g → (λ h → ·₀' h (suc n) g) , 0·₀' (suc n) g) + λ m _ → main n m f + + where + main : (n m : ℕ) (ind : ((m : ℕ) → EM G' n → EM∙ H' m →∙ EM∙ (G' ⨂ H') (n +' m))) + → EM G' (suc n) → EM∙ H' (suc m) →∙ EM∙ (G' ⨂ H') (suc (suc (n + m))) + main zero m ind = + elimGroupoid _ (λ _ → isOfHLevel↑∙ _ _) + ((λ _ → 0ₖ (2 + m)) , refl) + (f m) + λ n h → finalpp m n h + where + f : (m : ℕ) → G → typ (Ω (EM∙ H' (suc m) →∙ EM∙ (G' ⨂ H') (suc (suc m)) ∙)) + fst (f m g i) x = EM→ΩEM+1 _ (·₀ g _ x) i + snd (f zero g i) j = EM→ΩEM+1-0ₖ (suc zero) j i + snd (f (suc m) g i) j = EM→ΩEM+1-0ₖ (suc (suc m)) j i + + f-hom-fst : (m : ℕ) (g h : G) → cong fst (f m (g +G h)) ≡ cong fst (f m g ∙ f m h) + f-hom-fst m g h = + (λ i j x → EM→ΩEM+1 _ (·₀-distr g h (suc m) x i) j) + ∙∙ (λ i j x → EM→ΩEM+1-hom _ (·₀ g (suc m) x) (·₀ h (suc m) x) i j) + ∙∙ sym (cong-∙ fst (f m g) (f m h)) + + f-hom : (m : ℕ) (g h : G) → f m (g +G h) ≡ f m g ∙ f m h + f-hom m g h = →∙Homogeneous≡Path (isHomogeneousEM _) _ _ (f-hom-fst m g h) + + finalpp : (m : ℕ) (g h : G) → PathP (λ i → f m g i ≡ f m (g +G h) i) refl (f m h) + finalpp m g h = + compPathR→PathP (sym (rCancel _) + ∙∙ cong (_∙ sym (f m (g +G h))) (f-hom m g h) + ∙∙ sym (∙assoc _ _ _)) + + main (suc n) m ind = + trElim (λ _ → isOfHLevel↑∙ (2 + n) m) + λ { north → (λ _ → 0ₖ (3 + (n + m))) , refl + ; south → (λ _ → 0ₖ (3 + (n + m))) , refl + ; (merid a i) → Iso.inv (ΩfunExtIso _ _) + (EM→ΩEM+1∙ _ ∘∙ ind (suc m) (EM-raw→EM _ _ a)) i} + + _⌣ₖ_ : {n m : ℕ} (x : EM G' n) (y : EM H' m) → EM (G' ⨂ H') (n +' m) + _⌣ₖ_ x y = cup∙ _ _ x .fst y + + ⌣ₖ-0ₖ : (n m : ℕ) (x : EM G' n) → (x ⌣ₖ 0ₖ m) ≡ 0ₖ (n +' m) + ⌣ₖ-0ₖ n m x = cup∙ n m x .snd + + 0ₖ-⌣ₖ : (n m : ℕ) (x : EM H' m) → ((0ₖ n) ⌣ₖ x) ≡ 0ₖ (n +' m) + 0ₖ-⌣ₖ zero m = 0·₀ _ + 0ₖ-⌣ₖ (suc zero) zero x = refl + 0ₖ-⌣ₖ (suc (suc n)) zero x = refl + 0ₖ-⌣ₖ (suc zero) (suc m) x = refl + 0ₖ-⌣ₖ (suc (suc n)) (suc m) x = refl + +module LeftDistributivity {G' : AbGroup ℓ} {H' : AbGroup ℓ'} where + private + distrl1 : (n m : ℕ) → EM H' m → EM H' m + → EM∙ G' n →∙ EM∙ (G' ⨂ H') (n +' m) + fst (distrl1 n m x y) z = z ⌣ₖ (x +ₖ y) + snd (distrl1 n m x y) = 0ₖ-⌣ₖ n m _ + + distrl2 : (n m : ℕ) → EM H' m → EM H' m + → EM∙ G' n →∙ EM∙ (G' ⨂ H') (n +' m) + fst (distrl2 n m x y) z = (z ⌣ₖ x) +ₖ (z ⌣ₖ y) + snd (distrl2 n m x y) = + cong₂ _+ₖ_ (0ₖ-⌣ₖ n m x) (0ₖ-⌣ₖ n m y) ∙ rUnitₖ _ (0ₖ (n +' m)) + + hLevLem : (n m : ℕ) → isOfHLevel (suc (suc m)) (EM∙ G' (suc n) →∙ EM∙ (G' ⨂ H') ((suc n) +' m)) + hLevLem n m = + subst (isOfHLevel (suc (suc m))) + (λ i → EM∙ G' (suc n) →∙ EM∙ (G' ⨂ H') + ((cong suc (+-comm m n) ∙ sym (+'≡+ (suc n) m)) i)) (isOfHLevel↑∙ m n) + + mainDistrL : (n m : ℕ) (x y : EM H' (suc m)) + → distrl1 (suc n) (suc m) x y ≡ distrl2 (suc n) (suc m) x y + mainDistrL n zero = + wedgeConEM.fun H' H' 0 0 + (λ _ _ → hLevLem _ _ _ _) + (λ x → →∙Homogeneous≡ (isHomogeneousEM _) + (funExt λ z → l x z)) + (λ y → →∙Homogeneous≡ (isHomogeneousEM _) + (funExt λ z → r y z )) + λ i → →∙Homogeneous≡ (isHomogeneousEM (suc (suc (n + 0)))) + (funExt (λ z → l≡r z i)) + where + l : (x : EM H' 1) (z : _) + → (distrl1 (suc n) 1 embase x .fst z) ≡ (distrl2 (suc n) 1 embase x .fst z) + l x z = cong (z ⌣ₖ_) (lUnitₖ _ x) + ∙∙ sym (lUnitₖ _ (z ⌣ₖ x)) + ∙∙ λ i → (⌣ₖ-0ₖ (suc n) (suc zero) z (~ i)) +ₖ (z ⌣ₖ x) + + r : (z : EM H' 1) (x : EM G' (suc n)) + → (distrl1 (suc n) 1 z embase .fst x) ≡ (distrl2 (suc n) 1 z embase .fst x) + r y z = cong (z ⌣ₖ_) (rUnitₖ _ y) + ∙∙ sym (rUnitₖ _ (z ⌣ₖ y)) + ∙∙ λ i → (z ⌣ₖ y) +ₖ (⌣ₖ-0ₖ (suc n) (suc zero) z (~ i)) + + l≡r : (z : EM G' (suc n)) → l embase z ≡ r embase z + l≡r z = sym (pathTypeMake _ _ (sym (⌣ₖ-0ₖ (suc n) (suc zero) z))) + + mainDistrL n (suc m) = + elim2 (λ _ _ → isOfHLevelPath (4 + m) (hLevLem _ _) _ _) + (wedgeConEM.fun H' H' (suc m) (suc m) + (λ x y p q → isOfHLevelPlus {n = suc (suc m)} (suc m) + (hLevLem n (suc (suc m)) + (distrl1 (suc n) (suc (suc m)) ∣ x ∣ ∣ y ∣) + (distrl2 (suc n) (suc (suc m)) ∣ x ∣ ∣ y ∣) p q)) + (λ x → →∙Homogeneous≡ (isHomogeneousEM _) + (funExt (l x))) + (λ x → →∙Homogeneous≡ (isHomogeneousEM _) + (funExt (r x))) + λ i → →∙Homogeneous≡ (isHomogeneousEM _) + (funExt (λ z → l≡r z i))) + where + l : (x : EM-raw H' (suc (suc m))) (z : EM G' (suc n)) + → (distrl1 (suc n) (suc (suc m)) (0ₖ _) ∣ x ∣ₕ .fst z) + ≡ (distrl2 (suc n) (suc (suc m)) (0ₖ _) ∣ x ∣ₕ .fst z) + l x z = cong (z ⌣ₖ_) (lUnitₖ (suc (suc m)) ∣ x ∣) + ∙∙ sym (lUnitₖ _ (z ⌣ₖ ∣ x ∣)) + ∙∙ λ i → (⌣ₖ-0ₖ (suc n) (suc (suc m)) z (~ i)) +ₖ (z ⌣ₖ ∣ x ∣) + + r : (x : EM-raw H' (suc (suc m))) (z : EM G' (suc n)) + → (distrl1 (suc n) (suc (suc m)) ∣ x ∣ₕ (0ₖ _) .fst z) + ≡ (distrl2 (suc n) (suc (suc m)) ∣ x ∣ₕ (0ₖ _) .fst z) + r x z = cong (z ⌣ₖ_) (rUnitₖ (suc (suc m)) ∣ x ∣) + ∙∙ sym (rUnitₖ _ (z ⌣ₖ ∣ x ∣)) + ∙∙ λ i → (z ⌣ₖ ∣ x ∣) +ₖ (⌣ₖ-0ₖ (suc n) (suc (suc m)) z (~ i)) + + l≡r : (z : EM G' (suc n)) → l north z ≡ r north z + l≡r z = sym (pathTypeMake _ _ (sym (⌣ₖ-0ₖ (suc n) (suc (suc m)) z))) + +module RightDistributivity {G' : AbGroup ℓ} {H' : AbGroup ℓ'} where + private + G = fst G' + H = fst H' + + strG = snd G' + strH = snd H' + + 0G = 0g strG + 0H = 0g strH + + _+G_ = _+Gr_ strG + _+H_ = _+Gr_ strH + + -H_ = -Gr_ strH + -G_ = -Gr_ strG + + + distrr1 : (n m : ℕ) → EM G' n → EM G' n → EM∙ H' m →∙ EM∙ (G' ⨂ H') (n +' m) + fst (distrr1 n m x y) z = (x +ₖ y) ⌣ₖ z + snd (distrr1 n m x y) = ⌣ₖ-0ₖ n m _ + + distrr2 : (n m : ℕ) → EM G' n → EM G' n → EM∙ H' m →∙ EM∙ (G' ⨂ H') (n +' m) + fst (distrr2 n m x y) z = (x ⌣ₖ z) +ₖ (y ⌣ₖ z) + snd (distrr2 n m x y) = cong₂ _+ₖ_ (⌣ₖ-0ₖ n m x) (⌣ₖ-0ₖ n m y) ∙ rUnitₖ _ (0ₖ (n +' m)) + + mainDistrR : (n m : ℕ) (x y : EM G' (suc n)) + → distrr1 (suc n) (suc m) x y ≡ distrr2 (suc n) (suc m) x y + mainDistrR zero m = + wedgeConEM.fun G' G' 0 0 + (λ _ _ → isOfHLevel↑∙ 1 m _ _) + (λ x → →∙Homogeneous≡ (isHomogeneousEM _) + (funExt (l x))) + (λ x → →∙Homogeneous≡ (isHomogeneousEM _) + (funExt (r x))) + λ i → →∙Homogeneous≡ (isHomogeneousEM _) + (funExt λ z → l≡r z i) + where + l : (x : _) (z : _) → _ ≡ _ + l x z = + (λ i → (lUnitₖ 1 x i) ⌣ₖ z) + ∙∙ sym (lUnitₖ _ (x ⌣ₖ z)) + ∙∙ λ i → 0ₖ-⌣ₖ _ _ z (~ i) +ₖ (x ⌣ₖ z) + + r : (x : _) (z : _) → _ ≡ _ + r x z = + ((λ i → (rUnitₖ 1 x i) ⌣ₖ z)) + ∙∙ sym (rUnitₖ _ _) + ∙∙ λ i → (_⌣ₖ_ {n = 1} {m = suc m} x z) +ₖ 0ₖ-⌣ₖ (suc zero) (suc m) z (~ i) + + l≡r : (z : _) → l embase z ≡ r embase z + l≡r z = pathTypeMake _ _ _ + + mainDistrR (suc n) m = + elim2 (λ _ _ → isOfHLevelPath (4 + n) + (isOfHLevel↑∙ (2 + n) m) _ _) + (wedgeConEM.fun _ _ _ _ + (λ x y → isOfHLevelPath ((2 + n) + (2 + n)) + (transport (λ i → isOfHLevel (((λ i → (+-comm n 2 (~ i) + (2 + n))) + ∙ sym (+-assoc n 2 (2 + n))) (~ i)) + (EM∙ H' (suc m) →∙ EM∙ ((fst (AbGroupPath (G' ⨂ H') (H' ⨂ G'))) ⨂-comm (~ i)) + ((+'-comm (suc m) (suc (suc n))) i))) + (isOfHLevelPlus n + (LeftDistributivity.hLevLem m (suc (suc n))))) _ _) + (λ x → →∙Homogeneous≡ (isHomogeneousEM _) + (funExt (l x))) + (λ x → →∙Homogeneous≡ (isHomogeneousEM _) + (funExt (r x))) + λ i → →∙Homogeneous≡ (isHomogeneousEM _) + (funExt λ z → r≡l z i)) + where + l : (x : _) (z : _) → _ ≡ _ + l x z = (λ i → (lUnitₖ _ ∣ x ∣ i) ⌣ₖ z) + ∙∙ sym (lUnitₖ _ (∣ x ∣ ⌣ₖ z)) + ∙∙ λ i → 0ₖ-⌣ₖ _ _ z (~ i) +ₖ (∣ x ∣ ⌣ₖ z) + + r : (x : _) (z : _) → _ ≡ _ + r x z = (λ i → (rUnitₖ _ ∣ x ∣ i) ⌣ₖ z) + ∙∙ sym (rUnitₖ _ (∣ x ∣ ⌣ₖ z)) + ∙∙ λ i → (∣ x ∣ ⌣ₖ z) +ₖ 0ₖ-⌣ₖ _ _ z (~ i) + + r≡l : (z : _) → l north z ≡ r north z + r≡l z = pathTypeMake _ _ _ + +-- TODO: Summarise distributivity proofs +-- TODO: Associativity and graded commutativity, following Cubical.ZCohomology.RingStructure +-- The following lemmas will be needed to make the types match up. diff --git a/Cubical/Algebra/Group/EilenbergMacLane/GroupStructure.agda b/Cubical/Algebra/Group/EilenbergMacLane/GroupStructure.agda new file mode 100644 index 000000000..0eed521de --- /dev/null +++ b/Cubical/Algebra/Group/EilenbergMacLane/GroupStructure.agda @@ -0,0 +1,415 @@ +{-# OPTIONS --safe --experimental-lossy-unification #-} + +module Cubical.Algebra.Group.EilenbergMacLane.GroupStructure where + +open import Cubical.Algebra.Group.EilenbergMacLane.Base +open import Cubical.Algebra.Group.EilenbergMacLane.WedgeConnectivity +open import Cubical.Algebra.Group.Base +open import Cubical.Algebra.Group.Properties +open import Cubical.Algebra.AbGroup.Base + +open import Cubical.Data.Nat + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.GroupoidLaws renaming (assoc to ∙assoc) +open import Cubical.Foundations.HLevels +open import Cubical.Foundations.Pointed +open import Cubical.Foundations.Path + +open import Cubical.Homotopy.Loopspace + +open import Cubical.HITs.EilenbergMacLane1 +open import Cubical.HITs.Truncation + renaming (elim to trElim ; rec to trRec ; rec2 to trRec2) +open import Cubical.HITs.Susp + +open import Cubical.Functions.Morphism + +private + variable ℓ : Level + +module _ {G : AbGroup ℓ} where + infixr 34 _+ₖ_ + infixr 34 _-ₖ_ + open AbGroupStr (snd G) renaming (_+_ to _+G_ ; -_ to -G_ ; assoc to assocG) + + private + help : (n : ℕ) → n + (4 + n) ≡ (2 + n) + (2 + n) + help n = +-suc n (3 + n) ∙ cong suc (+-suc n (suc (suc n))) + + hLevHelp : (n : ℕ) → isOfHLevel ((2 + n) + (2 + n)) (EM G (2 + n)) + hLevHelp n = + transport (λ i → isOfHLevel (help n i) (EM G (2 + n))) + (isOfHLevelPlus {n = 4 + n} n (isOfHLevelTrunc (4 + n))) + + helper : (g h : fst G) + → PathP (λ i → Path (EM₁ (AbGroup→Group G)) + (emloop h i) (emloop h i)) (emloop g) (emloop g) + helper g h = + comm→PathP + ((sym (emloop-comp _ h g) + ∙∙ cong emloop (comm h g) + ∙∙ emloop-comp _ g h)) + + _+ₖ_ : {n : ℕ} → EM G n → EM G n → EM G n + _+ₖ_ {n = zero} = _+G_ + _+ₖ_ {n = suc zero} = + rec _ (isGroupoidΠ (λ _ → emsquash)) + (λ x → x) + (λ x → funExt (looper x)) + λ g h i j x → el g h x i j + where + looper : fst G → (x : _) → x ≡ x + looper g = (elimSet _ (λ _ → emsquash _ _) + (emloop g) + (helper g)) + + el : (g h : fst G) (x : EM₁ (AbGroup→Group G)) + → Square (looper g x) + (looper (g +G h) x) + refl (looper h x) + el g h = + elimProp _ (λ _ → isOfHLevelPathP' 1 (emsquash _ _) _ _) + (emcomp g h) + + _+ₖ_ {n = suc (suc n)} = + trRec2 (isOfHLevelTrunc (4 + n)) + (wedgeConEM.fun G G (suc n) (suc n) + (λ _ _ → hLevHelp n) + ∣_∣ ∣_∣ refl) + + σ-EM : (n : ℕ) → EM-raw G (suc n) → Path (EM-raw G (2 + n)) ptEM-raw ptEM-raw + σ-EM n x = merid x ∙ sym (merid ptEM-raw) + + -ₖ_ : {n : ℕ} → EM G n → EM G n + -ₖ_ {n = zero} x = -G x + -ₖ_ {n = suc zero} = + rec _ emsquash + embase + (λ g → sym (emloop g)) + λ g h → sym (emloop-sym _ g) + ◁ (flipSquare + (flipSquare (emcomp (-G g) (-G h)) + ▷ emloop-sym _ h) + ▷ (cong emloop (comm (-G g) (-G h) + ∙ sym (GroupTheory.invDistr (AbGroup→Group G) g h)) + ∙ emloop-sym _ (g +G h))) + -ₖ_ {n = suc (suc n)} = + map λ { north → north + ; south → north + ; (merid a i) → σ-EM n a (~ i)} + + _-ₖ_ : {n : ℕ} → EM G n → EM G n → EM G n + _-ₖ_ {n = n} x y = _+ₖ_ {n = n} x (-ₖ_ {n = n} y) + + +ₖ-syntax : (n : ℕ) → EM G n → EM G n → EM G n + +ₖ-syntax n = _+ₖ_ {n = n} + + -ₖ-syntax : (n : ℕ) → EM G n → EM G n + -ₖ-syntax n = -ₖ_ {n = n} + + -'ₖ-syntax : (n : ℕ) → EM G n → EM G n → EM G n + -'ₖ-syntax n = _-ₖ_ {n = n} + + syntax +ₖ-syntax n x y = x +[ n ]ₖ y + syntax -ₖ-syntax n x = -[ n ]ₖ x + syntax -'ₖ-syntax n x y = x -[ n ]ₖ y + + lUnitₖ : (n : ℕ) (x : EM G n) → 0ₖ n +[ n ]ₖ x ≡ x + lUnitₖ zero x = lid x + lUnitₖ (suc zero) _ = refl + lUnitₖ (suc (suc n)) = + trElim (λ _ → isOfHLevelTruncPath {n = 4 + n}) + λ _ → refl + + rUnitₖ : (n : ℕ) (x : EM G n) → x +[ n ]ₖ 0ₖ n ≡ x + rUnitₖ zero x = rid x + rUnitₖ (suc zero) = + elimSet _ (λ _ → emsquash _ _) + refl + λ _ _ → refl + rUnitₖ (suc (suc n)) = + trElim (λ _ → isOfHLevelTruncPath {n = 4 + n}) + (wedgeConEM.right G G (suc n) (suc n) + (λ _ _ → hLevHelp n) + ∣_∣ ∣_∣ refl) + + commₖ : (n : ℕ) (x y : EM G n) → x +[ n ]ₖ y ≡ y +[ n ]ₖ x + commₖ zero = comm + commₖ (suc zero) = + wedgeConEM.fun G G 0 0 (λ _ _ → emsquash _ _) + (λ x → sym (rUnitₖ 1 x)) + (rUnitₖ 1) + refl + commₖ (suc (suc n)) = + elim2 (λ _ _ → isOfHLevelTruncPath {n = 4 + n}) + (wedgeConEM.fun G G _ _ (λ _ _ → isOfHLevelPath ((2 + n) + (2 + n)) (hLevHelp n) _ _) + (λ x → sym (rUnitₖ (2 + n) ∣ x ∣)) + (λ x → rUnitₖ (2 + n) ∣ x ∣) + refl) + + cong₂+₁ : (p q : typ (Ω (EM∙ G 1))) + → cong₂ (λ x y → x +[ 1 ]ₖ y) p q ≡ p ∙ q + cong₂+₁ p q = + (cong₂Funct (λ x y → x +[ 1 ]ₖ y) p q) + ∙ (λ i → (cong (λ x → rUnitₖ 1 x i) p) ∙ (cong (λ x → lUnitₖ 1 x i) q)) + + cong₂+₂ : (n : ℕ) (p q : typ (Ω (EM∙ G (suc (suc n))))) + → cong₂ (λ x y → x +[ (2 + n) ]ₖ y) p q ≡ p ∙ q + cong₂+₂ n p q = + (cong₂Funct (λ x y → x +[ (2 + n) ]ₖ y) p q) + ∙ (λ i → (cong (λ x → rUnitₖ (2 + n) x i) p) ∙ (cong (λ x → lUnitₖ (2 + n) x i) q)) + + isCommΩEM : (n : ℕ) (p q : typ (Ω (EM∙ G (suc n)))) → p ∙ q ≡ q ∙ p + isCommΩEM zero p q = + sym (cong₂+₁ p q) + ∙∙ (λ i j → commₖ 1 (p j) (q j) i) + ∙∙ cong₂+₁ q p + isCommΩEM (suc n) p q = + (sym (cong₂+₂ n p q) + ∙∙ (λ i j → commₖ (suc (suc n)) (p j) (q j) i) + ∙∙ cong₂+₂ n q p) + + cong-₁ : (p : typ (Ω (EM∙ G 1))) → cong (λ x → -[ 1 ]ₖ x) p ≡ sym p + cong-₁ p = main embase p + where + decoder : (x : EM G 1) → embase ≡ x → x ≡ embase + decoder = + elimSet _ + (λ _ → isSetΠ λ _ → emsquash _ _) + (λ p i → -[ 1 ]ₖ (p i)) + λ g → toPathP + (funExt λ x → + (λ i → transport (λ i → Path (EM G 1) (emloop g i) embase) + (cong (-ₖ_ {n = 1}) + (transp (λ j → Path (EM G 1) embase (emloop g (~ j ∧ ~ i))) i + (compPath-filler x (sym (emloop g)) i) ))) + ∙∙ (λ i → transp (λ j → Path (EM G 1) (emloop g (i ∨ j)) embase) i + (compPath-filler' + (sym (emloop g)) + (cong-∙ (-ₖ_ {n = 1}) + x (sym (emloop g)) i) i)) + ∙∙ (cong (sym (emloop g) ∙_) (isCommΩEM 0 (cong (-ₖ_ {n = 1}) x) (emloop g))) + ∙∙ ∙assoc _ _ _ + ∙∙ cong (_∙ (cong (-ₖ_ {n = 1}) x)) (lCancel (emloop g)) + ∙ sym (lUnit _)) + + main : (x : EM G 1) (p : embase ≡ x) → decoder x p ≡ sym p + main x = J (λ x p → decoder x p ≡ sym p) refl + + cong-₂ : (n : ℕ) (p : typ (Ω (EM∙ G (2 + n)))) + → cong (λ x → -[ 2 + n ]ₖ x) p ≡ sym p + cong-₂ n p = main _ p + where + pp : (a : _) + → PathP (λ i → 0ₖ (suc (suc n)) ≡ ∣ merid a i ∣ₕ → ∣ merid a i ∣ₕ ≡ 0ₖ (2 + n)) + (cong (λ x → -[ 2 + n ]ₖ x)) + λ p → cong ∣_∣ₕ (sym (merid ptEM-raw)) ∙ cong (λ x → -[ 2 + n ]ₖ x) p + pp a = + toPathP + (funExt λ x → + (λ k → transp (λ i → Path (EM G (2 + n)) ∣ merid a (i ∨ k) ∣ ∣ ptEM-raw ∣) k + (compPath-filler' (cong ∣_∣ₕ (sym (merid a))) + (cong (-ₖ-syntax (suc (suc n))) + (transp (λ j → Path (EM G (2 + n)) ∣ ptEM-raw ∣ ∣ merid a (~ j ∧ ~ k) ∣) k + (compPath-filler x (sym (cong ∣_∣ₕ (merid a))) k))) k)) + ∙∙ cong (cong ∣_∣ₕ (sym (merid a)) ∙_) + (cong-∙ (λ x → -[ 2 + n ]ₖ x) x (sym (cong ∣_∣ₕ (merid a))) + ∙ isCommΩEM (suc n) (cong (λ x → -[ 2 + n ]ₖ x) x) (cong ∣_∣ₕ (σ-EM n a))) + ∙∙ (λ k → (λ i → ∣ merid a (~ i ∨ k) ∣) + ∙ (λ i → ∣ compPath-filler' (merid a) (sym (merid ptEM-raw)) (~ k) i ∣) + ∙ cong (λ x → -ₖ-syntax (suc (suc n)) x) x) + ∙ sym (lUnit _)) + + decoder : (x : EM G (2 + n)) + → 0ₖ (2 + n) ≡ x → x ≡ 0ₖ (2 + n) + decoder = + trElim (λ _ → isOfHLevelΠ (4 + n) λ _ → isOfHLevelTruncPath {n = 4 + n}) + λ { north → pp ptEM-raw i0 + ; south → pp ptEM-raw i1 + ; (merid a i) → pp a i} + + main : (x : EM G (2 + n)) (p : 0ₖ (2 + n) ≡ x) → decoder x p ≡ sym p + main x = J (λ x p → decoder x p ≡ sym p) refl + + rCancelₖ : (n : ℕ) (x : EM G n) → x +[ n ]ₖ (-[ n ]ₖ x) ≡ 0ₖ n + rCancelₖ zero x = invr x + rCancelₖ (suc zero) = + elimSet _ (λ _ → emsquash _ _) + refl + λ g → flipSquare (cong₂+₁ (emloop g) (λ i → -ₖ-syntax 1 (emloop g i)) + ∙ rCancel (emloop g)) + rCancelₖ (suc (suc n)) = + trElim (λ _ → isOfHLevelTruncPath {n = 4 + n}) + λ { north → refl + ; south i → +ₖ-syntax (suc (suc n)) ∣ merid ptEM-raw (~ i) ∣ + (-ₖ-syntax (suc (suc n)) ∣ merid ptEM-raw (~ i) ∣) + ; (merid a i) j + → hcomp (λ r → λ { (i = i0) → 0ₖ (2 + n) + ; (i = i1) → ∣ merid ptEM-raw (~ j ∧ r) ∣ₕ -[ 2 + n ]ₖ ∣ merid ptEM-raw (~ j ∧ r) ∣ + ; (j = i0) → ∣ compPath-filler (merid a) (sym (merid ptEM-raw)) (~ r) i ∣ + -[ 2 + n ]ₖ ∣ compPath-filler (merid a) (sym (merid ptEM-raw)) (~ r) i ∣ + ; (j = i1) → 0ₖ (2 + n)}) + (help' a j i) } + where + help' : (a : _) + → cong₂ (λ x y → ∣ x ∣ -[ suc (suc n) ]ₖ ∣ y ∣) (σ-EM n a) (σ-EM n a) ≡ refl + help' a = + cong₂+₂ n (cong ∣_∣ₕ (σ-EM n a)) (cong (λ x → -[ 2 + n ]ₖ ∣ x ∣) (σ-EM n a)) + ∙∙ cong (cong ∣_∣ₕ (σ-EM n a) ∙_) (cong-₂ n (cong ∣_∣ₕ (σ-EM n a))) + ∙∙ rCancel _ + + lCancelₖ : (n : ℕ) (x : EM G n) → (-[ n ]ₖ x) +[ n ]ₖ x ≡ 0ₖ n + lCancelₖ n x = commₖ n (-[ n ]ₖ x) x ∙ rCancelₖ n x + + assocₖ : (n : ℕ) (x y z : EM G n) + → (x +[ n ]ₖ (y +[ n ]ₖ z) ≡ (x +[ n ]ₖ y) +[ n ]ₖ z) + assocₖ zero = assocG + assocₖ (suc zero) = + elimSet _ (λ _ → isSetΠ2 λ _ _ → emsquash _ _) + (λ _ _ → refl) + λ g i y z k → lem g y z k i + where + lem : (g : fst G) (y z : _) + → cong (λ x → x +[ suc zero ]ₖ (y +[ suc zero ]ₖ z)) (emloop g) + ≡ cong (λ x → (x +[ suc zero ]ₖ y) +[ suc zero ]ₖ z) (emloop g) + lem g = + elimProp _ (λ _ → isPropΠ λ _ → emsquash _ _ _ _) + (elimProp _ (λ _ → emsquash _ _ _ _) + refl) + assocₖ (suc (suc n)) = + elim2 (λ _ _ → isOfHLevelΠ (4 + n) λ _ → isOfHLevelTruncPath {n = 4 + n}) + λ a b → trElim (λ _ → isOfHLevelTruncPath {n = 4 + n}) + (λ c → main c a b) + where + lem : (c : _) (a b : _) + → PathP (λ i → (∣ a ∣ₕ +[ suc (suc n) ]ₖ (∣ b ∣ₕ +[ suc (suc n) ]ₖ ∣ merid c i ∣ₕ) + ≡ (∣ a ∣ₕ +[ suc (suc n) ]ₖ ∣ b ∣ₕ) +[ suc (suc n) ]ₖ ∣ merid c i ∣ₕ)) + (cong (λ x → ∣ a ∣ₕ +[ suc (suc n) ]ₖ x) (rUnitₖ (suc (suc n)) ∣ b ∣) + ∙ sym (rUnitₖ (suc (suc n)) (∣ a ∣ₕ +[ suc (suc n) ]ₖ ∣ b ∣ₕ))) + ((λ i → ∣ a ∣ₕ +[ suc (suc n) ]ₖ (∣ b ∣ₕ +[ suc (suc n) ]ₖ ∣ merid ptEM-raw (~ i) ∣ₕ)) + ∙∙ cong (λ x → ∣ a ∣ₕ +[ suc (suc n) ]ₖ x) (rUnitₖ (suc (suc n)) ∣ b ∣) + ∙ sym (rUnitₖ (suc (suc n)) (∣ a ∣ₕ +[ suc (suc n) ]ₖ ∣ b ∣ₕ)) + ∙∙ λ i → (∣ a ∣ₕ +[ suc (suc n) ]ₖ ∣ b ∣ₕ) +[ suc (suc n) ]ₖ ∣ merid ptEM-raw i ∣ₕ) + lem c = + raw-elim G (suc n) + (λ _ → isOfHLevelΠ (2 + n) + (λ _ → isOfHLevelPathP' (2 + n) (isOfHLevelTrunc (4 + n) _ _) _ _)) + (raw-elim G (suc n) + (λ _ → isOfHLevelPathP' (2 + n) (isOfHLevelTrunc (4 + n) _ _) _ _) + ((sym (rUnit refl) + ◁ λ _ → refl) + ▷ (sym (lCancel (cong ∣_∣ₕ (merid ptEM-raw))) + ∙ λ i → (λ j → ∣ merid ptEM-raw (~ j ∨ ~ i) ∣ₕ) + ∙∙ lUnit (λ j → ∣ merid ptEM-raw (~ j ∧ ~ i) ∣ₕ) i + ∙∙ cong ∣_∣ₕ (merid ptEM-raw)))) + main : (c a b : _) + → (∣ a ∣ₕ +[ suc (suc n) ]ₖ (∣ b ∣ₕ +[ suc (suc n) ]ₖ ∣ c ∣ₕ) + ≡ (∣ a ∣ₕ +[ suc (suc n) ]ₖ ∣ b ∣ₕ) +[ suc (suc n) ]ₖ ∣ c ∣ₕ) + main north a b = lem ptEM-raw a b i0 + main south a b = lem ptEM-raw a b i1 + main (merid c i) a b = lem c a b i + + σ-EM' : (n : ℕ) (x : EM G (suc n)) + → Path (EM G (suc (suc n))) + (0ₖ (suc (suc n))) + (0ₖ (suc (suc n))) + σ-EM' zero x = cong ∣_∣ₕ (σ-EM zero x) + σ-EM' (suc n) = + trElim (λ _ → isOfHLevelTrunc (5 + n) _ _) + λ x → cong ∣_∣ₕ (σ-EM (suc n) x) + + σ-EM'-0ₖ : (n : ℕ) → σ-EM' n (0ₖ (suc n)) ≡ refl + σ-EM'-0ₖ zero = cong (cong ∣_∣ₕ) (rCancel (merid ptEM-raw)) + σ-EM'-0ₖ (suc n) = cong (cong ∣_∣ₕ) (rCancel (merid ptEM-raw)) + + private + lUnit-rUnit-coh : ∀ {ℓ} {A : Type ℓ} {x : A} (p : x ≡ x) (r : refl ≡ p) + → lUnit p ∙ cong (_∙ p) r + ≡ rUnit p ∙ cong (p ∙_) r + lUnit-rUnit-coh p = + J (λ p r → lUnit p ∙ cong (_∙ p) r ≡ rUnit p ∙ cong (p ∙_) r) refl + + σ-EM'-hom : (n : ℕ) → (a b : _) → σ-EM' n (a +ₖ b) ≡ σ-EM' n a ∙ σ-EM' n b + σ-EM'-hom zero = + wedgeConEM.fun G G 0 0 (λ _ _ → isOfHLevelTrunc 4 _ _ _ _) l r p + where + l : _ + l x = cong (σ-EM' zero) (lUnitₖ 1 x) + ∙∙ lUnit (σ-EM' zero x) + ∙∙ cong (_∙ σ-EM' zero x) (sym (σ-EM'-0ₖ zero)) + + r : _ + r x = + cong (σ-EM' zero) (rUnitₖ 1 x) + ∙∙ rUnit (σ-EM' zero x) + ∙∙ cong (σ-EM' zero x ∙_) (sym (σ-EM'-0ₖ zero)) + + p : _ + p = lUnit-rUnit-coh (σ-EM' zero embase) (sym (σ-EM'-0ₖ zero)) + σ-EM'-hom (suc n) = + elim2 (λ _ _ → isOfHLevelPath (4 + n) (isOfHLevelTrunc (5 + n) _ _) _ _) + (wedgeConEM.fun G G _ _ + (λ x y → transport (λ i → isOfHLevel (help n i) + ((σ-EM' (suc n) (∣ x ∣ₕ +ₖ ∣ y ∣ₕ) + ≡ σ-EM' (suc n) ∣ x ∣ₕ ∙ σ-EM' (suc n) ∣ y ∣ₕ))) + (isOfHLevelPlus {n = 4 + n} n + (isOfHLevelPath (4 + n) + (isOfHLevelTrunc (5 + n) _ _) _ _))) + (λ x → cong (σ-EM' (suc n)) (lUnitₖ (suc (suc n)) ∣ x ∣) + ∙∙ lUnit (σ-EM' (suc n) ∣ x ∣) + ∙∙ cong (_∙ σ-EM' (suc n) ∣ x ∣) (sym (σ-EM'-0ₖ (suc n)))) + (λ x → cong (σ-EM' (suc n)) (rUnitₖ (2 + n) ∣ x ∣) + ∙∙ rUnit (σ-EM' (suc n) ∣ x ∣) + ∙∙ cong (σ-EM' (suc n) ∣ x ∣ ∙_) (sym (σ-EM'-0ₖ (suc n)))) + (lUnit-rUnit-coh (σ-EM' (suc n) (0ₖ (2 + n))) (sym (σ-EM'-0ₖ (suc n))))) + + σ-EM'-ₖ : (n : ℕ) → (a : _) → σ-EM' n (-ₖ a) ≡ sym (σ-EM' n a) + σ-EM'-ₖ n = + morphLemmas.distrMinus + (λ x y → x +[ suc n ]ₖ y) (_∙_) + (σ-EM' n) (σ-EM'-hom n) + (0ₖ (suc n)) refl + (λ x → -ₖ x) sym + (λ x → sym (lUnit x)) (λ x → sym (rUnit x)) + (lCancelₖ (suc n)) rCancel + ∙assoc (σ-EM'-0ₖ n) + + -Dist : (n : ℕ) (x y : EM G n) → -[ n ]ₖ (x +[ n ]ₖ y) ≡ (-[ n ]ₖ x) +[ n ]ₖ (-[ n ]ₖ y) + -Dist zero x y = (GroupTheory.invDistr (AbGroup→Group G) x y) ∙ commₖ zero _ _ + -Dist (suc zero) = k + where -- useless where clause. Needed for fast type checking for some reason. + l : _ + l x = refl + + r : _ + r x = cong (λ z → -[ 1 ]ₖ z) (rUnitₖ 1 x) ∙ sym (rUnitₖ 1 (-[ 1 ]ₖ x)) + + p : r ptEM-raw ≡ l ptEM-raw + p = sym (rUnit refl) + + k = wedgeConEM.fun G G 0 0 (λ _ _ → emsquash _ _) l r (sym p) + + -Dist (suc (suc n)) = + elim2 (λ _ _ → isOfHLevelTruncPath {n = 4 + n}) + (wedgeConEM.fun G G (suc n) (suc n) + (λ _ _ → isOfHLevelPath ((2 + n) + (2 + n)) (hLevHelp n) _ _) + (λ x → refl) + (λ x → cong (λ z → -[ (suc (suc n)) ]ₖ z) + (rUnitₖ (suc (suc n)) ∣ x ∣ₕ) + ∙ sym (rUnitₖ (suc (suc n)) (-[ (suc (suc n)) ]ₖ ∣ x ∣ₕ))) + (rUnit refl)) + + addIso : (n : ℕ) (x : EM G n) → Iso (EM G n) (EM G n) + Iso.fun (addIso n x) y = y +[ n ]ₖ x + Iso.inv (addIso n x) y = y -[ n ]ₖ x + Iso.rightInv (addIso n x) y = + sym (assocₖ n y (-[ n ]ₖ x) x) + ∙∙ cong (λ x → y +[ n ]ₖ x) (lCancelₖ n x) + ∙∙ rUnitₖ n y + Iso.leftInv (addIso n x) y = + sym (assocₖ n y x (-[ n ]ₖ x)) + ∙∙ cong (λ x → y +[ n ]ₖ x) (rCancelₖ n x) + ∙∙ rUnitₖ n y diff --git a/Cubical/Algebra/Group/EilenbergMacLane/Properties.agda b/Cubical/Algebra/Group/EilenbergMacLane/Properties.agda new file mode 100644 index 000000000..cbc712a7c --- /dev/null +++ b/Cubical/Algebra/Group/EilenbergMacLane/Properties.agda @@ -0,0 +1,539 @@ +{-# OPTIONS --safe --experimental-lossy-unification #-} + +module Cubical.Algebra.Group.EilenbergMacLane.Properties where + +open import Cubical.Algebra.Group.EilenbergMacLane.Base renaming (elim to EM-elim) +open import Cubical.Algebra.Group.EilenbergMacLane.WedgeConnectivity +open import Cubical.Algebra.Group.EilenbergMacLane.GroupStructure +open import Cubical.Algebra.Group.Base +open import Cubical.Algebra.Group.Properties +open import Cubical.Algebra.Group.Morphisms +open import Cubical.Algebra.Group.MorphismProperties +open import Cubical.Algebra.AbGroup.TensorProduct +open import Cubical.Algebra.AbGroup.Base + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.GroupoidLaws renaming (assoc to ∙assoc) +open import Cubical.Foundations.Path +open import Cubical.Foundations.HLevels +open import Cubical.Foundations.Univalence +open import Cubical.Foundations.Pointed +open import Cubical.Foundations.Transport +open import Cubical.Foundations.Pointed.Homogeneous + +open import Cubical.Homotopy.Connected +open import Cubical.Homotopy.Loopspace + +open import Cubical.Functions.Morphism + +open import Cubical.Data.Sigma +open import Cubical.Data.Nat hiding (_·_) + +open import Cubical.HITs.Truncation as Trunc + renaming (rec to trRec; elim to trElim) +open import Cubical.HITs.EilenbergMacLane1 renaming (rec to EMrec) +open import Cubical.HITs.Truncation + renaming (elim to trElim ; rec to trRec ; rec2 to trRec2) +open import Cubical.HITs.Susp + +private + variable ℓ ℓ' ℓ'' : Level + +isConnectedEM₁ : (G : Group ℓ) → isConnected 2 (EM₁ G) +isConnectedEM₁ G = ∣ embase ∣ , h + where + h : (y : hLevelTrunc 2 (EM₁ G)) → ∣ embase ∣ ≡ y + h = trElim (λ y → isOfHLevelSuc 1 (isOfHLevelTrunc 2 ∣ embase ∣ y)) + (elimProp G (λ x → isOfHLevelTrunc 2 ∣ embase ∣ ∣ x ∣) refl) + +module _ {G' : AbGroup ℓ} where + private + G = fst G' + open AbGroupStr (snd G') renaming (_+_ to _+G_) + + + isConnectedEM : (n : ℕ) → isConnected (suc n) (EM G' n) + fst (isConnectedEM zero) = ∣ 0g ∣ + snd (isConnectedEM zero) y = isOfHLevelTrunc 1 _ _ + isConnectedEM (suc zero) = isConnectedEM₁ (AbGroup→Group G') + fst (isConnectedEM (suc (suc n))) = ∣ 0ₖ _ ∣ + snd (isConnectedEM (suc (suc n))) = + trElim (λ _ → isOfHLevelTruncPath) + (trElim (λ _ → isOfHLevelSuc (3 + n) (isOfHLevelTruncPath {n = (3 + n)})) + (raw-elim G' + (suc n) + (λ _ → isOfHLevelTrunc (3 + n) _ _) + refl)) + + +module _ (Ĝ : Group ℓ) where + private + G = fst Ĝ + open GroupStr (snd Ĝ) + + emloop-id : emloop 1g ≡ refl + emloop-id = + emloop 1g ≡⟨ rUnit (emloop 1g) ⟩ + emloop 1g ∙ refl ≡⟨ cong (emloop 1g ∙_) (rCancel (emloop 1g) ⁻¹) ⟩ + emloop 1g ∙ (emloop 1g ∙ (emloop 1g) ⁻¹) ≡⟨ ∙assoc _ _ _ ⟩ + (emloop 1g ∙ emloop 1g) ∙ (emloop 1g) ⁻¹ ≡⟨ cong (_∙ emloop 1g ⁻¹) + ((emloop-comp Ĝ 1g 1g) ⁻¹) ⟩ + emloop (1g · 1g) ∙ (emloop 1g) ⁻¹ ≡⟨ cong (λ g → emloop {Group = Ĝ} g + ∙ (emloop 1g) ⁻¹) + (rid 1g) ⟩ + emloop 1g ∙ (emloop 1g) ⁻¹ ≡⟨ rCancel (emloop 1g) ⟩ + refl ∎ + + emloop-inv : (g : G) → emloop (inv g) ≡ (emloop g) ⁻¹ + emloop-inv g = + emloop (inv g) ≡⟨ rUnit (emloop (inv g)) ⟩ + emloop (inv g) ∙ refl ≡⟨ cong (emloop (inv g) ∙_) + (rCancel (emloop g) ⁻¹) ⟩ + emloop (inv g) ∙ (emloop g ∙ (emloop g) ⁻¹) ≡⟨ ∙assoc _ _ _ ⟩ + (emloop (inv g) ∙ emloop g) ∙ (emloop g) ⁻¹ ≡⟨ cong (_∙ emloop g ⁻¹) + ((emloop-comp Ĝ (inv g) g) ⁻¹) ⟩ + emloop (inv g · g) ∙ (emloop g) ⁻¹ ≡⟨ cong (λ h → emloop {Group = Ĝ} h + ∙ (emloop g) ⁻¹) + (invl g) ⟩ + emloop 1g ∙ (emloop g) ⁻¹ ≡⟨ cong (_∙ (emloop g) ⁻¹) emloop-id ⟩ + refl ∙ (emloop g) ⁻¹ ≡⟨ (lUnit ((emloop g) ⁻¹)) ⁻¹ ⟩ + (emloop g) ⁻¹ ∎ + + isGroupoidEM₁ : isGroupoid (EM₁ Ĝ) + isGroupoidEM₁ = emsquash + + --------- Ω (EM₁ G) ≃ G --------- + + {- since we write composition in diagrammatic order, + and function composition in the other order, + we need right multiplication here -} + rightEquiv : (g : G) → G ≃ G + rightEquiv g = isoToEquiv isom + where + isom : Iso G G + isom .Iso.fun = _· g + isom .Iso.inv = _· inv g + isom .Iso.rightInv h = + (h · inv g) · g ≡⟨ (assoc h (inv g) g) ⁻¹ ⟩ + h · inv g · g ≡⟨ cong (h ·_) (invl g) ⟩ + h · 1g ≡⟨ rid h ⟩ h ∎ + isom .Iso.leftInv h = + (h · g) · inv g ≡⟨ (assoc h g (inv g)) ⁻¹ ⟩ + h · g · inv g ≡⟨ cong (h ·_) (invr g) ⟩ + h · 1g ≡⟨ rid h ⟩ h ∎ + + compRightEquiv : (g h : G) + → compEquiv (rightEquiv g) (rightEquiv h) ≡ rightEquiv (g · h) + compRightEquiv g h = equivEq (funExt (λ x → (assoc x g h) ⁻¹)) + + CodesSet : EM₁ Ĝ → hSet ℓ + CodesSet = EMrec Ĝ (isOfHLevelTypeOfHLevel 2) (G , is-set) RE REComp + where + RE : (g : G) → Path (hSet ℓ) (G , is-set) (G , is-set) + RE g = Σ≡Prop (λ X → isPropIsOfHLevel {A = X} 2) (ua (rightEquiv g)) + + lemma₁ : (g h : G) → Square + (ua (rightEquiv g)) (ua (rightEquiv (g · h))) + refl (ua (rightEquiv h)) + lemma₁ g h = invEq + (Square≃doubleComp (ua (rightEquiv g)) (ua (rightEquiv (g · h))) + refl (ua (rightEquiv h))) + (ua (rightEquiv g) ∙ ua (rightEquiv h) + ≡⟨ (uaCompEquiv (rightEquiv g) (rightEquiv h)) ⁻¹ ⟩ + ua (compEquiv (rightEquiv g) (rightEquiv h)) + ≡⟨ cong ua (compRightEquiv g h) ⟩ + ua (rightEquiv (g · h)) ∎) + + REComp : (g h : G) → Square (RE g) (RE (g · h)) refl (RE h) + REComp g h = ΣSquareSet (λ _ → isProp→isSet isPropIsSet) (lemma₁ g h) + Codes : EM₁ Ĝ → Type ℓ + Codes x = CodesSet x .fst + + encode : (x : EM₁ Ĝ) → embase ≡ x → Codes x + encode x p = subst Codes p 1g + + decode : (x : EM₁ Ĝ) → Codes x → embase ≡ x + decode = elimSet Ĝ (λ x → isOfHLevelΠ 2 (λ c → isGroupoidEM₁ (embase) x)) + emloop λ g → ua→ λ h → emcomp h g + + decode-encode : (x : EM₁ Ĝ) (p : embase ≡ x) → decode x (encode x p) ≡ p + decode-encode x p = J (λ y q → decode y (encode y q) ≡ q) + (emloop (transport refl 1g) ≡⟨ cong emloop (transportRefl 1g) ⟩ + emloop 1g ≡⟨ emloop-id ⟩ refl ∎) p + + encode-decode : (x : EM₁ Ĝ) (c : Codes x) → encode x (decode x c) ≡ c + encode-decode = elimProp Ĝ (λ x → isOfHLevelΠ 1 (λ c → CodesSet x .snd _ _)) + λ g → encode embase (decode embase g) ≡⟨ refl ⟩ + encode embase (emloop g) ≡⟨ refl ⟩ + transport (ua (rightEquiv g)) 1g ≡⟨ uaβ (rightEquiv g) 1g ⟩ + 1g · g ≡⟨ lid g ⟩ + g ∎ + + ΩEM₁Iso : Iso (Path (EM₁ Ĝ) embase embase) G + Iso.fun ΩEM₁Iso = encode embase + Iso.inv ΩEM₁Iso = emloop + Iso.rightInv ΩEM₁Iso = encode-decode embase + Iso.leftInv ΩEM₁Iso = decode-encode embase + + ΩEM₁≡ : (Path (EM₁ Ĝ) embase embase) ≡ G + ΩEM₁≡ = isoToPath ΩEM₁Iso + +--------- Ω (EMₙ₊₁ G) ≃ EMₙ G --------- +module _ {G : AbGroup ℓ} where + open AbGroupStr (snd G) + renaming (_+_ to _+G_ ; -_ to -G_ ; assoc to assocG) + + CODE : (n : ℕ) → EM G (suc (suc n)) → TypeOfHLevel ℓ (3 + n) + CODE n = + trElim (λ _ → isOfHLevelTypeOfHLevel (3 + n)) + λ { north → EM G (suc n) , hLevelEM G (suc n) + ; south → EM G (suc n) , hLevelEM G (suc n) + ; (merid a i) → fib n a i} + where + fib : (n : ℕ) → (a : EM-raw G (suc n)) + → Path (TypeOfHLevel _ (3 + n)) + (EM G (suc n) , hLevelEM G (suc n)) + (EM G (suc n) , hLevelEM G (suc n)) + fib zero a = Σ≡Prop (λ _ → isPropIsOfHLevel 3) + (isoToPath (addIso 1 a)) + fib (suc n) a = Σ≡Prop (λ _ → isPropIsOfHLevel (4 + n)) + (isoToPath (addIso (suc (suc n)) ∣ a ∣)) + + decode' : (n : ℕ) (x : EM G (suc (suc n))) → CODE n x .fst → 0ₖ (suc (suc n)) ≡ x + decode' n = + trElim (λ _ → isOfHLevelΠ (4 + n) + λ _ → isOfHLevelPath (4 + n) (isOfHLevelTrunc (4 + n)) _ _) + λ { north → f n + ; south → g n + ; (merid a i) → main a i} + where + f : (n : ℕ) → _ + f n = σ-EM' n + + g : (n : ℕ) → EM G (suc n) → ∣ ptEM-raw ∣ ≡ ∣ south ∣ + g n x = σ-EM' n x ∙ cong ∣_∣ₕ (merid ptEM-raw) + + lem₂ : (n : ℕ) (a x : _) + → Path (Path (EM G (suc (suc n))) _ _) + ((λ i → cong ∣_∣ₕ (σ-EM n x) i) ∙ sym (cong ∣_∣ₕ (σ-EM n a)) ∙ (λ i → ∣ merid a i ∣ₕ)) + (g n (EM-raw→EM G (suc n) x)) + lem₂ zero a x = + cong (f zero x ∙_) + (cong (_∙ cong ∣_∣ₕ (merid a)) (cong (cong ∣_∣ₕ) (symDistr (merid a) (sym (merid embase))) + ∙ cong-∙ ∣_∣ₕ (merid embase) (sym (merid a))) + ∙∙ sym (∙assoc _ _ _) + ∙∙ cong (cong ∣_∣ₕ (merid embase) ∙_) (lCancel (cong ∣_∣ₕ (merid a))) + ∙ sym (rUnit _)) + lem₂ (suc n) a x = + cong (f (suc n) ∣ x ∣ ∙_) + ((cong (_∙ cong ∣_∣ₕ (merid a)) (cong (cong ∣_∣ₕ) (symDistr (merid a) (sym (merid north))) + ∙ cong-∙ ∣_∣ₕ (merid north) (sym (merid a))) + ∙∙ sym (∙assoc _ _ _) + ∙∙ cong (cong ∣_∣ₕ (merid north) ∙_) (lCancel (cong ∣_∣ₕ (merid a))) + ∙ sym (rUnit _))) + + lem : (n : ℕ) (x a : EM-raw G (suc n)) + → f n (transport (sym (cong (λ x → CODE n x .fst) (cong ∣_∣ₕ (merid a)))) + (EM-raw→EM G (suc n) x)) + ≡ cong ∣_∣ₕ (σ-EM n x) ∙ sym (cong ∣_∣ₕ (σ-EM n a)) + lem zero x a = (λ i → cong ∣_∣ₕ (merid (transportRefl x i -[ 1 ]ₖ a) ∙ sym (merid embase))) + ∙∙ σ-EM'-hom zero x (-ₖ a) + ∙∙ cong (f zero x ∙_) (σ-EM'-ₖ zero a) + lem (suc n) x a = + cong (f (suc n)) (λ i → transportRefl ∣ x ∣ i -[ 2 + n ]ₖ ∣ a ∣) + ∙∙ σ-EM'-hom (suc n) ∣ x ∣ (-ₖ ∣ a ∣) + ∙∙ cong (f (suc n) ∣ x ∣ ∙_) (σ-EM'-ₖ (suc n) ∣ a ∣) + + main : (a : _) + → PathP (λ i → CODE n ∣ merid a i ∣ₕ .fst + → 0ₖ (suc (suc n)) ≡ ∣ merid a i ∣ₕ) (f n) (g n) + main a = + toPathP (funExt + (EM-elim _ (λ _ → isOfHLevelPathP (2 + (suc n)) (isOfHLevelTrunc (4 + n) _ _) _ _) + λ x → + ((λ i → transp (λ j → Path (EM G (2 + n)) ∣ ptEM-raw ∣ ∣ merid a (i ∨ j) ∣) + i (compPath-filler (lem n x a i) (cong ∣_∣ₕ (merid a)) i) )) + ∙∙ sym (∙assoc _ _ _) + ∙∙ lem₂ n a x)) + + encode' : (n : ℕ) (x : EM G (suc (suc n))) → 0ₖ (suc (suc n)) ≡ x → CODE n x .fst + encode' n x p = subst (λ x → CODE n x .fst) p (0ₖ (suc n)) + + decode'-encode' : (n : ℕ) (x : EM G (2 + n)) (p : 0ₖ (2 + n) ≡ x) + → decode' n x (encode' n x p) ≡ p + decode'-encode' zero x = + J (λ x p → decode' 0 x (encode' 0 x p) ≡ p) + (σ-EM'-0ₖ 0) + decode'-encode' (suc n) x = + J (λ x p → decode' (suc n) x (encode' (suc n) x p) ≡ p) + (σ-EM'-0ₖ (suc n)) + + encode'-decode' : (n : ℕ) (x : _) + → encode' n (0ₖ (suc (suc n))) (decode' n (0ₖ (suc (suc n))) x) ≡ x + encode'-decode' zero x = + cong (encode' zero (0ₖ 2)) (cong-∙ ∣_∣ₕ (merid x) (sym (merid embase))) + ∙∙ substComposite (λ x → CODE zero x .fst) + (cong ∣_∣ₕ (merid x)) (sym (cong ∣_∣ₕ (merid ptEM-raw))) embase + ∙∙ (cong (subst (λ x₁ → CODE zero x₁ .fst) (λ i → ∣ merid embase (~ i) ∣ₕ)) + (λ i → lUnitₖ 1 (transportRefl x i) i) + ∙ (λ i → rUnitₖ 1 (transportRefl x i) i)) + encode'-decode' (suc n) = + trElim (λ _ → isOfHLevelTruncPath {n = 4 + n}) + λ x → cong (encode' (suc n) (0ₖ (3 + n))) (cong-∙ ∣_∣ₕ (merid x) (sym (merid north))) + ∙∙ substComposite (λ x → CODE (suc n) x .fst) + (cong ∣_∣ₕ (merid x)) (sym (cong ∣_∣ₕ (merid ptEM-raw))) (0ₖ (2 + n)) + ∙∙ cong (subst (λ x₁ → CODE (suc n) x₁ .fst) (λ i → ∣ merid ptEM-raw (~ i) ∣ₕ)) + (λ i → lUnitₖ (2 + n) (transportRefl ∣ x ∣ₕ i) i) + ∙ (λ i → rUnitₖ (2 + n) (transportRefl ∣ x ∣ₕ i) i) + + Iso-EM-ΩEM+1 : (n : ℕ) → Iso (EM G n) (typ (Ω (EM∙ G (suc n)))) + Iso-EM-ΩEM+1 zero = invIso (ΩEM₁Iso (AbGroup→Group G)) + Iso.fun (Iso-EM-ΩEM+1 (suc zero)) = decode' 0 (0ₖ 2) + Iso.inv (Iso-EM-ΩEM+1 (suc zero)) = encode' 0 (0ₖ 2) + Iso.rightInv (Iso-EM-ΩEM+1 (suc zero)) = decode'-encode' 0 (0ₖ 2) + Iso.leftInv (Iso-EM-ΩEM+1 (suc zero)) = encode'-decode' 0 + Iso.fun (Iso-EM-ΩEM+1 (suc (suc n))) = decode' (suc n) (0ₖ (3 + n)) + Iso.inv (Iso-EM-ΩEM+1 (suc (suc n))) = encode' (suc n) (0ₖ (3 + n)) + Iso.rightInv (Iso-EM-ΩEM+1 (suc (suc n))) = decode'-encode' (suc n) (0ₖ (3 + n)) + Iso.leftInv (Iso-EM-ΩEM+1 (suc (suc n))) = encode'-decode' (suc n) + + EM≃ΩEM+1 : (n : ℕ) → EM G n ≃ typ (Ω (EM∙ G (suc n))) + EM≃ΩEM+1 n = isoToEquiv (Iso-EM-ΩEM+1 n) + + -- Some properties of the isomorphism + EM→ΩEM+1 : (n : ℕ) → EM G n → typ (Ω (EM∙ G (suc n))) + EM→ΩEM+1 n = Iso.fun (Iso-EM-ΩEM+1 n) + + ΩEM+1→EM : (n : ℕ) → typ (Ω (EM∙ G (suc n))) → EM G n + ΩEM+1→EM n = Iso.inv (Iso-EM-ΩEM+1 n) + + EM→ΩEM+1-0ₖ : (n : ℕ) → EM→ΩEM+1 n (0ₖ n) ≡ refl + EM→ΩEM+1-0ₖ zero = emloop-1g _ + EM→ΩEM+1-0ₖ (suc zero) = cong (cong ∣_∣ₕ) (rCancel (merid ptEM-raw)) + EM→ΩEM+1-0ₖ (suc (suc n)) = cong (cong ∣_∣ₕ) (rCancel (merid ptEM-raw)) + + EM→ΩEM+1-hom : (n : ℕ) (x y : EM G n) + → EM→ΩEM+1 n (x +[ n ]ₖ y) ≡ EM→ΩEM+1 n x ∙ EM→ΩEM+1 n y + EM→ΩEM+1-hom zero x y = emloop-comp _ x y + EM→ΩEM+1-hom (suc zero) x y = σ-EM'-hom zero x y + EM→ΩEM+1-hom (suc (suc n)) x y = σ-EM'-hom (suc n) x y + + ΩEM+1→EM-hom : (n : ℕ) → (p q : typ (Ω (EM∙ G (suc n)))) + → ΩEM+1→EM n (p ∙ q) ≡ (ΩEM+1→EM n p) +[ n ]ₖ (ΩEM+1→EM n q) + ΩEM+1→EM-hom n = + morphLemmas.isMorphInv (λ x y → x +[ n ]ₖ y) (_∙_) (EM→ΩEM+1 n) + (EM→ΩEM+1-hom n) (ΩEM+1→EM n) + (Iso.rightInv (Iso-EM-ΩEM+1 n)) (Iso.leftInv (Iso-EM-ΩEM+1 n)) + + ΩEM+1→EM-refl : (n : ℕ) → ΩEM+1→EM n refl ≡ 0ₖ n + ΩEM+1→EM-refl zero = transportRefl 0g + ΩEM+1→EM-refl (suc zero) = refl + ΩEM+1→EM-refl (suc (suc n)) = refl + + EM→ΩEM+1∙ : (n : ℕ) → EM∙ G n →∙ Ω (EM∙ G (suc n)) + EM→ΩEM+1∙ n .fst = EM→ΩEM+1 n + EM→ΩEM+1∙ zero .snd = emloop-1g (AbGroup→Group G) + EM→ΩEM+1∙ (suc zero) .snd = cong (cong ∣_∣ₕ) (rCancel (merid embase)) + EM→ΩEM+1∙ (suc (suc n)) .snd = cong (cong ∣_∣ₕ) (rCancel (merid north)) + + EM≃ΩEM+1∙ : (n : ℕ) → EM∙ G n ≡ Ω (EM∙ G (suc n)) + EM≃ΩEM+1∙ n = ua∙ (EM≃ΩEM+1 n) (EM→ΩEM+1-0ₖ n) + + isHomogeneousEM : (n : ℕ) → isHomogeneous (EM∙ G n) + isHomogeneousEM n x = + ua∙ (isoToEquiv (addIso n x)) (lUnitₖ n x) + + +-- Some HLevel lemmas about function spaces (EM∙ G n →∙ EM∙ H m), mainly used for +-- the cup product +module _ where + open AbGroupStr renaming (_+_ to comp) + + isContr-↓∙ : {G : AbGroup ℓ} {H : AbGroup ℓ'} (n : ℕ) → isContr (EM∙ G (suc n) →∙ EM∙ H n) + fst (isContr-↓∙ {G = G} {H = H} zero) = (λ _ → 0g (snd H)) , refl + snd (isContr-↓∙{G = G} {H = H} zero) (f , p) = + Σ≡Prop (λ x → is-set (snd H) _ _) + (funExt (raw-elim G 0 (λ _ → is-set (snd H) _ _) (sym p))) + fst (isContr-↓∙ {G = G} {H = H} (suc n)) = (λ _ → 0ₖ (suc n)) , refl + fst (snd (isContr-↓∙ {G = G} {H = H} (suc n)) f i) x = + trElim {B = λ x → 0ₖ (suc n) ≡ fst f x} + (λ _ → isOfHLevelPath (4 + n) (isOfHLevelSuc (3 + n) (hLevelEM H (suc n))) _ _) + (raw-elim _ _ (λ _ → hLevelEM H (suc n) _ _) (sym (snd f))) + x i + snd (snd (isContr-↓∙ (suc n)) f i) j = snd f (~ i ∨ j) + + isContr-↓∙' : {G : AbGroup ℓ} {H : AbGroup ℓ'} (n : ℕ) + → isContr ((EM-raw G (suc n) , ptEM-raw) →∙ EM∙ H n) + isContr-↓∙' zero = isContr-↓∙ zero + fst (isContr-↓∙' (suc n)) = (λ _ → 0ₖ (suc n)) , refl + fst (snd (isContr-↓∙' {H = H} (suc n)) f i) x = + raw-elim _ _ {A = λ x → 0ₖ (suc n) ≡ fst f x} + (λ _ → hLevelEM H (suc n) _ _) (sym (snd f)) x i + snd (snd (isContr-↓∙' (suc n)) f i) j = snd f (~ i ∨ j) + + isOfHLevel→∙EM : ∀ {ℓ} {A : Pointed ℓ} {G : AbGroup ℓ'} (n m : ℕ) + → isOfHLevel (suc m) (A →∙ EM∙ G n) + → isOfHLevel (suc (suc m)) (A →∙ EM∙ G (suc n)) + isOfHLevel→∙EM {A = A} {G = G} n m hlev = step₃ + where + step₁ : isOfHLevel (suc m) (A →∙ Ω (EM∙ G (suc n))) + step₁ = + subst (isOfHLevel (suc m)) + (λ i → A →∙ ua∙ {A = Ω (EM∙ G (suc n))} {B = EM∙ G n} + (invEquiv (EM≃ΩEM+1 n)) + (ΩEM+1→EM-refl n) (~ i)) hlev + + step₂ : isOfHLevel (suc m) (typ (Ω (A →∙ EM∙ G (suc n) ∙))) + step₂ = isOfHLevelRetractFromIso (suc m) (invIso (invIso (ΩfunExtIso _ _))) step₁ + + step₃ : isOfHLevel (suc (suc m)) (A →∙ EM∙ G (suc n)) + step₃ = isOfHLevelΩ→isOfHLevel m + λ f → subst (λ x → isOfHLevel (suc m) (typ (Ω x))) + (isHomogeneous→∙ (isHomogeneousEM (suc n)) f) + step₂ + + isOfHLevel↑∙ : {G : AbGroup ℓ} {H : AbGroup ℓ'} + → ∀ n m → isOfHLevel (2 + n) (EM∙ G (suc m) →∙ EM∙ H (suc (n + m))) + isOfHLevel↑∙ zero m = isOfHLevel→∙EM m 0 (isContr→isProp (isContr-↓∙ m)) + isOfHLevel↑∙ (suc n) m = isOfHLevel→∙EM (suc (n + m)) (suc n) (isOfHLevel↑∙ n m) + + isOfHLevel↑∙' : {G : AbGroup ℓ} {H : AbGroup ℓ'} + → ∀ n m → isOfHLevel (2 + n) (EM-raw∙ G (suc m) →∙ EM∙ H (suc (n + m))) + isOfHLevel↑∙' zero m = isOfHLevel→∙EM m 0 (isContr→isProp (isContr-↓∙' m)) + isOfHLevel↑∙' (suc n) m = isOfHLevel→∙EM (suc (n + m)) (suc n) (isOfHLevel↑∙' n m) + + →∙EMPath : ∀ {ℓ} {G : AbGroup ℓ} (A : Pointed ℓ') (n : ℕ) + → Ω (A →∙ EM∙ G (suc n) ∙) ≡ (A →∙ EM∙ G n ∙) + →∙EMPath {G = G} A n = + ua∙ (isoToEquiv (ΩfunExtIso A (EM∙ G (suc n)))) refl + ∙ (λ i → (A →∙ EM≃ΩEM+1∙ {G = G} n (~ i) ∙)) + + private + contr∙-lem : {G : AbGroup ℓ} {H : AbGroup ℓ'} {L : AbGroup ℓ''} (n m : ℕ) + → isContr (EM∙ G (suc n) →∙ (EM∙ H (suc m) →∙ EM∙ L (suc (n + m)) ∙)) + fst (contr∙-lem n m) = (λ _ → (λ _ → 0ₖ _) , refl), refl + snd (contr∙-lem {G = G} {H = H} {L = L} n m) (f , p) = + →∙Homogeneous≡ (isHomogeneous→∙ (isHomogeneousEM _)) + (sym (funExt (help n f p))) + where + help : (n : ℕ) → (f : EM G (suc n) → EM∙ H (suc m) →∙ EM∙ L (suc (n + m))) + → f (snd (EM∙ G (suc n))) ≡ snd (EM∙ H (suc m) →∙ EM∙ L (suc (n + m)) ∙) + → (x : _) → (f x) ≡ ((λ _ → 0ₖ _) , refl) + help zero f p = + raw-elim G zero + (λ _ → isOfHLevel↑∙ zero m _ _) p + help (suc n) f p = + trElim (λ _ → isOfHLevelPath (4 + n) + (subst (λ x → isOfHLevel x (EM∙ H (suc m) →∙ EM∙ L (suc ((suc n) + m)))) + (λ i → suc (suc (+-comm (suc n) 1 i))) + (isOfHLevelPlus' {n = 1} (3 + n) (isOfHLevel↑∙ (suc n) m))) _ _) + (raw-elim G (suc n) + (λ _ → isOfHLevel↑∙ (suc n) m _ _) p) + + isOfHLevel↑∙∙ : {G : AbGroup ℓ} {H : AbGroup ℓ'} {L : AbGroup ℓ''} + → ∀ n m l → isOfHLevel (2 + l) (EM∙ G (suc n) + →∙ (EM∙ H (suc m) + →∙ EM∙ L (suc (suc (l + n + m))) ∙)) + isOfHLevel↑∙∙ {G = G} {H = H} {L = L} n m zero = + isOfHLevelΩ→isOfHLevel 0 λ f + → subst + isProp (cong (λ x → typ (Ω x)) + (isHomogeneous→∙ (isHomogeneous→∙ (isHomogeneousEM _)) f)) + (isOfHLevelRetractFromIso 1 (ΩfunExtIso _ _) h) + where + h : isProp (EM∙ G (suc n) + →∙ (Ω (EM∙ H (suc m) + →∙ EM∙ L (suc (suc (n + m))) ∙))) + h = + subst isProp + (λ i → EM∙ G (suc n) + →∙ (→∙EMPath {G = L} (EM∙ H (suc m)) (suc (n + m)) (~ i))) + (isContr→isProp (contr∙-lem n m)) + isOfHLevel↑∙∙ {G = G} {H = H} {L = L} n m (suc l) = + isOfHLevelΩ→isOfHLevel (suc l) + λ f → + subst (isOfHLevel (2 + l)) + (cong (λ x → typ (Ω x)) + (isHomogeneous→∙ (isHomogeneous→∙ (isHomogeneousEM _)) f)) + (isOfHLevelRetractFromIso (2 + l) (ΩfunExtIso _ _) h) + where + h : isOfHLevel (2 + l) + (EM∙ G (suc n) + →∙ (Ω (EM∙ H (suc m) + →∙ EM∙ L (suc (suc (suc (l + n + m)))) ∙))) + h = + subst (isOfHLevel (2 + l)) + (λ i → EM∙ G (suc n) + →∙ →∙EMPath {G = L} (EM∙ H (suc m)) (suc (suc (l + n + m))) (~ i)) + (isOfHLevel↑∙∙ n m l) + + +-- A homomorphism φ : G → H of AbGroups induces a homomorphism +-- φ' : K(G,n) → K(H,n) +inducedFun-EM-raw : {G' : AbGroup ℓ} {H' : AbGroup ℓ'} + → AbGroupHom G' H' + → ∀ n + → EM-raw G' n → EM-raw H' n +inducedFun-EM-raw f = + elim+2 (fst f) + (EMrec _ emsquash embase + (λ g → emloop (fst f g)) + λ g h → compPathR→PathP (sym + (sym (lUnit _) + ∙∙ cong (_∙ (sym (emloop (fst f h)))) + (cong emloop (IsGroupHom.pres· (snd f) g h) + ∙ emloop-comp _ (fst f g) (fst f h)) + ∙∙ sym (∙assoc _ _ _) + ∙∙ cong (emloop (fst f g) ∙_) (rCancel _) + ∙∙ sym (rUnit _)))) + (λ n ind → λ { north → north + ; south → south + ; (merid a i) → merid (ind a) i} ) + +inducedFun-EM-rawIso : {G' : AbGroup ℓ} {H' : AbGroup ℓ'} + → AbGroupEquiv G' H' + → ∀ n → Iso (EM-raw G' n) (EM-raw H' n) +Iso.fun (inducedFun-EM-rawIso e n) = inducedFun-EM-raw (_ , (snd e)) n +Iso.inv (inducedFun-EM-rawIso e n) = inducedFun-EM-raw (_ , isGroupHomInv e) n +Iso.rightInv (inducedFun-EM-rawIso e n) = h n + where + h : (n : ℕ) → section (inducedFun-EM-raw (fst e .fst , snd e) n) + (inducedFun-EM-raw (invEq (fst e) , isGroupHomInv e) n) + h = elim+2 + (secEq (fst e)) + (elimSet _ (λ _ → emsquash _ _) refl + (λ g → compPathR→PathP + ((sym (cong₂ _∙_ (cong emloop (secEq (fst e) g)) (sym (lUnit _)) + ∙ rCancel _))))) + λ n p → λ { north → refl + ; south → refl + ; (merid a i) k → merid (p a k) i} +Iso.leftInv (inducedFun-EM-rawIso e n) = h n + where + h : (n : ℕ) → retract (Iso.fun (inducedFun-EM-rawIso e n)) + (Iso.inv (inducedFun-EM-rawIso e n)) + h = elim+2 + (retEq (fst e)) + (elimSet _ (λ _ → emsquash _ _) refl + (λ g → compPathR→PathP + ((sym (cong₂ _∙_ (cong emloop (retEq (fst e) g)) (sym (lUnit _)) + ∙ rCancel _))))) + λ n p → λ { north → refl + ; south → refl + ; (merid a i) k → merid (p a k) i} + +Iso→EMIso : {G : AbGroup ℓ} {H : AbGroup ℓ'} + → AbGroupEquiv G H → ∀ n → Iso (EM G n) (EM H n) +Iso→EMIso is zero = inducedFun-EM-rawIso is zero +Iso→EMIso is (suc zero) = inducedFun-EM-rawIso is 1 +Iso→EMIso is (suc (suc n)) = mapCompIso (inducedFun-EM-rawIso is (suc (suc n))) + +EM⊗-commIso : {G : AbGroup ℓ} {H : AbGroup ℓ'} + → ∀ n → Iso (EM (G ⨂ H) n) (EM (H ⨂ G) n) +EM⊗-commIso {G = G} {H = H} = Iso→EMIso (GroupIso→GroupEquiv ⨂-commIso) + +EM⊗-assocIso : {G : AbGroup ℓ} {H : AbGroup ℓ'} {L : AbGroup ℓ''} + → ∀ n → Iso (EM (G ⨂ (H ⨂ L)) n) (EM ((G ⨂ H) ⨂ L) n) +EM⊗-assocIso = Iso→EMIso (GroupIso→GroupEquiv (GroupEquiv→GroupIso ⨂assoc)) diff --git a/Cubical/Algebra/Group/EilenbergMacLane/WedgeConnectivity.agda b/Cubical/Algebra/Group/EilenbergMacLane/WedgeConnectivity.agda new file mode 100644 index 000000000..1a9ae3a27 --- /dev/null +++ b/Cubical/Algebra/Group/EilenbergMacLane/WedgeConnectivity.agda @@ -0,0 +1,285 @@ +{-# OPTIONS --safe --experimental-lossy-unification #-} + +module Cubical.Algebra.Group.EilenbergMacLane.WedgeConnectivity where + +open import Cubical.Algebra.Group.EilenbergMacLane.Base +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.HLevels + +open import Cubical.Algebra.Group.Base +open import Cubical.HITs.Truncation as Trunc renaming (rec to trRec; elim to trElim) +open import Cubical.HITs.EilenbergMacLane1 +open import Cubical.Algebra.AbGroup.Base +open import Cubical.Data.Empty + renaming (rec to ⊥-rec) +open import Cubical.Data.Nat +open import Cubical.HITs.Susp + +{- +This file contains a direct construction of the wedge connectivity lemma for EM +spaces. This direct construction gives nicer reductions and computes better than +the more general theorem. The main results are in the module "wedgeConEM" at the +end of this file. +-} + +private + variable ℓ ℓ' ℓ'' : Level + +-- One of the base cases, stated separately to avoid termination issues + wedgeConFun' : (G : AbGroup ℓ) (H : AbGroup ℓ') (n : ℕ) + → {A : EM-raw G (suc n) → EM-raw H (suc zero) → Type ℓ''} + → ((x : _) (y : _) → isOfHLevel (suc n + suc zero) (A x y)) + → (f : (x : _) → A ptEM-raw x) + → (g : (x : _) → A x ptEM-raw) + → f ptEM-raw ≡ g ptEM-raw + → (x : _) (y : _) → A x y + wedgeConFun'ᵣ : (G : AbGroup ℓ) (H : AbGroup ℓ') (n : ℕ) + → {A : EM-raw G (suc n) → EM-raw H (suc zero) → Type ℓ''} + → (hLev : ((x : _) (y : _) → isOfHLevel (suc n + suc zero) (A x y))) + → (f : (x : _) → A ptEM-raw x) + → (g : (x : _) → A x ptEM-raw) + → (p : f ptEM-raw ≡ g ptEM-raw) + → (x : _) → wedgeConFun' G H n hLev f g p x ptEM-raw ≡ g x + wedgeConFun' G H zero {A = A} hlev f g p = + elimSet _ (λ _ → isSetΠ λ _ → hlev _ _) f mainpath + where + I→A : (x : fst G) → (i : I) → A (emloop x i) embase + I→A x i = + hcomp (λ k → λ {(i = i0) → p (~ k) ; (i = i1) → p (~ k)}) + (g (emloop x i)) + + SquareP2 : (x : _) (z : _) + → SquareP (λ i j → A (emloop x i) (emloop z j)) + (cong f (emloop z)) (cong f (emloop z)) + (λ i → I→A x i) λ i → I→A x i + SquareP2 x z = + toPathP (isOfHLevelPathP' 1 (λ _ _ → hlev _ _ _ _) _ _ _ _) + + CubeP2 : (x : _) (g h : _) + → PathP (λ k → PathP (λ j → PathP (λ i → A (emloop x i) (emcomp g h j k)) + (f (emcomp g h j k)) (f (emcomp g h j k))) + (λ i → SquareP2 x g i k) λ i → SquareP2 x ((snd (AbGroup→Group H) GroupStr.· g) h) i k) + (λ _ i → I→A x i) λ j i → SquareP2 x h i j + CubeP2 x g h = toPathP (isOfHLevelPathP' 1 (isOfHLevelPathP 2 (hlev _ _) _ _) _ _ _ _) + + mainpath : (x : _) → PathP (λ i → (y : EM₁ (AbGroup→Group H)) → A (emloop x i) y) f f + mainpath x i embase = I→A x i + mainpath x i (emloop z j) = SquareP2 x z i j + mainpath x i (emcomp g h j k) = CubeP2 x g h k j i + mainpath x i (emsquash y z p q r s j k' l) = mega i j k' l + where + mega : + PathP (λ i → PathP (λ j → PathP (λ k → + PathP (λ l → A (emloop x i) (emsquash y z p q r s j k l)) + (mainpath x i y) + (mainpath x i z)) + (λ l → mainpath x i (p l)) + λ l → mainpath x i (q l)) + (λ k l → mainpath x i (r k l)) + λ k l → mainpath x i (s k l)) + (λ j mainpath l → f (emsquash y z p q r s j mainpath l)) + λ j mainpath l → f (emsquash y z p q r s j mainpath l) + mega = + toPathP (isOfHLevelPathP' 1 + (isOfHLevelPathP 2 (isOfHLevelPathP 2 (hlev _ _) _ _) _ _) _ _ _ _) + wedgeConFun' G H (suc n) {A = A} hLev f g p north y = f y + wedgeConFun' G H (suc n) {A = A} hLev f g p south y = subst (λ x → A x y) (merid ptEM-raw) (f y) + wedgeConFun' G H (suc n) {A = A} hLev f g p (merid a i) y = mainₗ a y i + module _ where + llem₁ : g south ≡ subst (λ x₁ → A x₁ ptEM-raw) (merid ptEM-raw) (f ptEM-raw) + llem₁ = (λ i → transp (λ j → A (merid ptEM-raw (j ∨ ~ i)) ptEM-raw) (~ i) (g (merid ptEM-raw (~ i)))) + ∙ cong (subst (λ x₁ → A x₁ ptEM-raw) (merid ptEM-raw)) (sym p) + + llem₁' : + Square + (λ i → transp (λ j → A (merid ptEM-raw (i ∨ j)) ptEM-raw) i (g (merid ptEM-raw i))) refl + (cong (subst (λ x → A x ptEM-raw) (merid ptEM-raw)) (sym p)) llem₁ + llem₁' i j = + hcomp (λ k → λ { (i = i0) → transp (λ z → A (merid ptEM-raw (j ∨ z)) ptEM-raw) j + (g (merid ptEM-raw j)) + ; (i = i1) → subst (λ x₁ → A x₁ ptEM-raw) (merid ptEM-raw) (p (~ k)) + ; (j = i0) → (subst (λ x → A x ptEM-raw) (merid ptEM-raw)) (p (~ k ∨ ~ i))}) + (transp (λ k → A (merid ptEM-raw (k ∨ ~ i ∧ j)) ptEM-raw) (~ i ∧ j) (g (merid ptEM-raw (~ i ∧ j)))) + + llem₂ : (λ i₁ → transp (λ j → A (merid ptEM-raw (i₁ ∧ j)) ptEM-raw) (~ i₁) (f ptEM-raw)) + ≡ (λ i₁ → hcomp (λ k → λ { (i₁ = i0) → p (~ k) ; (i₁ = i1) → llem₁ k }) + (g (merid ptEM-raw i₁))) + llem₂ i j = + hcomp (λ k → λ { (i = i0) → transp (λ j₁ → A (merid ptEM-raw (j ∧ j₁)) ptEM-raw) (~ j) (p (~ k)) + ; (j = i0) → p (~ k) + ; (j = i1) → llem₁' k i}) + (transp (λ k → A (merid ptEM-raw ((i ∨ k) ∧ j)) ptEM-raw) (i ∨ ~ j) (g (merid ptEM-raw (i ∧ j)))) + + mainₗ : (a : _) (y : _) + → PathP (λ i → A (merid a i) y) (f y) (subst (λ x → A x y) (merid ptEM-raw) (f y)) + mainₗ = + wedgeConFun' G H n + (λ _ _ → isOfHLevelPathP' (suc (n + 1)) (hLev _ _) _ _) + (λ x i → transp (λ j → A (merid ptEM-raw (i ∧ j)) x) (~ i) (f x)) + (λ x i → hcomp (λ k → λ { (i = i0) → p (~ k) + ; (i = i1) → llem₁ k}) + (g (merid x i))) + llem₂ + + mainP : (y : _) + → mainₗ y ptEM-raw + ≡ λ i → hcomp (λ k → λ { (i = i0) → p (~ k) + ; (i = i1) → llem₁ k}) + (g (merid y i)) + mainP y = + wedgeConFun'ᵣ G H n + (λ _ _ → isOfHLevelPathP' (suc (n + 1)) (hLev _ _) _ _) + (λ x i → transp (λ j → A (merid ptEM-raw (i ∧ j)) x) (~ i) (f x)) + (λ x i → hcomp (λ k → λ { (i = i0) → p (~ k) + ; (i = i1) → llem₁ k}) + (g (merid x i))) + llem₂ y + wedgeConFun'ᵣ G H zero {A = A} hLev f g p = + elimProp _ (λ _ → hLev _ _ _ _) p + wedgeConFun'ᵣ G H (suc n) {A = A} hLev f g p north = p + wedgeConFun'ᵣ G H (suc n) {A = A} hLev f g p south = sym (llem₁ G H n hLev f g p ptEM-raw i0 ptEM-raw) + wedgeConFun'ᵣ G H (suc n) {A = A} hLev f g p (merid a i) k = P k i + where + llem : _ + llem i j = + hcomp (λ k → λ { (i = i1) → g (merid a j) + ; (j = i0) → p (i ∨ ~ k) + ; (j = i1) → llem₁ G H n hLev f g p ptEM-raw i0 ptEM-raw (~ i ∧ k)}) + (g (merid a j)) + + P : PathP (λ k → PathP (λ i → A (merid a i) ptEM-raw) + (p k) (llem₁ G H n hLev f g p ptEM-raw i0 ptEM-raw (~ k))) + (λ i → mainₗ G H n hLev f g p a i ptEM-raw a ptEM-raw i) λ i → g (merid a i) + P = mainP G H n hLev f g p a i0 ptEM-raw a ◁ llem + +-- Here, the actual stuff gets proved. However an additional natural number is stuck into the context +-- to convince the termination checker +private + wedgeConFun : (G : AbGroup ℓ) (H : AbGroup ℓ') + (k n m : ℕ) → (n + m ≡ k) → {A : EM-raw G (suc n) → EM-raw H (suc m) → Type ℓ''} + → ((x : _) (y : _) → isOfHLevel (suc n + suc m) (A x y)) + → (f : (x : _) → A ptEM-raw x) + → (g : (x : _) → A x ptEM-raw) + → f ptEM-raw ≡ g ptEM-raw + → (x : _) (y : _) → A x y + wedgeconLeft : (G : AbGroup ℓ) (H : AbGroup ℓ') (k n m : ℕ) (P : n + m ≡ k) + {A : EM-raw G (suc n) → EM-raw H (suc m) → Type ℓ''} + → (hLev : ((x : _) (y : _) → isOfHLevel (suc n + suc m) (A x y))) + → (f : (x : _) → A ptEM-raw x) + → (g : (x : _) → A x ptEM-raw) + → (p : f ptEM-raw ≡ g ptEM-raw) + → (x : _) → wedgeConFun G H k n m P hLev f g p ptEM-raw x ≡ f x + wedgeconRight : (G : AbGroup ℓ) (H : AbGroup ℓ') + (k n m : ℕ) (P : n + m ≡ k) {A : EM-raw G (suc n) → EM-raw H (suc m) → Type ℓ''} + → (hLev : ((x : _) (y : _) → isOfHLevel (suc n + suc m) (A x y))) + → (f : (x : _) → A ptEM-raw x) + → (g : (x : _) → A x ptEM-raw) + → (p : f ptEM-raw ≡ g ptEM-raw) + → (x : _) → wedgeConFun G H k n m P hLev f g p x ptEM-raw ≡ g x + wedgeConFun G H k n zero P {A = A} hLev f g p = wedgeConFun' G H n hLev f g p + wedgeConFun G H k zero (suc m) P {A = A} hLev f g p x y = + wedgeConFun' H G (suc m) {A = λ x y → A y x} + (λ x y → subst (λ n → isOfHLevel (2 + n) (A y x)) (+-comm 1 m) (hLev y x)) + g f (sym p) y x + wedgeConFun G H l (suc n) (suc m) P {A = A} hlev f g p north y = f y + wedgeConFun G H l (suc n) (suc m) P {A = A} hlev f g p south y = subst (λ x → A x y) (merid ptEM-raw) (f y) + wedgeConFun G H zero (suc n) (suc m) P {A = A} hlev f g p (merid a i) y = ⊥-path i + where + ⊥-path : PathP (λ i → A (merid a i) y) (f y) (subst (λ x → A x y) (merid ptEM-raw) (f y)) + ⊥-path = ⊥-rec (snotz P) + wedgeConFun G H (suc l) (suc n) (suc m) P {A = A} hlev f g p (merid a i) y = mmain a y i + module _ where + llem₃ : g south ≡ (subst (λ x → A x ptEM-raw) (merid ptEM-raw) (f ptEM-raw)) + llem₃ = ((λ i → transp (λ j → A (merid ptEM-raw (~ i ∨ j)) ptEM-raw) (~ i) (g (merid ptEM-raw (~ i))))) + ∙ cong (subst (λ x → A x ptEM-raw) (merid ptEM-raw)) (sym p) + + llem₃' : + Square + (λ i → transp (λ j → A (merid ptEM-raw (~ i ∨ j)) ptEM-raw) (~ i) (g (merid ptEM-raw (~ i)))) + (refl {x = subst (λ x → A x ptEM-raw) (merid ptEM-raw) (f ptEM-raw)}) + llem₃ + ((cong (transport (λ z → A (merid ptEM-raw z) ptEM-raw)) (sym p))) + llem₃' i j = + hcomp (λ k → λ { (i = i0) → transp (λ j₁ → A (merid ptEM-raw (~ j ∨ j₁)) ptEM-raw) (~ j) (g (merid ptEM-raw (~ j))) + ; (i = i1) → subst (λ x → A x ptEM-raw) (merid ptEM-raw) (p (~ k)) + ; (j = i1) → cong (transport (λ z → A (merid ptEM-raw z) ptEM-raw)) (sym p) (i ∧ k)}) + (transp (λ j₁ → A (merid ptEM-raw ((~ j ∧ ~ i) ∨ j₁)) ptEM-raw) (~ j ∧ ~ i) (g (merid ptEM-raw (~ j ∧ ~ i)))) + + + llem₄ : (λ i₁ → transp (λ j → A (merid ptEM-raw (j ∧ i₁)) ptEM-raw) (~ i₁) (f ptEM-raw)) + ≡ (λ i₁ → hcomp (λ k → λ { (i₁ = i0) → p (~ k) ; (i₁ = i1) → llem₃ k }) + (g (merid ptEM-raw i₁))) + llem₄ i j = + hcomp (λ k → λ { (i = i0) → transp (λ z → A (merid ptEM-raw (z ∧ j)) ptEM-raw) (~ j) (p (~ k)) + ; (j = i0) → p (~ k) + ; (j = i1) → llem₃' k (~ i)}) + (transp (λ z → A (merid ptEM-raw ((i ∨ z) ∧ j)) ptEM-raw) (i ∨ ~ j) (g (merid ptEM-raw (i ∧ j)))) + + mmain : (a : _) (y : _) + → PathP (λ i → A (merid a i) y) (f y) + (subst (λ x → A x y) (merid ptEM-raw) (f y)) + mmain = + wedgeConFun G H l n (suc m) (cong predℕ P) + (λ _ _ → isOfHLevelPathP' (suc (n + (suc (suc m)))) (hlev _ _) _ _) + (λ x i → transp (λ j → A (merid ptEM-raw (j ∧ i)) x) (~ i) (f x)) + (λ y i → hcomp (λ k → λ { (i = i0) → p (~ k) + ; (i = i1) → llem₃ k}) + (g (merid y i))) + llem₄ + + mainR : (x : _) → mmain x ptEM-raw + ≡ λ i → hcomp (λ k → λ { (i = i0) → p (~ k) + ; (i = i1) → llem₃ k}) + (g (merid x i)) + mainR x = + wedgeconRight G H l n (suc m) (cong predℕ P) + (λ _ _ → isOfHLevelPathP' (suc (n + (suc (suc m)))) (hlev _ _) _ _) + (λ x i → transp (λ j → A (merid ptEM-raw (j ∧ i)) x) (~ i) (f x)) + (λ y i → hcomp (λ k → λ { (i = i0) → p (~ k) + ; (i = i1) → llem₃ k}) + (g (merid y i))) + llem₄ x + wedgeconLeft G H k zero zero P {A = A} hLev f g p _ = refl + wedgeconLeft G H k (suc n) zero P {A = A} hLev f g p _ = refl + wedgeconLeft G H k zero (suc m) P {A = A} hLev f g p x = + wedgeConFun'ᵣ H G (suc m) + (λ x₁ y → + subst (λ n → (x₂ y₁ : A y x₁) → isOfHLevel (suc n) (x₂ ≡ y₁)) + (+-comm 1 m) (hLev y x₁)) + g f (λ i → p (~ i)) x + wedgeconLeft G H k (suc n) (suc m) P {A = A} hLev f g p _ = refl + wedgeconRight G H k n zero P {A = A} hLev f g p = wedgeConFun'ᵣ G H n hLev f g p + wedgeconRight G H k zero (suc m) P {A = A} hLev f g p _ = refl + wedgeconRight G H zero (suc n) (suc m) P {A = A} hLev f g p x = ⊥-rec (snotz P) + wedgeconRight G H l (suc n) (suc m) P {A = A} hLev f g p north = p + wedgeconRight G H l (suc n) (suc m) P {A = A} hLev f g p south = + sym (llem₃ G H _ n m refl hLev f g p ptEM-raw i0 ptEM-raw) + wedgeconRight G H (suc l) (suc n) (suc m) P {A = A} hLev f g p (merid a i) k = + help k i + where + llem : _ + llem i j = + hcomp (λ k → λ { (i = i1) → g (merid a j) + ; (j = i0) → p (i ∨ ~ k) + ; (j = i1) → llem₃ G H l n m P hLev f g p ptEM-raw i0 ptEM-raw (~ i ∧ k)}) + (g (merid a j)) + + help : PathP (λ k → PathP (λ i → A (merid a i) ptEM-raw) + (p k) (llem₃ G H l n m P hLev f g p ptEM-raw i0 ptEM-raw (~ k))) + (λ i → mmain G H l n m P hLev f g p a i north a north i) (cong g (merid a)) + help = mainR G H l n m P hLev f g p a i0 ptEM-raw a ◁ llem + +module wedgeConEM (G : AbGroup ℓ) (H : AbGroup ℓ') (n m : ℕ) + {A : EM-raw G (suc n) → EM-raw H (suc m) → Type ℓ''} + (hLev : ((x : _) (y : _) → isOfHLevel (suc n + suc m) (A x y))) + (f : (x : _) → A ptEM-raw x) + (g : (x : _) → A x ptEM-raw) + (p : f ptEM-raw ≡ g ptEM-raw) where + fun : (x : EM-raw G (suc n)) (y : EM-raw H (suc m)) → A x y + fun = wedgeConFun G H (n + m) n m refl hLev f g p + + left : (x : EM-raw H (suc m)) → fun ptEM-raw x ≡ f x + left = wedgeconLeft G H (n + m) n m refl hLev f g p + + right : (x : EM-raw G (suc n)) → fun x ptEM-raw ≡ g x + right = wedgeconRight G H (n + m) n m refl hLev f g p diff --git a/Cubical/Algebra/Group/EilenbergMacLane1.agda b/Cubical/Algebra/Group/EilenbergMacLane1.agda deleted file mode 100644 index 93f0566b5..000000000 --- a/Cubical/Algebra/Group/EilenbergMacLane1.agda +++ /dev/null @@ -1,151 +0,0 @@ -{-# OPTIONS --cubical --no-import-sorts --safe --experimental-lossy-unification #-} - -module Cubical.Algebra.Group.EilenbergMacLane1 where - -open import Cubical.Foundations.Prelude -open import Cubical.Foundations.Isomorphism -open import Cubical.Foundations.Equiv -open import Cubical.Foundations.Equiv.HalfAdjoint -open import Cubical.Foundations.GroupoidLaws renaming (assoc to ∙assoc) -open import Cubical.Foundations.Path -open import Cubical.Foundations.HLevels -open import Cubical.Foundations.Univalence -open import Cubical.Data.Unit -open import Cubical.Data.Sigma -open import Cubical.Algebra.Group.Base -open import Cubical.Algebra.Group.Properties -open import Cubical.Homotopy.Connected -open import Cubical.HITs.Truncation as Trunc renaming (rec to trRec; elim to trElim) -open import Cubical.HITs.EilenbergMacLane1 - -private - variable ℓ : Level - -module _ (Ĝ : Group ℓ) where - private - G = fst Ĝ - open GroupStr (snd Ĝ) - - emloop-id : emloop 1g ≡ refl - emloop-id = - emloop 1g ≡⟨ rUnit (emloop 1g) ⟩ - emloop 1g ∙ refl ≡⟨ cong (emloop 1g ∙_) (rCancel (emloop 1g) ⁻¹) ⟩ - emloop 1g ∙ (emloop 1g ∙ (emloop 1g) ⁻¹) ≡⟨ ∙assoc _ _ _ ⟩ - (emloop 1g ∙ emloop 1g) ∙ (emloop 1g) ⁻¹ ≡⟨ cong (_∙ emloop 1g ⁻¹) - ((emloop-comp Ĝ 1g 1g) ⁻¹) ⟩ - emloop (1g · 1g) ∙ (emloop 1g) ⁻¹ ≡⟨ cong (λ g → emloop {Group = Ĝ} g - ∙ (emloop 1g) ⁻¹) - (rid 1g) ⟩ - emloop 1g ∙ (emloop 1g) ⁻¹ ≡⟨ rCancel (emloop 1g) ⟩ - refl ∎ - - emloop-inv : (g : G) → emloop (inv g) ≡ (emloop g) ⁻¹ - emloop-inv g = - emloop (inv g) ≡⟨ rUnit (emloop (inv g)) ⟩ - emloop (inv g) ∙ refl ≡⟨ cong (emloop (inv g) ∙_) - (rCancel (emloop g) ⁻¹) ⟩ - emloop (inv g) ∙ (emloop g ∙ (emloop g) ⁻¹) ≡⟨ ∙assoc _ _ _ ⟩ - (emloop (inv g) ∙ emloop g) ∙ (emloop g) ⁻¹ ≡⟨ cong (_∙ emloop g ⁻¹) - ((emloop-comp Ĝ (inv g) g) ⁻¹) ⟩ - emloop (inv g · g) ∙ (emloop g) ⁻¹ ≡⟨ cong (λ h → emloop {Group = Ĝ} h - ∙ (emloop g) ⁻¹) - (invl g) ⟩ - emloop 1g ∙ (emloop g) ⁻¹ ≡⟨ cong (_∙ (emloop g) ⁻¹) emloop-id ⟩ - refl ∙ (emloop g) ⁻¹ ≡⟨ (lUnit ((emloop g) ⁻¹)) ⁻¹ ⟩ - (emloop g) ⁻¹ ∎ - - isGroupoidEM₁ : isGroupoid (EM₁ Ĝ) - isGroupoidEM₁ = emsquash - - isConnectedEM₁ : isConnected 2 (EM₁ Ĝ) - isConnectedEM₁ = ∣ embase ∣ , h - where - h : (y : hLevelTrunc 2 (EM₁ Ĝ)) → ∣ embase ∣ ≡ y - h = trElim (λ y → isOfHLevelSuc 1 (isOfHLevelTrunc 2 ∣ embase ∣ y)) - (elimProp Ĝ (λ x → isOfHLevelTrunc 2 ∣ embase ∣ ∣ x ∣) refl) - - {- since we write composition in diagrammatic order, - and function composition in the other order, - we need right multiplication here -} - rightEquiv : (g : G) → G ≃ G - rightEquiv g = isoToEquiv isom - where - isom : Iso G G - isom .Iso.fun = _· g - isom .Iso.inv = _· inv g - isom .Iso.rightInv h = - (h · inv g) · g ≡⟨ (assoc h (inv g) g) ⁻¹ ⟩ - h · inv g · g ≡⟨ cong (h ·_) (invl g) ⟩ - h · 1g ≡⟨ rid h ⟩ h ∎ - isom .Iso.leftInv h = - (h · g) · inv g ≡⟨ (assoc h g (inv g)) ⁻¹ ⟩ - h · g · inv g ≡⟨ cong (h ·_) (invr g) ⟩ - h · 1g ≡⟨ rid h ⟩ h ∎ - - compRightEquiv : (g h : G) - → compEquiv (rightEquiv g) (rightEquiv h) ≡ rightEquiv (g · h) - compRightEquiv g h = equivEq (funExt (λ x → (assoc x g h) ⁻¹)) - - CodesSet : EM₁ Ĝ → hSet ℓ - CodesSet = rec Ĝ (isOfHLevelTypeOfHLevel 2) (G , is-set) RE REComp - where - RE : (g : G) → Path (hSet ℓ) (G , is-set) (G , is-set) - RE g = Σ≡Prop (λ X → isPropIsOfHLevel {A = X} 2) (ua (rightEquiv g)) - - lemma₁ : (g h : G) → Square - (ua (rightEquiv g)) (ua (rightEquiv (g · h))) - refl (ua (rightEquiv h)) - lemma₁ g h = invEq - (Square≃doubleComp (ua (rightEquiv g)) (ua (rightEquiv (g · h))) - refl (ua (rightEquiv h))) - (ua (rightEquiv g) ∙ ua (rightEquiv h) - ≡⟨ (uaCompEquiv (rightEquiv g) (rightEquiv h)) ⁻¹ ⟩ - ua (compEquiv (rightEquiv g) (rightEquiv h)) - ≡⟨ cong ua (compRightEquiv g h) ⟩ - ua (rightEquiv (g · h)) ∎) - - lemma₂ : {A₀₀ A₀₁ : hSet ℓ} (p₀₋ : A₀₀ ≡ A₀₁) - {A₁₀ A₁₁ : hSet ℓ} (p₁₋ : A₁₀ ≡ A₁₁) - (p₋₀ : A₀₀ ≡ A₁₀) (p₋₁ : A₀₁ ≡ A₁₁) - (s : Square (cong fst p₀₋) (cong fst p₁₋) (cong fst p₋₀) (cong fst p₋₁)) - → Square p₀₋ p₁₋ p₋₀ p₋₁ - fst (lemma₂ p₀₋ p₁₋ p₋₀ p₋₁ s i j) = s i j - snd (lemma₂ p₀₋ p₁₋ p₋₀ p₋₁ s i j) = - isSet→SquareP {A = (λ i j → isSet (s i j))} - (λ i j → isProp→isSet (isPropIsOfHLevel 2)) - (cong snd p₀₋) (cong snd p₁₋) (cong snd p₋₀) (cong snd p₋₁) i j - - REComp : (g h : G) → Square (RE g) (RE (g · h)) refl (RE h) - REComp g h = lemma₂ (RE g) (RE (g · h)) refl (RE h) (lemma₁ g h) - Codes : EM₁ Ĝ → Type ℓ - Codes x = CodesSet x .fst - - encode : (x : EM₁ Ĝ) → embase ≡ x → Codes x - encode x p = subst Codes p 1g - - decode : (x : EM₁ Ĝ) → Codes x → embase ≡ x - decode = elimSet Ĝ (λ x → isOfHLevelΠ 2 (λ c → isGroupoidEM₁ (embase) x)) - emloop λ g → ua→ λ h → emcomp h g - - - decode-encode : (x : EM₁ Ĝ) (p : embase ≡ x) → decode x (encode x p) ≡ p - decode-encode x p = J (λ y q → decode y (encode y q) ≡ q) - (emloop (transport refl 1g) ≡⟨ cong emloop (transportRefl 1g) ⟩ - emloop 1g ≡⟨ emloop-id ⟩ refl ∎) p - - encode-decode : (x : EM₁ Ĝ) (c : Codes x) → encode x (decode x c) ≡ c - encode-decode = elimProp Ĝ (λ x → isOfHLevelΠ 1 (λ c → CodesSet x .snd _ _)) - λ g → encode embase (decode embase g) ≡⟨ refl ⟩ - encode embase (emloop g) ≡⟨ refl ⟩ - transport (ua (rightEquiv g)) 1g ≡⟨ uaβ (rightEquiv g) 1g ⟩ - 1g · g ≡⟨ lid g ⟩ - g ∎ - - ΩEM₁Iso : Iso (Path (EM₁ Ĝ) embase embase) G - Iso.fun ΩEM₁Iso = encode embase - Iso.inv ΩEM₁Iso = emloop - Iso.rightInv ΩEM₁Iso = encode-decode embase - Iso.leftInv ΩEM₁Iso = decode-encode embase - - ΩEM₁≡ : (Path (EM₁ Ĝ) embase embase) ≡ G - ΩEM₁≡ = isoToPath ΩEM₁Iso diff --git a/Cubical/Algebra/Group/MorphismProperties.agda b/Cubical/Algebra/Group/MorphismProperties.agda index 89e1e5a3b..c3897279a 100644 --- a/Cubical/Algebra/Group/MorphismProperties.agda +++ b/Cubical/Algebra/Group/MorphismProperties.agda @@ -77,6 +77,21 @@ module _ {A : Type ℓ} {B : Type ℓ'} {G : GroupStr A} {f : A → B} {H : Grou makeIsGroupHom .pres1 = hom1g G f H pres makeIsGroupHom .presinv = homInv G f H pres +isGroupHomInv : (f : GroupEquiv G H) → IsGroupHom (H .snd) (invEq (fst f)) (G .snd) +isGroupHomInv {G = G} {H = H} f = makeIsGroupHom λ h h' → + isInj-f _ _ + (f' (g (h ⋆² h')) ≡⟨ secEq (fst f) _ ⟩ + (h ⋆² h') ≡⟨ sym (cong₂ _⋆²_ (secEq (fst f) h) (secEq (fst f) h')) ⟩ + (f' (g h) ⋆² f' (g h')) ≡⟨ sym (pres· (snd f) _ _) ⟩ + f' (g h ⋆¹ g h') ∎) + where + f' = fst (fst f) + _⋆¹_ = _·_ (snd G) + _⋆²_ = _·_ (snd H) + g = invEq (fst f) + + isInj-f : (x y : ⟨ G ⟩) → f' x ≡ f' y → x ≡ y + isInj-f x y = invEq (_ , isEquiv→isEmbedding (snd (fst f)) x y) -- H-level results isPropIsGroupHom : (G : Group ℓ) (H : Group ℓ') {f : ⟨ G ⟩ → ⟨ H ⟩} @@ -195,22 +210,6 @@ compGroupEquiv : GroupEquiv F G → GroupEquiv G H → GroupEquiv F H fst (compGroupEquiv f g) = compEquiv (fst f) (fst g) snd (compGroupEquiv f g) = isGroupHomComp (_ , f .snd) (_ , g .snd) -isGroupHomInv : (f : GroupEquiv G H) → IsGroupHom (H .snd) (invEq (fst f)) (G .snd) -isGroupHomInv {G = G} {H = H} f = makeIsGroupHom λ h h' → - isInj-f _ _ - (f' (g (h ⋆² h')) ≡⟨ secEq (fst f) _ ⟩ - (h ⋆² h') ≡⟨ sym (cong₂ _⋆²_ (secEq (fst f) h) (secEq (fst f) h')) ⟩ - (f' (g h) ⋆² f' (g h')) ≡⟨ sym (pres· (snd f) _ _) ⟩ - f' (g h ⋆¹ g h') ∎) - where - f' = fst (fst f) - _⋆¹_ = _·_ (snd G) - _⋆²_ = _·_ (snd H) - g = invEq (fst f) - - isInj-f : (x y : ⟨ G ⟩) → f' x ≡ f' y → x ≡ y - isInj-f x y = invEq (_ , isEquiv→isEmbedding (snd (fst f)) x y) - invGroupEquiv : GroupEquiv G H → GroupEquiv H G fst (invGroupEquiv f) = invEquiv (fst f) snd (invGroupEquiv f) = isGroupHomInv f diff --git a/Cubical/Data/Nat/Base.agda b/Cubical/Data/Nat/Base.agda index 427cdb8a2..87ba8e68a 100644 --- a/Cubical/Data/Nat/Base.agda +++ b/Cubical/Data/Nat/Base.agda @@ -42,6 +42,14 @@ elim : ∀ {ℓ} {A : ℕ → Type ℓ} elim a₀ _ zero = a₀ elim a₀ f (suc n) = f n (elim a₀ f n) +elim+2 : ∀ {ℓ} {A : ℕ → Type ℓ} → A 0 → A 1 + → ((n : ℕ) → (A (suc n) → A (suc (suc n)))) + → (n : ℕ) → A n +elim+2 a0 a1 ind zero = a0 +elim+2 a0 a1 ind (suc zero) = a1 +elim+2 {A = A} a0 a1 ind (suc (suc n)) = + ind n (elim+2 {A = A} a0 a1 ind (suc n)) + isEven isOdd : ℕ → Bool isEven zero = true isEven (suc n) = isOdd n diff --git a/Cubical/Foundations/HLevels.agda b/Cubical/Foundations/HLevels.agda index 3b218317f..ab292e257 100644 --- a/Cubical/Foundations/HLevels.agda +++ b/Cubical/Foundations/HLevels.agda @@ -763,4 +763,3 @@ isSet→Iso-Iso-≡ isSet-A isSet-A′ = ww hSet-Iso-Iso-≡ : (A : hSet ℓ) → (A' : hSet ℓ) → Iso (Iso (fst A) (fst A')) (A ≡ A') hSet-Iso-Iso-≡ A A' = compIso (isSet→Iso-Iso-≡ (snd A) (snd A')) (equivToIso (_ , isEquiv-Σ≡Prop λ _ → isPropIsSet)) - diff --git a/Cubical/Foundations/Path.agda b/Cubical/Foundations/Path.agda index 0d879ef9f..f20fc3d58 100644 --- a/Cubical/Foundations/Path.agda +++ b/Cubical/Foundations/Path.agda @@ -367,3 +367,16 @@ compPathR→PathP∙∙ {p = p} {q = q} {r = r} {s = s} P j i = ; (j = i0) → r i ; (j = i1) → doubleCompPath-filler p s (sym q) (~ k) i}) (P j i) + +comm→PathP : {a b c d : A} {p : a ≡ c} {q : b ≡ d} {r : a ≡ b} {s : c ≡ d} + → p ∙ s ≡ r ∙ q + → PathP (λ i → p i ≡ q i) r s +comm→PathP {p = p} {q = q} {r = r} {s = s} P i j = + hcomp + (λ k → λ + { (i = i0) → r (j ∧ k) + ; (i = i1) → s (j ∨ ~ k) + ; (j = i0) → compPath-filler p s (~ k) i + ; (j = i1) → compPath-filler' r q (~ k) i + }) + (P j i) diff --git a/Cubical/Foundations/Pointed/Homogeneous.agda b/Cubical/Foundations/Pointed/Homogeneous.agda index 4c00385ca..c2661ad44 100644 --- a/Cubical/Foundations/Pointed/Homogeneous.agda +++ b/Cubical/Foundations/Pointed/Homogeneous.agda @@ -46,6 +46,49 @@ isHomogeneous {ℓ} (A , x) = ∀ y → Path (Pointed ℓ) (A , x) (A , y) }) (sym (h (pt B∙)) ∙ h ((sym f₀ ∙∙ funExt⁻ p a₀ ∙∙ g₀) i)) +→∙Homogeneous≡Path : ∀ {ℓ ℓ'} {A∙ : Pointed ℓ} {B∙ : Pointed ℓ'} {f∙ g∙ : A∙ →∙ B∙} + (h : isHomogeneous B∙) → (p q : f∙ ≡ g∙) → cong fst p ≡ cong fst q → p ≡ q +→∙Homogeneous≡Path {A∙ = A∙@(A , a₀)} {B∙@(B , b)} {f∙@(f , f₀)} {g∙@(g , g₀)} h p q r = + transport (λ k + → PathP (λ i + → PathP (λ j → (A , a₀) →∙ newPath-refl p q r i j (~ k)) + (f , f₀) (g , g₀)) p q) + (badPath p q r) + where + newPath : (p q : f∙ ≡ g∙) (r : cong fst p ≡ cong fst q) + → Square (refl {x = b}) refl refl refl + newPath p q r i j = + hcomp (λ k → λ {(i = i0) → cong snd p j k + ; (i = i1) → cong snd q j k + ; (j = i0) → f₀ k + ; (j = i1) → g₀ k}) + (r i j a₀) + + newPath-refl : (p q : f∙ ≡ g∙) (r : cong fst p ≡ cong fst q) + → PathP (λ i → (PathP (λ j → B∙ ≡ (B , newPath p q r i j))) refl refl) refl refl + newPath-refl p q r i j k = + hcomp (λ w → λ { (i = i0) → lCancel (h b) w k + ; (i = i1) → lCancel (h b) w k + ; (j = i0) → lCancel (h b) w k + ; (j = i1) → lCancel (h b) w k + ; (k = i0) → lCancel (h b) w k + ; (k = i1) → B , newPath p q r i j}) + ((sym (h b) ∙ h (newPath p q r i j)) k) + + badPath : (p q : f∙ ≡ g∙) (r : cong fst p ≡ cong fst q) + → PathP (λ i → + PathP (λ j → A∙ →∙ (B , newPath p q r i j)) + (f , f₀) (g , g₀)) + p q + fst (badPath p q r i j) = r i j + snd (badPath p q s i j) k = + hcomp (λ r → λ { (i = i0) → snd (p j) (r ∧ k) + ; (i = i1) → snd (q j) (r ∧ k) + ; (j = i0) → f₀ (k ∧ r) + ; (j = i1) → g₀ (k ∧ r) + ; (k = i0) → s i j a₀}) + (s i j a₀) + isHomogeneousPi : ∀ {ℓ ℓ'} {A : Type ℓ} {B∙ : A → Pointed ℓ'} → (∀ a → isHomogeneous (B∙ a)) → isHomogeneous (Πᵘ∙ A B∙) isHomogeneousPi h f i .fst = ∀ a → typ (h a (f a) i) diff --git a/Cubical/HITs/EilenbergMacLane1/Base.agda b/Cubical/HITs/EilenbergMacLane1/Base.agda index b28a48d27..c9c76557a 100644 --- a/Cubical/HITs/EilenbergMacLane1/Base.agda +++ b/Cubical/HITs/EilenbergMacLane1/Base.agda @@ -9,6 +9,8 @@ This file contains: module Cubical.HITs.EilenbergMacLane1.Base where open import Cubical.Foundations.Prelude +open import Cubical.Foundations.GroupoidLaws + renaming (assoc to assoc∙) open import Cubical.Algebra.Group.Base private @@ -41,3 +43,19 @@ module _ (Group@(G , str) : Group ℓ) where emloop-comp g h i = compPath-unique refl (emloop g) (emloop h) (emloop (g · h) , emcomp g h) (emloop g ∙ emloop h , compPath-filler (emloop g) (emloop h)) i .fst + + emloop-1g : emloop 1g ≡ refl + emloop-1g = + lUnit (emloop 1g) + ∙∙ cong (_∙ emloop 1g) (sym (lCancel (emloop 1g)) ) + ∙∙ sym (assoc∙ _ _ _) + ∙∙ cong (sym (emloop 1g) ∙_) (sym (emloop-comp 1g 1g) ∙ cong emloop (lid 1g)) + ∙∙ rCancel _ + + emloop-sym : (g : G) → emloop (inv g) ≡ sym (emloop g) + emloop-sym g = + rUnit _ + ∙∙ cong (emloop (inv g) ∙_) (sym (rCancel (emloop g))) + ∙∙ assoc∙ _ _ _ + ∙∙ cong (_∙ sym (emloop g)) (sym (emloop-comp (inv g) g) ∙∙ cong emloop (invl g) ∙∙ emloop-1g) + ∙∙ sym (lUnit _) diff --git a/Cubical/HITs/EilenbergMacLane1/Properties.agda b/Cubical/HITs/EilenbergMacLane1/Properties.agda index 7af601e5d..de5d1f51b 100644 --- a/Cubical/HITs/EilenbergMacLane1/Properties.agda +++ b/Cubical/HITs/EilenbergMacLane1/Properties.agda @@ -4,7 +4,7 @@ Eilenberg–Mac Lane type K(G, 1) -} -{-# OPTIONS --cubical --no-import-sorts --safe #-} +{-# OPTIONS --cubical --no-import-sorts --safe --experimental-lossy-unification #-} module Cubical.HITs.EilenbergMacLane1.Properties where open import Cubical.HITs.EilenbergMacLane1.Base @@ -15,10 +15,19 @@ open import Cubical.Foundations.Prelude open import Cubical.Foundations.Isomorphism open import Cubical.Foundations.Equiv open import Cubical.Foundations.HLevels +open import Cubical.Foundations.GroupoidLaws +open import Cubical.Foundations.Univalence open import Cubical.Data.Sigma +open import Cubical.Data.Empty renaming (rec to ⊥-rec) hiding (elim) + open import Cubical.Algebra.Group.Base +open import Cubical.Algebra.Group.Properties + +open import Cubical.Algebra.AbGroup.Base + +open import Cubical.Functions.Morphism open import Cubical.HITs.PropositionalTruncation as PropTrunc using (∥_∥; ∣_∣; squash) open import Cubical.HITs.SetTruncation as SetTrunc using (∥_∥₂; ∣_∣₂; squash₂) @@ -31,6 +40,29 @@ module _ ((G , str) : Group ℓG) where open GroupStr str + elimGroupoid : + {B : EM₁ (G , str) → Type ℓ} + → ((x : EM₁ (G , str)) → isGroupoid (B x)) + → (b : B embase) + → (bloop : ((g : G) → PathP (λ i → B (emloop g i)) b b)) + → ((g h : G) → PathP (λ i → PathP (λ j → B (emcomp g h j i)) + (bloop g i) (bloop (g · h) i)) (λ _ → b) (bloop h)) + → (x : EM₁ (G , str)) + → B x + elimGroupoid Bgroup b bloop bcomp embase = b + elimGroupoid Bgroup b bloop bcomp (emloop x i) = bloop x i + elimGroupoid Bgroup b bloop bcomp (emcomp g h j i) = bcomp g h i j + elimGroupoid {B = B} Bgroup b bloop bcomp (emsquash g h p q r s i j k) = help i j k + where + help : PathP (λ i → PathP (λ j → PathP (λ k → B (emsquash g h p q r s i j k)) + (elimGroupoid Bgroup b bloop bcomp g) + (elimGroupoid Bgroup b bloop bcomp h)) + (λ k → elimGroupoid Bgroup b bloop bcomp (p k)) + λ k → elimGroupoid Bgroup b bloop bcomp (q k)) + (λ j k → elimGroupoid Bgroup b bloop bcomp (r j k)) + λ j k → elimGroupoid Bgroup b bloop bcomp (s j k) + help = toPathP (isOfHLevelPathP' 1 (isOfHLevelPathP' 2 (Bgroup _) _ _) _ _ _ _) + elimSet : {B : EM₁ (G , str) → Type ℓ} → ((x : EM₁ (G , str)) → isSet (B x)) → (b : B embase) diff --git a/Cubical/ZCohomology/RingStructure/CupProduct.agda b/Cubical/ZCohomology/RingStructure/CupProduct.agda index dd9da8180..b2a0f2697 100644 --- a/Cubical/ZCohomology/RingStructure/CupProduct.agda +++ b/Cubical/ZCohomology/RingStructure/CupProduct.agda @@ -31,6 +31,9 @@ suc a +' suc b = 2 + (a + b) +'≡+ (suc n) zero = cong suc (sym (+-comm n zero)) +'≡+ (suc n) (suc m) = cong suc (sym (+-suc n m)) ++'-comm : (n m : ℕ) → n +' m ≡ m +' n ++'-comm n m = +'≡+ n m ∙∙ +-comm n m ∙∙ sym (+'≡+ m n) + -- Cup product with one integer (K₀) argument _·₀_ : {n : ℕ} (m : ℤ) → coHomK n → coHomK n _·₀_ {n = n} (pos zero) x = 0ₖ _ diff --git a/Cubical/ZCohomology/RingStructure/GradedCommutativity.agda b/Cubical/ZCohomology/RingStructure/GradedCommutativity.agda index 68ea383b7..1257f8cf0 100644 --- a/Cubical/ZCohomology/RingStructure/GradedCommutativity.agda +++ b/Cubical/ZCohomology/RingStructure/GradedCommutativity.agda @@ -45,17 +45,13 @@ natTranspLem : ∀ {ℓ} {A B : ℕ → Type ℓ} {n m : ℕ} (a : A n) → f m (subst A p a) ≡ subst B p (f n a) natTranspLem {A = A} {B = B} a f p = sym (substCommSlice A B f p a) -+'-comm : (n m : ℕ) → n +' m ≡ m +' n -+'-comm n m = +'≡+ n m ∙∙ +-comm n m ∙∙ sym (+'≡+ m n) +transp0₁ : (n : ℕ) → subst coHomK (+'-comm 1 (suc n)) (0ₖ _) ≡ 0ₖ _ +transp0₁ zero = refl +transp0₁ (suc n) = refl -private - transp0₁ : (n : ℕ) → subst coHomK (+'-comm 1 (suc n)) (0ₖ _) ≡ 0ₖ _ - transp0₁ zero = refl - transp0₁ (suc n) = refl - - transp0₂ : (n m : ℕ) → subst coHomK (+'-comm (suc (suc n)) (suc m)) (0ₖ _) ≡ 0ₖ _ - transp0₂ n zero = refl - transp0₂ n (suc m) = refl +transp0₂ : (n m : ℕ) → subst coHomK (+'-comm (suc (suc n)) (suc m)) (0ₖ _) ≡ 0ₖ _ +transp0₂ n zero = refl +transp0₂ n (suc m) = refl -- Recurring expressions private diff --git a/Cubical/ZCohomology/RingStructure/RingLaws.agda b/Cubical/ZCohomology/RingStructure/RingLaws.agda index 701b805d0..8b30e16b4 100644 --- a/Cubical/ZCohomology/RingStructure/RingLaws.agda +++ b/Cubical/ZCohomology/RingStructure/RingLaws.agda @@ -102,12 +102,14 @@ private snd (⌣ₖ-distrFun2 n m x y) = cong₂ _+ₖ_ (0ₖ-⌣ₖ m n x) (0ₖ-⌣ₖ m n y) ∙ rUnitₖ _ _ - leftDistr-⌣ₖ· : (n m : ℕ) (x y : coHomK (suc n)) → ⌣ₖ-distrFun (suc n) (suc m) x y ≡ ⌣ₖ-distrFun2 (suc n) (suc m) x y + leftDistr-⌣ₖ· : (n m : ℕ) (x y : coHomK (suc n)) + → ⌣ₖ-distrFun (suc n) (suc m) x y ≡ ⌣ₖ-distrFun2 (suc n) (suc m) x y leftDistr-⌣ₖ· n m = elim2 (λ _ _ → isOfHLevelSuc (2 + n) (hLevHelp n m _ _)) main where - hLevHelp : (n m : ℕ) (x y : _) → isOfHLevel (2 + n) ( ⌣ₖ-distrFun (suc n) (suc m) x y ≡ ⌣ₖ-distrFun2 (suc n) (suc m) x y) + hLevHelp : (n m : ℕ) (x y : _) + → isOfHLevel (2 + n) ( ⌣ₖ-distrFun (suc n) (suc m) x y ≡ ⌣ₖ-distrFun2 (suc n) (suc m) x y) hLevHelp n m x y = (subst (isOfHLevel (3 + n)) (λ i → (coHomK-ptd (suc m) →∙ coHomK-ptd (suc (suc (+-comm n m i))))) @@ -230,7 +232,8 @@ private snd (⌣ₖ-distrFun2-r n m x y) = cong₂ _+ₖ_ (⌣ₖ-0ₖ n m x) (⌣ₖ-0ₖ n m y) ∙ rUnitₖ _ _ - rightDistr-⌣ₖ· : (n m : ℕ) (x y : coHomK (suc n)) → ⌣ₖ-distrFun-r (suc n) (suc m) x y ≡ ⌣ₖ-distrFun2-r (suc n) (suc m) x y + rightDistr-⌣ₖ· : (n m : ℕ) (x y : coHomK (suc n)) + → ⌣ₖ-distrFun-r (suc n) (suc m) x y ≡ ⌣ₖ-distrFun2-r (suc n) (suc m) x y rightDistr-⌣ₖ· n m = elim2 (λ _ _ → isOfHLevelPath (3 + n) (isOfHLevel↑∙ (suc n) m) _ _) main