From 210881667d7f04ead89cf23fe69fe9e5827beecd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Na=C3=AFm=20Favier?= Date: Tue, 27 Aug 2024 13:12:37 +0200 Subject: [PATCH] =?UTF-8?q?chore:=20only=20lift=20=E2=84=A4=20and=20?= =?UTF-8?q?=E2=84=A4/n=20as=20needed?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Having ℤ unlifted means that we can use the category reasoning combinators to prove identities of the integers without having to sprinkle lifts and lowers everywhere. --- src/Algebra/Group/Cat/Base.lagda.md | 31 ++++++++++ src/Algebra/Group/Instances/Cyclic.lagda.md | 60 +++++++++---------- src/Algebra/Group/Instances/Dihedral.lagda.md | 2 +- src/Algebra/Group/Instances/Integers.lagda.md | 58 +++++++++--------- src/Data/Int/DivMod.lagda.md | 8 +-- src/Homotopy/Space/Circle.lagda.md | 6 +- 6 files changed, 99 insertions(+), 66 deletions(-) diff --git a/src/Algebra/Group/Cat/Base.lagda.md b/src/Algebra/Group/Cat/Base.lagda.md index a71952259..2943014ab 100644 --- a/src/Algebra/Group/Cat/Base.lagda.md +++ b/src/Algebra/Group/Cat/Base.lagda.md @@ -1,7 +1,10 @@ + ## The underlying set The category of groups admits a `faithful`{.Agda ident=is-faithful} diff --git a/src/Algebra/Group/Instances/Cyclic.lagda.md b/src/Algebra/Group/Instances/Cyclic.lagda.md index 455649920..e45f16113 100644 --- a/src/Algebra/Group/Instances/Cyclic.lagda.md +++ b/src/Algebra/Group/Instances/Cyclic.lagda.md @@ -19,7 +19,6 @@ open import Data.Nat open represents-subgroup open normal-subgroup open is-group-hom -open Lift ``` --> @@ -29,7 +28,7 @@ module Algebra.Group.Instances.Cyclic where @@ -75,20 +74,20 @@ $n$ when $n \geq 1$, and is the infinite cyclic group when $n = 0$. ```agda infix 30 _·ℤ -_·ℤ : ∀ (n : Nat) {ℓ} → normal-subgroup (ℤ {ℓ}) λ (lift i) → el (n ∣ℤ i) (∣ℤ-is-prop n i) +_·ℤ : ∀ (n : Nat) → normal-subgroup ℤ λ i → el (n ∣ℤ i) (∣ℤ-is-prop n i) (n ·ℤ) .has-rep .has-unit = ∣ℤ-zero (n ·ℤ) .has-rep .has-⋆ = ∣ℤ-+ (n ·ℤ) .has-rep .has-inv = ∣ℤ-negℤ -(n ·ℤ) {ℓ} .has-conjugate {lift x} {lift y} = subst (n ∣ℤ_) x≡y+x-y +(n ·ℤ) .has-conjugate {x} {y} = subst (n ∣ℤ_) x≡y+x-y where x≡y+x-y : x ≡ y +ℤ (x -ℤ y) x≡y+x-y = - x ≡⟨ ap lower (ℤ.insertl {h = lift {ℓ = ℓ} y} (ℤ.inverser {x = lift y})) ⟩ + x ≡⟨ ℤ.insertl {h = y} (ℤ.inverser {x = y}) ⟩ y +ℤ (negℤ y +ℤ x) ≡⟨ ap (y +ℤ_) (+ℤ-commutative (negℤ y) x) ⟩ y +ℤ (x -ℤ y) ∎ infix 25 ℤ/_ -ℤ/_ : Nat → ∀ {ℓ} → Group ℓ +ℤ/_ : Nat → Group lzero ℤ/ n = ℤ /ᴳ n ·ℤ ``` @@ -96,11 +95,11 @@ $\ZZ/n\ZZ$ is an [[abelian group]], since the commutativity of addition descends to the quotient. ```agda -ℤ/n-commutative : ∀ n {ℓ} → is-commutative-group {ℓ} (ℤ/ n) -ℤ/n-commutative n = elim! λ x y → ap (inc ⊙ lift) (+ℤ-commutative x y) +ℤ/n-commutative : ∀ n → is-commutative-group (ℤ/ n) +ℤ/n-commutative n = elim! λ x y → ap inc (+ℤ-commutative x y) infix 25 ℤ-ab/_ -ℤ-ab/_ : Nat → ∀ {ℓ} → Abelian-group ℓ +ℤ-ab/_ : Nat → Abelian-group lzero ℤ-ab/_ n = from-commutative-group (ℤ/ n) (ℤ/n-commutative n) ``` @@ -109,24 +108,23 @@ by $1$. ```agda - ℤ/n-cyclic : is-cyclic ℤ/n + ℤ/n-cyclic : is-cyclic (ℤ/ n) ℤ/n-cyclic = inc (1 , gen) where - gen : ℤ/n is-generated-by 1 + gen : ℤ/ n is-generated-by 1 gen = elim! λ x → inc (x , Integers.induction Int-integers - {P = λ x → inc (lift x) ≡ pow ℤ/n 1 x} + {P = λ x → inc x ≡ pow (ℤ/ n) 1 x} refl (λ x → - inc (lift x) ≡ pow ℤ/n 1 x ≃⟨ _ , equiv→cancellable (⋆-equivr 1) ⟩ - inc (lift x) ⋆ 1 ≡ pow ℤ/n 1 x ⋆ 1 ≃⟨ ∙-pre-equiv (sym (ap (inc ⊙ lift) (+ℤ-oner x))) ⟩ - inc (lift (sucℤ x)) ≡ pow ℤ/n 1 x ⋆ 1 ≃⟨ ∙-post-equiv (sym (pow-sucr ℤ/n 1 x)) ⟩ - inc (lift (sucℤ x)) ≡ pow ℤ/n 1 (sucℤ x) ≃∎) + inc x ≡ pow (ℤ/ n) 1 x ≃⟨ _ , equiv→cancellable (⋆-equivr 1) ⟩ + inc x ⋆ 1 ≡ pow (ℤ/ n) 1 x ⋆ 1 ≃⟨ ∙-pre-equiv (sym (ap inc (+ℤ-oner x))) ⟩ + inc (sucℤ x) ≡ pow (ℤ/ n) 1 x ⋆ 1 ≃⟨ ∙-post-equiv (sym (pow-sucr (ℤ/ n) 1 x)) ⟩ + inc (sucℤ x) ≡ pow (ℤ/ n) 1 (sucℤ x) ≃∎) x) ``` @@ -148,8 +146,8 @@ module _ (wraps : x^ pos n ≡ unit) where - ℤ/-out : Groups.Hom (ℤ/ n) G - ℤ/-out .hom = Coeq-rec (apply x^-) λ (lift a , lift b , n∣a-b) → zero-diff $ + ℤ/-out : Groups.Hom (LiftGroup ℓ (ℤ/ n)) G + ℤ/-out .hom (lift i) = Coeq-rec (apply x^- ⊙ lift) (λ (a , b , n∣a-b) → zero-diff $ let k , k*n≡a-b = ∣ℤ→fibre n∣a-b in x^ a — x^ b ≡˘⟨ pres-diff (x^- .preserves) {lift a} {lift b} ⟩ x^ (a -ℤ b) ≡˘⟨ ap x^_ k*n≡a-b ⟩ @@ -157,7 +155,8 @@ module _ x^ (pos n *ℤ k) ≡⟨ pow-* G x (pos n) k ⟩ pow G ⌜ x^ pos n ⌝ k ≡⟨ ap! wraps ⟩ pow G unit k ≡⟨ pow-unit G k ⟩ - unit ∎ + unit ∎) + i ℤ/-out .preserves .pres-⋆ = elim! λ x y → x^- .preserves .pres-⋆ (lift x) (lift y) ``` @@ -165,14 +164,14 @@ module _ We can check that $\ZZ/0\ZZ \is \ZZ$: ```agda -ℤ-ab/0≡ℤ-ab : ∀ {ℓ} → ℤ-ab/ 0 ≡ ℤ-ab {ℓ} +ℤ-ab/0≡ℤ-ab : ℤ-ab/ 0 ≡ ℤ-ab ℤ-ab/0≡ℤ-ab = ∫-Path (total-hom - (Coeq-rec (λ z → z) (λ (_ , _ , p) → ℤ.zero-diff (ap lift p))) + (Coeq-rec (λ z → z) (λ (_ , _ , p) → ℤ.zero-diff p)) (record { pres-⋆ = elim! λ _ _ → refl })) (is-iso→is-equiv (iso inc (λ _ → refl) (elim! λ _ → refl))) -ℤ/0≡ℤ : ∀ {ℓ} → ℤ/ 0 ≡ ℤ {ℓ} +ℤ/0≡ℤ : ℤ/ 0 ≡ ℤ ℤ/0≡ℤ = Grp→Ab→Grp (ℤ/ 0) (ℤ/n-commutative 0) ∙ ap Abelian→Group ℤ-ab/0≡ℤ-ab ``` @@ -182,16 +181,16 @@ $x : \ZZ$ to the representative of its congruence class modulo $n$, $x \% n$. ```agda -ℤ/n≃ℕ @@ -29,26 +28,24 @@ private module ℤ = Integers Int-integers # The group of integers {defines="integer-group group-of-integers"} -The fundamental example of an [[abelian group]] is the group of [[**integers**]], $\ZZ$, under -addition. A type-theoretic interjection is necessary: the integers live -on the zeroth universe, so to have an $\ell$-sized group of integers, we -must lift it. +The fundamental example of an [[abelian group]] is the group of +[[**integers**]], $\ZZ$, under addition. ```agda -ℤ-ab : ∀ {ℓ} → Abelian-group ℓ +ℤ-ab : Abelian-group lzero ℤ-ab = to-ab mk-ℤ where open make-abelian-group - mk-ℤ : make-abelian-group (Lift _ Int) + mk-ℤ : make-abelian-group Int mk-ℤ .ab-is-set = hlevel 2 - mk-ℤ .mul (lift x) (lift y) = lift (x +ℤ y) - mk-ℤ .inv (lift x) = lift (negℤ x) + mk-ℤ .mul x y = x +ℤ y + mk-ℤ .inv x = negℤ x mk-ℤ .1g = 0 - mk-ℤ .idl (lift x) = ap lift (+ℤ-zerol x) - mk-ℤ .assoc (lift x) (lift y) (lift z) = ap lift (+ℤ-assoc x y z) - mk-ℤ .invl (lift x) = ap lift (+ℤ-invl x) - mk-ℤ .comm (lift x) (lift y) = ap lift (+ℤ-commutative x y) + mk-ℤ .idl x = +ℤ-zerol x + mk-ℤ .assoc x y z = +ℤ-assoc x y z + mk-ℤ .invl x = +ℤ-invl x + mk-ℤ .comm x y = +ℤ-commutative x y -ℤ : ∀ {ℓ} → Group ℓ +ℤ : Group lzero ℤ = Abelian→Group ℤ-ab ``` @@ -85,8 +82,14 @@ module _ {ℓ} (G : Group ℓ) where pow (a +ℤ b) ⋆ x ≡ pow a ⋆ pow (sucℤ b) ≃⟨ ∙-pre-equiv (pow-sucr (a +ℤ b)) ⟩ pow (sucℤ (a +ℤ b)) ≡ pow a ⋆ pow (sucℤ b) ≃⟨ ∙-pre-equiv (ap pow (+ℤ-sucr a b)) ⟩ pow (a +ℤ sucℤ b) ≡ pow a ⋆ pow (sucℤ b) ≃∎ +``` - pow-hom : Groups.Hom ℤ G +A type-theoretic interjection is necessary: the integers live on the +zeroth universe, so to have an $\ell$-sized group of integers, we +must lift it. + +```agda + pow-hom : Groups.Hom (LiftGroup ℓ ℤ) G pow-hom .hom (lift i) = pow i pow-hom .preserves .pres-⋆ (lift a) (lift b) = pow-+ a b ``` @@ -94,7 +97,7 @@ module _ {ℓ} (G : Group ℓ) where This is the unique group homomorphism $\ZZ \to G$ that sends $1$ to $x$. ```agda - pow-unique : (g : Groups.Hom ℤ G) → g # 1 ≡ x → g ≡ pow-hom + pow-unique : (g : Groups.Hom (LiftGroup ℓ ℤ) G) → g # 1 ≡ x → g ≡ pow-hom pow-unique g g1≡x = ext $ ℤ.map-out-unique (λ i → g # lift i) (pres-id (g .preserves)) λ y → @@ -158,7 +161,7 @@ one generator. ```agda ℤ-free : Free-object Grp↪Sets (el! ⊤) -ℤ-free .Free-object.free = ℤ +ℤ-free .Free-object.free = LiftGroup lzero ℤ ℤ-free .Free-object.unit _ = 1 ℤ-free .Free-object.fold {G} x = pow-hom G (x _) ℤ-free .Free-object.commute {G} {x} = ext λ _ → pow-1 G (x _) @@ -173,12 +176,12 @@ notation. In fact, we can show that $n \cdot x$ coincides with the multiplication $n \times x$ in the group of integers itself. ```agda -pow-ℤ : ∀ {ℓ} a b → Lift.lower (pow (ℤ {ℓ}) (lift a) b) ≡ a *ℤ b -pow-ℤ {ℓ} a = ℤ.induction (sym (*ℤ-zeror a)) λ b → - lower (pow ℤ (lift a) b) ≡ a *ℤ b ≃⟨ ap (_+ℤ a) , equiv→cancellable (equiv≃ Lift-≃ Lift-≃ .fst (_ , Group-on.⋆-equivr (ℤ {ℓ} .snd) (lift a)) .snd) ⟩ - lower (pow ℤ (lift a) b) +ℤ a ≡ a *ℤ b +ℤ a ≃⟨ ∙-pre-equiv (ap lower (pow-sucr ℤ (lift a) b)) ⟩ - lower (pow ℤ (lift a) (sucℤ b)) ≡ a *ℤ b +ℤ a ≃⟨ ∙-post-equiv (sym (*ℤ-sucr a b)) ⟩ - lower (pow ℤ (lift a) (sucℤ b)) ≡ a *ℤ sucℤ b ≃∎ +pow-ℤ : ∀ a b → pow ℤ a b ≡ a *ℤ b +pow-ℤ a = ℤ.induction (sym (*ℤ-zeror a)) λ b → + pow ℤ a b ≡ a *ℤ b ≃⟨ ap (_+ℤ a) , equiv→cancellable (Group-on.⋆-equivr (ℤ .snd) a) ⟩ + pow ℤ a b +ℤ a ≡ a *ℤ b +ℤ a ≃⟨ ∙-pre-equiv (pow-sucr ℤ a b) ⟩ + pow ℤ a (sucℤ b) ≡ a *ℤ b +ℤ a ≃⟨ ∙-post-equiv (sym (*ℤ-sucr a b)) ⟩ + pow ℤ a (sucℤ b) ≡ a *ℤ sucℤ b ≃∎ ``` ::: @@ -238,9 +241,8 @@ We quickly note that $\ZZ$ is torsion-free, since multiplication by a nonzero integer is injective. ```agda -ℤ-torsion-free : ∀ {ℓ} → is-torsion-free (ℤ {ℓ}) -ℤ-torsion-free (lift n) (k , (k>0 , nk≡0) , _) = ap lift $ - *ℤ-injectiver (pos k) n 0 - (λ p → <-not-equal k>0 (pos-injective (sym p))) - (sym (pow-ℤ n (pos k)) ∙ ap Lift.lower nk≡0) +ℤ-torsion-free : is-torsion-free ℤ +ℤ-torsion-free n (k , (k>0 , nk≡0) , _) = *ℤ-injectiver (pos k) n 0 + (λ p → <-not-equal k>0 (pos-injective (sym p))) + (sym (pow-ℤ n (pos k)) ∙ nk≡0) ``` diff --git a/src/Data/Int/DivMod.lagda.md b/src/Data/Int/DivMod.lagda.md index 779c248d6..a6fa2f9ff 100644 --- a/src/Data/Int/DivMod.lagda.md +++ b/src/Data/Int/DivMod.lagda.md @@ -21,7 +21,7 @@ module Data.Int.DivMod where @@ -85,7 +85,7 @@ $b - (-a)\%b$ as the remainder. lemma = assign neg (q * b + suc r) ≡⟨ ap (assign neg) (+-commutative (q * b) _) ⟩ negsuc (r + q * b) ≡˘⟨ negℤ-+ℤ-negsuc r (q * b) ⟩ - negℤ (pos r) +ℤ negsuc (q * b) ≡⟨ ap (_+ℤ negsuc (q * b)) (ap Lift.lower (ℤ.insertl {h = lift (negℤ (pos b'))} (ap lift (+ℤ-invl (pos b'))) {f = lift (negℤ (pos r))})) ⟩ + negℤ (pos r) +ℤ negsuc (q * b) ≡⟨ ap (_+ℤ negsuc (q * b)) (ℤ.insertl {h = negℤ (pos b')} (+ℤ-invl (pos b')) {f = negℤ (pos r)}) ⟩ ⌜ negℤ (pos b') ⌝ +ℤ (pos b' -ℤ pos r) +ℤ negsuc (q * b) ≡˘⟨ ap¡ (assign-neg b') ⟩ assign neg b' +ℤ (pos b' -ℤ pos r) +ℤ negsuc (q * b) ≡⟨ ap (_+ℤ negsuc (q * b)) (+ℤ-commutative (assign neg b') (pos b' -ℤ pos r)) ⟩ (pos b' -ℤ pos r) +ℤ assign neg b' +ℤ negsuc (q * b) ≡˘⟨ +ℤ-assoc (pos b' -ℤ pos r) _ _ ⟩ @@ -135,7 +135,7 @@ hence it must be zero. b∣r'-r .fst = q -ℤ q' b∣r'-r .snd = (q -ℤ q') *ℤ pos b ≡⟨ *ℤ-distribr-minus (pos b) q q' ⟩ - q *ℤ pos b -ℤ q' *ℤ pos b ≡⟨ ap Lift.lower (ℤ.equal-sum→equal-diff (lift (q *ℤ pos b)) (lift (pos r)) (lift (q' *ℤ pos b)) (lift (pos r')) (ap lift (sym (recover p) ∙ recover p'))) ⟩ + q *ℤ pos b -ℤ q' *ℤ pos b ≡⟨ ℤ.equal-sum→equal-diff (q *ℤ pos b) (pos r) (q' *ℤ pos b) (pos r') (sym (recover p) ∙ recover p') ⟩ pos r' -ℤ pos r ≡⟨ pos-pos r' r ⟩ r' ℕ- r ∎ @@ -186,7 +186,7 @@ divides-diff→same-rem n x y n∣x-y p' : y ≡ (q -ℤ k) *ℤ pos n +ℤ pos r p' = y ≡˘⟨ negℤ-negℤ y ⟩ - negℤ (negℤ y) ≡⟨ ap Lift.lower (ℤ.insertr (ℤ.inversel {lift x}) {f = lift (negℤ (negℤ y))}) ⟩ + negℤ (negℤ y) ≡⟨ ℤ.insertr (ℤ.inversel {x}) {f = negℤ (negℤ y)} ⟩ ⌜ negℤ (negℤ y) +ℤ negℤ x ⌝ +ℤ x ≡⟨ ap! (+ℤ-commutative (negℤ (negℤ y)) _) ⟩ ⌜ negℤ x -ℤ negℤ y ⌝ +ℤ x ≡˘⟨ ap¡ (negℤ-distrib x (negℤ y)) ⟩ negℤ ⌜ x -ℤ y ⌝ +ℤ x ≡˘⟨ ap¡ z ⟩ diff --git a/src/Homotopy/Space/Circle.lagda.md b/src/Homotopy/Space/Circle.lagda.md index a582f8134..ac74cc9a7 100644 --- a/src/Homotopy/Space/Circle.lagda.md +++ b/src/Homotopy/Space/Circle.lagda.md @@ -300,9 +300,9 @@ loopⁿ-+ a = Integers.induction Int-integers π₁S¹≡ℤ : π₁Groupoid.π₁ S¹∙ S¹-is-groupoid ≡ ℤ π₁S¹≡ℤ = sym $ ∫-Path - (total-hom (Equiv.from ΩS¹≃integers ∘ Lift.lower) - (record { pres-⋆ = λ (lift a) (lift b) → loopⁿ-+ a b })) - (∙-is-equiv (Lift-≃ .snd) ((ΩS¹≃integers e⁻¹) .snd)) + (total-hom (Equiv.from ΩS¹≃integers) + (record { pres-⋆ = loopⁿ-+ })) + ((ΩS¹≃integers e⁻¹) .snd) ``` Furthermore, since the loop space of the circle is a set, we automatically