From 36ba29453b23e593a46c256872fc18c9f0d3f6a1 Mon Sep 17 00:00:00 2001 From: Siegmentation Fault Date: Sun, 13 Oct 2024 21:17:32 +0700 Subject: [PATCH] abandon some unsuccessful experiments & format Transformational.lean --- GroundZero.lean | 1 - GroundZero/Algebra/Group/Limited.lean | 132 --- GroundZero/Algebra/Transformational.lean | 170 +-- pictures/dependency-map.svg | 1340 +++++++++++----------- 4 files changed, 720 insertions(+), 923 deletions(-) delete mode 100644 GroundZero/Algebra/Group/Limited.lean diff --git a/GroundZero.lean b/GroundZero.lean index 7c023c6..8e4b577 100644 --- a/GroundZero.lean +++ b/GroundZero.lean @@ -16,7 +16,6 @@ import GroundZero.Algebra.Group.Free import GroundZero.Algebra.Group.Homotopy import GroundZero.Algebra.Group.Isomorphism import GroundZero.Algebra.Group.Lemmas -import GroundZero.Algebra.Group.Limited import GroundZero.Algebra.Group.Periodic import GroundZero.Algebra.Group.Presentation import GroundZero.Algebra.Group.Product diff --git a/GroundZero/Algebra/Group/Limited.lean b/GroundZero/Algebra/Group/Limited.lean deleted file mode 100644 index 69c301b..0000000 --- a/GroundZero/Algebra/Group/Limited.lean +++ /dev/null @@ -1,132 +0,0 @@ -import GroundZero.Algebra.Group.Symmetric -import GroundZero.Algebra.Reals - -open GroundZero.Types.Id (ap) -open GroundZero.Structures -open GroundZero.Types -open GroundZero.HITs - -namespace GroundZero.Algebra - def diameter {M : Metric} (φ : Group.S.carrier M.1) := - im (λ x, M.ρ x (φ.1 x)) - - def limited {M : Metric} (φ : Group.S.carrier M.1) := - ∥Σ m, Π x, R.ρ (M.ρ x (φ.1 x)) m∥ - - noncomputable hott def diameter.majorizedIfLimited {M : Metric} - (φ : Group.S.carrier M.1) : limited φ → @majorized R.κ (diameter φ) := - begin - apply Merely.lift; intro H; existsi H.1; intro x; apply Merely.rec; apply R.κ.prop; - intro p; apply Equiv.transport (R.ρ · _); apply p.2; apply H.2 - end - - noncomputable hott def lim (M : Metric) : (Group.S M.1).subgroup := - begin - fapply Sigma.mk; existsi @limited M; intro; apply Merely.uniq; apply Prod.mk; - { apply Merely.elem; existsi R.τ.zero; intro x; - apply Equiv.transport (R.ρ · _); symmetry; - apply M.refl; apply @reflexive.refl R.κ }; apply Prod.mk; - { intros a b; apply Merely.lift₂; - intros p q; existsi q.1 + p.1; intro x; - apply @transitive.trans R.κ; apply M.triangle; - exact b.1 x; apply ineqAdd; apply q.2; apply p.2 }; - { intro a; apply Merely.lift; intro p; existsi p.1; - intro x; apply Equiv.transport (R.ρ · _); - symmetry; transitivity; apply M.symm; apply ap (M.ρ _); - symmetry; apply Equiv.forwardRight a; apply p.2 } - end - - noncomputable hott def Lim (M : Metric) : Group := - Group.Subgroup (Group.S M.1) (lim M) - - abbrev Lim.carrier (M : Metric) := (Lim M).carrier - noncomputable abbrev Lim.φ {M : Metric} := (Lim M).φ - noncomputable abbrev Lim.ι {M : Metric} := (Lim M).ι - - noncomputable hott def ω (M : Metric⁎) (φ : Lim.carrier M.1) : ℝ := - sup (diameter φ.1) (im.inh _ M.2) (diameter.majorizedIfLimited φ.1 φ.2) - - noncomputable hott def ω.invLe (M : Metric⁎) (φ : Lim.carrier M.1) : R.ρ (ω M (Lim.ι φ)) (ω M φ) := - begin - apply sup.ssubset; intro x; apply Merely.lift; intro ⟨y, p⟩; - existsi (Lim.ι φ).1.1 y; transitivity; apply M.1.symm; - transitivity; apply ap (M.1.ρ · _); - apply φ.1.forwardRight; exact p - end - - noncomputable hott def ω.inv (M : Metric⁎) (φ : Lim.carrier M.1) : ω M (Lim.ι φ) = ω M φ := - begin - apply @antisymmetric.asymm R.κ; apply ω.invLe; - apply Equiv.transport (λ ψ, R.ρ (ω M ψ) (ω M (Lim.ι φ))); - apply @Group.invInv (Lim M.1); apply ω.invLe - end - - noncomputable hott def ω.mulRev (M : Metric⁎) (φ ψ : Lim.carrier M.1) : - R.ρ (ω M (Lim.φ φ ψ)) (ω M ψ + ω M φ) := - begin - apply sup.exact; intro x; apply Merely.rec; apply R.κ.prop; - intro ⟨y, p⟩; induction p; apply @transitive.trans R.κ; - apply M.1.triangle; exact ψ.1.1 y; apply ineqAdd <;> - { apply sup.lawful; apply im.intro } - end - - noncomputable hott def ω.mul (M : Metric⁎) (φ ψ : Lim.carrier M.1) : - R.ρ (ω M (Lim.φ φ ψ)) (ω M φ + ω M ψ) := - begin apply Equiv.transport (R.ρ (ω M (Lim.φ φ ψ))); apply R.τ.addComm; apply ω.mulRev end - - noncomputable hott def Lim.ρ {M : Metric⁎} (g h : Lim.carrier M.1) := - ω M (Lim.φ g (Lim.ι h)) - - noncomputable hott def ω.geZero (M : Metric⁎) (g : Lim.carrier M.1) : R.ρ 0 (ω M g) := - begin - apply Equiv.transport (R.ρ · _); apply sup.singleton; apply sup.sep; - intros x y p; apply Merely.rec; apply R.κ.prop; intro ⟨z, q⟩; - induction p; induction q; apply M.1.positive - end - - noncomputable hott def ω.eqZeroIfLess {M : Metric⁎} - {g : Lim.carrier M.1} : R.ρ (ω M g) 0 → ω M g = 0 := - begin intro p; apply @antisymmetric.asymm R.κ; exact p; apply ω.geZero end - - noncomputable hott def ω.unit (M : Metric⁎) : ω M (Lim M.1).e = 0 := - begin - apply @antisymmetric.asymm R.κ; apply sup.exact; - { intro y; apply Merely.rec; apply R.κ.prop; intro ⟨x, p⟩; - induction p; apply R.leIfEq; apply M.1.refl }; - { apply ω.geZero } - end - - noncomputable hott def ω.unitIfZero (M : Metric⁎) - (φ : Lim.carrier M.1) (p : ω M φ = 0) : φ = (Lim M.1).e := - begin - apply Sigma.prod; apply Ens.prop; apply GroundZero.Theorems.Equiv.equivHmtpyLem; - intro x; apply M.1.eqIfLeZero; apply Equiv.transport (R.ρ (M.1.ρ (φ.1.1 x) x)); - exact p; apply sup.lawful; apply Merely.elem; existsi x; apply M.1.symm - end - - noncomputable hott def Lim.absolute (M : Metric⁎) : absolute (Lim M.1) (ω M) := - begin - apply (_, (_, _)); intro x; apply Prod.mk; apply ω.unitIfZero; - { intro p; transitivity; exact ap (ω M) p; apply ω.unit }; - intro x; symmetry; apply ω.inv; apply ω.mul - end - - noncomputable hott def Lim.metrizable (M : Metric⁎) : metric (@Lim.ρ M) := - Absolute.metrizable (Lim M.1) ⟨ω M, Lim.absolute M⟩ - - noncomputable hott def Limₘ : Metric⁎ → Metric := - λ M, ⟨(Lim M.1).1.1, ⟨Lim.ρ, Lim.metrizable M⟩⟩ - - -- (deterministic) timeout at 'whnf', maximum number of heartbeats (200000) has been reached (use 'set_option maxHeartbeats ' to set the limit) - - --noncomputable hott def Lim.pointed : Metric⁎ → Metric⁎ := λ M, ⟨Limₘ M, (Lim M.1).e⟩ - --notation "Lim⁎" => Lim.pointed - - --noncomputable hott def ω.mulInv (M : Metric⁎) (φ ψ : Lim.carrier M.1) : - -- R.ρ (abs (ω M φ - ω M ψ)) (ω M (Lim.φ φ ψ)) := - --Absolute.mulInv (Lim M.1) ⟨ω M, Lim.absolute M⟩ φ ψ - - --noncomputable hott def ω.continuous (M : Metric⁎) : - -- Π m, continuous⁎ (Lim⁎ M) R⁎ (ω M) m := - --Absolute.continuous (Lim M.1) ⟨ω M, Lim.absolute M⟩ -end GroundZero.Algebra diff --git a/GroundZero/Algebra/Transformational.lean b/GroundZero/Algebra/Transformational.lean index 660418d..8f5f205 100644 --- a/GroundZero/Algebra/Transformational.lean +++ b/GroundZero/Algebra/Transformational.lean @@ -30,7 +30,7 @@ namespace GroundZero.Algebra (trans : Π x y z, G.φ (ι x y) (ι y z) = ι x z) (full : Π g x, contr (Σ y, ι x y = g)) - def rga (M : Type u) (G : Group) := + hott definition rga (M : Type u) (G : Group) := Σ (φ : G ⮎ M), regular φ namespace gis @@ -39,8 +39,8 @@ namespace GroundZero.Algebra variable (L : gis M G) (K : gis N G) variable (f : M → N) - def preserving := Π x y, K.ι (f x) (f y) = L.ι x y - def reversing := Π x y, K.ι (f x) (f y) = L.ι y x + hott definition preserving := Π x y, K.ι (f x) (f y) = L.ι x y + hott definition reversing := Π x y, K.ι (f x) (f y) = L.ι y x end section @@ -48,19 +48,19 @@ namespace GroundZero.Algebra variable (L : gis A G) (K : gis B G) (N : gis C G) variable {f : B → C} {h : A → B} - hott def reversing.comp₁ (F : reversing K N f) (H : preserving L K h) : + hott lemma reversing.comp₁ (F : reversing K N f) (H : preserving L K h) : reversing L N (f ∘ h) := begin intros x y; transitivity; apply F; apply H end - hott def reversing.comp₂ (F : preserving K N f) (H : reversing L K h) : + hott lemma reversing.comp₂ (F : preserving K N f) (H : reversing L K h) : reversing L N (f ∘ h) := begin intros x y; transitivity; apply F; apply H end - hott def reversing.comp₃ (F : reversing K N f) (H : reversing L K h) : + hott lemma reversing.comp₃ (F : reversing K N f) (H : reversing L K h) : preserving L N (f ∘ h) := begin intros x y; transitivity; apply F; apply H end - hott def reversing.comp₄ (F : preserving K N f) (H : preserving L K h) : + hott lemma reversing.comp₄ (F : preserving K N f) (H : preserving L K h) : preserving L N (f ∘ h) := begin intros x y; transitivity; apply F; apply H end end @@ -70,31 +70,31 @@ namespace GroundZero.Algebra local infixl:70 " * " => G.φ local postfix:max (priority := high) "⁻¹" => G.ι - hott def neut : Π x, L.ι x x = G.e := + hott lemma neut : Π x, L.ι x x = G.e := begin intro; apply Group.unitOfSqr; apply L.trans end - hott def neut₂ (x y : M) : L.ι x x = L.ι y y := + hott lemma neut₂ (x y : M) : L.ι x x = L.ι y y := neut L x ⬝ Id.inv (neut L y) - hott def inv : Π x y, (L.ι x y)⁻¹ = L.ι y x := + hott lemma inv : Π x y, (L.ι x y)⁻¹ = L.ι y x := begin intros x y; apply Group.invEqOfMulEqOne; transitivity; apply L.trans; apply gis.neut end - hott def invTrans (x y z : M) : (L.ι x y)⁻¹ * (L.ι x z) = L.ι y z := + hott lemma invTrans (x y z : M) : (L.ι x y)⁻¹ * (L.ι x z) = L.ι y z := begin transitivity; apply ap (G.φ · (L.ι x z)); apply inv; apply L.trans end - hott def transInv (x y z : M) : (L.ι x y) * (L.ι z y)⁻¹ = L.ι x z := + hott lemma transInv (x y z : M) : (L.ι x y) * (L.ι z y)⁻¹ = L.ι x z := begin transitivity; apply ap; apply inv; apply L.trans end hott corollary propι : Π g x, prop (Σ y, L.ι x y = g) := λ g x, contrImplProp (L.full g x) - hott def fixι : Π g x, Σ y, L.ι x y = g := + hott definition fixι : Π g x, Σ y, L.ι x y = g := λ g x, (L.full g x).1 - hott def zero {x y : M} (p : L.ι x y = G.e) : x = y := + hott lemma zero {x y : M} (p : L.ι x y = G.e) : x = y := let q := L.propι (L.ι x y) x ⟨y, Id.refl⟩ ⟨x, L.neut x ⬝ Id.inv p⟩; ap Sigma.fst (Id.inv q) @@ -114,13 +114,13 @@ namespace GroundZero.Algebra exact Id.inv p end - hott def injεᵣ (x y z : M) (H : hset M) : (L.ι z x = L.ι z y) ≃ x = y := + hott lemma injεᵣ (x y z : M) (H : hset M) : (L.ι z x = L.ι z y) ≃ x = y := begin apply propEquivLemma; apply G.hset; apply H; exact injιᵣ L; intro p; induction p; reflexivity end - hott def prod {M₁ : Type u} {M₂ : Type v} {G H : Group} : gis M₁ G → gis M₂ H → gis (M₁ × M₂) (G × H) := + hott theorem prod {M₁ : Type u} {M₂ : Type v} {G H : Group} : gis M₁ G → gis M₂ H → gis (M₁ × M₂) (G × H) := begin intros L K; refine ⟨?_, ?_, ?_⟩; { intros m₁ m₂; fapply Prod.mk; @@ -142,10 +142,10 @@ namespace GroundZero.Algebra { apply Structures.prodHset; apply G.hset; apply H.hset } } } end - hott def octave.hrel (φ : G.subset) : hrel M := + hott definition octave.hrel (φ : G.subset) : hrel M := λ a b, ⟨L.ι a b ∈ φ, Ens.prop (L.ι a b) φ⟩ - hott def octave (φ : G.subgroup) : eqrel M := + hott definition octave (φ : G.subgroup) : eqrel M := begin existsi octave.hrel L φ.set; apply Prod.mk; { intro a; apply transport (· ∈ φ.set); @@ -156,7 +156,7 @@ namespace GroundZero.Algebra apply L.trans a b c; apply φ.mul <;> assumption } end - hott def oct (φ : G.subgroup) := Relquot (octave L φ) + hott definition oct (φ : G.subgroup) := Relquot (octave L φ) hott theorem normal (φ : G.normal) {a₁ a₂ b₁ b₂ : M} (p : L.ι a₁ b₁ ∈ φ.set) (q : L.ι a₂ b₂ ∈ φ.set) : G.φ (L.ι a₁ a₂)⁻¹ (L.ι b₁ b₂) ∈ φ.set := @@ -179,13 +179,13 @@ namespace GroundZero.Algebra end -- Transposition - hott def τ (i : G.carrier) : M → M := + hott definition τ (i : G.carrier) : M → M := λ x, (L.fixι i x).1 - hott def τ.lawful : Π i x, L.ι x (L.τ i x) = i := + hott definition τ.lawful : Π i x, L.ι x (L.τ i x) = i := λ i x, (L.fixι i x).2 - hott def τ.comp : Π i j x, L.τ i (L.τ j x) = L.τ (j * i) x := + hott definition τ.comp : Π i j x, L.τ i (L.τ j x) = L.τ (j * i) x := begin intros i j x; apply @injιᵣ M G L _ _ x; transitivity; symmetry; apply L.trans; exact L.τ j x; @@ -193,14 +193,14 @@ namespace GroundZero.Algebra symmetry; apply τ.lawful end - hott def τ.id : Π x, L.τ G.e x = x := + hott lemma τ.id : Π x, L.τ G.e x = x := begin intro x; apply @injιᵣ M G L _ _ x; transitivity; apply τ.lawful; symmetry; apply L.neut end - hott def τ.biinv (i : G.carrier) : biinv (L.τ i) := + hott theorem τ.biinv (i : G.carrier) : biinv (L.τ i) := begin apply Prod.mk <;> existsi L.τ i⁻¹ <;> { intro x; transitivity; apply τ.comp; @@ -209,16 +209,16 @@ namespace GroundZero.Algebra apply τ.id } end - hott def τ.tauto {a b : M} : L.τ (L.ι a b) a = b := + hott lemma τ.tauto {a b : M} : L.τ (L.ι a b) a = b := begin apply @injιᵣ M G L _ _ a; apply τ.lawful end - hott def τ.inj {g h : G.carrier} (x : M) (p : L.τ g x = L.τ h x) : g = h := + hott lemma τ.inj {g h : G.carrier} (x : M) (p : L.τ g x = L.τ h x) : g = h := Id.inv (τ.lawful L g x) ⬝ ap (L.ι x) p ⬝ τ.lawful L h x - hott def τ.act : Gᵒᵖ ⮎ M := + hott definition τ.act : Gᵒᵖ ⮎ M := ⟨L.τ, (τ.id L, τ.comp L)⟩ - hott def τ.reg (H : hset M) : regular (τ.act L) := + hott theorem τ.reg (H : hset M) : regular (τ.act L) := begin intros a b; fapply Sigma.mk; { existsi L.ι a b; apply τ.tauto }; @@ -228,7 +228,7 @@ namespace GroundZero.Algebra { apply H } } end - hott def preserving.comm {f : M → M} {i : G.carrier} + hott lemma preserving.comm {f : M → M} {i : G.carrier} (H : preserving L L f) : L.τ i ∘ f ~ f ∘ L.τ i := begin intro x; apply @injιᵣ M G L _ _ (f x); @@ -237,7 +237,7 @@ namespace GroundZero.Algebra apply τ.lawful end - hott def preserving.abelian (m : M) (H : Π i, preserving L L (L.τ i)) : G.isCommutative := + hott lemma preserving.abelian (m : M) (H : Π i, preserving L L (L.τ i)) : G.isCommutative := begin intros i j; apply τ.inj L m; transitivity; { symmetry; apply τ.comp }; @@ -245,10 +245,10 @@ namespace GroundZero.Algebra apply preserving.comm; apply H end - hott def preserving.id : preserving L L id := + hott lemma preserving.id : preserving L L id := λ x y, idp (L.ι x y) - hott def reversing.acomm {f : M → M} {i : G.carrier} + hott lemma reversing.acomm {f : M → M} {i : G.carrier} (H : reversing L L f) : L.τ i⁻¹ ∘ f ~ f ∘ L.τ i := begin intro x; apply @injιᵣ M G L _ _ (f x); @@ -258,14 +258,14 @@ namespace GroundZero.Algebra apply ap; apply τ.lawful end - hott def reversing.acommᵣ {f : M → M} {i : G.carrier} + hott lemma reversing.acommᵣ {f : M → M} {i : G.carrier} (H : reversing L L f) : L.τ i ∘ f ~ f ∘ L.τ i⁻¹ := begin apply transport (λ j, L.τ j ∘ f ~ f ∘ L.τ i⁻¹); apply invInv; apply reversing.acomm L H end - hott def reversing.unitSqr (m : M) + hott lemma reversing.unitSqr (m : M) (H : Π i, reversing L L (L.τ i)) : Π i, G.φ i i = G.e := begin intros i; apply τ.inj L m; @@ -275,25 +275,25 @@ namespace GroundZero.Algebra apply G.mulLeftInv end - hott def reversing.abelian (m : M) + hott theorem reversing.abelian (m : M) (H : Π i, reversing L L (L.τ i)) : G.isCommutative := Group.sqrUnitImplsAbelian (reversing.unitSqr L m H) - hott def π (i : G.carrier) (a b : M) : M := - (L.fixι (G.φ i (L.ι a b)) a).fst + hott definition π (i : G.carrier) (a b : M) : M := + (L.fixι (G.φ i (L.ι a b)) a).1 - hott def π.lawful {i : G.carrier} (a b : M) : + hott definition π.lawful {i : G.carrier} (a b : M) : L.ι a (L.π i a b) = G.φ i (L.ι a b) := - (L.fixι (G.φ i (L.ι a b)) a).snd + (L.fixι (G.φ i (L.ι a b)) a).2 - hott def τ.mulRight {i : G.carrier} (a b : M) : + hott definition τ.mulRight {i : G.carrier} (a b : M) : L.ι a (L.τ i b) = G.φ (L.ι a b) i := begin transitivity; { symmetry; apply L.trans _ b _ }; apply ap; apply τ.lawful end - hott def π.conjugate {i : G.carrier} (a b : M) : + hott definition π.conjugate {i : G.carrier} (a b : M) : L.ι a (L.π i⁻¹ a (L.τ i b)) = Group.conjugate (L.ι a b) i := begin transitivity; { apply π.lawful }; @@ -301,7 +301,7 @@ namespace GroundZero.Algebra symmetry; apply G.mulAssoc end - hott def π.preserving {i : G.carrier} (x : M) : preserving L L (L.π i x) := + hott lemma π.preserving {i : G.carrier} (x : M) : preserving L L (L.π i x) := begin intros a b; transitivity; { symmetry; apply L.trans _ x }; transitivity; apply ap; apply π.lawful; @@ -315,7 +315,7 @@ namespace GroundZero.Algebra apply G.mulLeftInv; apply G.oneMul; apply invTrans end - hott def π.uniq₁ {f : M → M} (H : gis.preserving L L f) + hott lemma π.uniq₁ {f : M → M} (H : gis.preserving L L f) (m : M) : L.π (L.ι m (f m)) (f m) ~ f := begin intro n; apply @injιᵣ M G L _ _ (f m); @@ -324,7 +324,7 @@ namespace GroundZero.Algebra symmetry; apply H end - hott def π.uniq₂ {f : M → M} (H : gis.preserving L L f) + hott lemma π.uniq₂ {f : M → M} (H : gis.preserving L L f) (m : M) : L.π (L.ι m (f m)) m ~ f := begin intro n; apply @injιᵣ M G L _ _ m; @@ -334,7 +334,7 @@ namespace GroundZero.Algebra apply ap; apply H end - hott def τ.abelianImplPreserving (ρ : G.isCommutative) : + hott lemma τ.abelianImplPreserving (ρ : G.isCommutative) : Π i, preserving L L (L.τ i) := begin intros i a b; @@ -351,14 +351,14 @@ namespace GroundZero.Algebra apply G.mulLeftInv; apply G.oneMul end - hott def τ.π (ρ : G.isCommutative) (m : M) : Π i, L.π i m ~ L.τ i := + hott theorem τ.π (ρ : G.isCommutative) (m : M) : Π i, L.π i m ~ L.τ i := begin intro i; apply transport (λ j, L.π j m ~ L.τ i); apply τ.lawful L i m; apply π.uniq₂; apply τ.abelianImplPreserving _ ρ end - hott def π.comp (i j : G.carrier) {m : M} : + hott lemma π.comp (i j : G.carrier) {m : M} : L.π i m ∘ L.π j m ~ L.π (i * j) m := begin intro n; apply @injιᵣ M G L _ _ m; @@ -367,13 +367,13 @@ namespace GroundZero.Algebra symmetry; transitivity; apply π.lawful; apply G.mulAssoc end - hott def π.id (m : M) : L.π G.e m ~ id := + hott lemma π.id (m : M) : L.π G.e m ~ id := begin intro n; apply @injιᵣ M G L _ _ m; transitivity; apply π.lawful; apply G.oneMul end - hott def π.biinv (i : G.carrier) (m : M) : biinv (L.π i m) := + hott lemma π.biinv (i : G.carrier) (m : M) : biinv (L.π i m) := begin apply Prod.mk <;> existsi L.π i⁻¹ m <;> { intro x; transitivity; apply π.comp; @@ -382,24 +382,24 @@ namespace GroundZero.Algebra apply π.id } end - hott def preserving.biinv {f : M → M} + hott theorem preserving.biinv {f : M → M} (H : preserving L L f) (m : M) : biinv f := transport Equiv.biinv (Theorems.funext (π.uniq₂ L H m)) (π.biinv L (L.ι m (f m)) m) - hott def ρ (u v : M) : M → M := + hott definition ρ (u v : M) : M → M := λ x, (L.fixι (L.ι x u) v).fst - hott def ρ.lawful (u v x : M) : L.ι v (L.ρ u v x) = L.ι x u := + hott definition ρ.lawful (u v x : M) : L.ι v (L.ρ u v x) = L.ι x u := (L.fixι (L.ι x u) v).snd - hott def ρ.ι (u v a b : M) : L.ι a (L.ρ u v b) = L.ι a v * L.ι b u := + hott definition ρ.ι (u v a b : M) : L.ι a (L.ρ u v b) = L.ι a v * L.ι b u := begin transitivity; symmetry; apply L.trans _ v _; apply ap; apply ρ.lawful end - hott def ρ.inv (u v : M) : ρ L u v ∘ ρ L v u ~ id := + hott lemma ρ.inv (u v : M) : ρ L u v ∘ ρ L v u ~ id := begin intro m; apply @injιᵣ M G L _ _ m; transitivity; apply ρ.ι; @@ -414,7 +414,7 @@ namespace GroundZero.Algebra transitivity; apply gis.inv; apply neut₂ end - hott def ρ.biinv (u v : M) : biinv (ρ L u v) := + hott theorem ρ.biinv (u v : M) : biinv (ρ L u v) := begin apply Prod.mk <;> existsi ρ L v u <;> apply ρ.inv end section @@ -451,10 +451,10 @@ namespace GroundZero.Algebra end end - hott def rga.decode (H : hset M) : gis M G → rga M Gᵒᵖ := + hott definition rga.decode (H : hset M) : gis M G → rga M Gᵒᵖ := λ L, ⟨τ.act L, τ.reg L H⟩ - hott def rga.encode : rga M Gᵒᵖ → gis M G := + hott definition rga.encode : rga M Gᵒᵖ → gis M G := λ ⟨φ, H⟩, ⟨λ a b, (H a b).1.1, begin intros x y z; apply (regular.elim φ H).2 x; @@ -490,12 +490,12 @@ namespace GroundZero.Algebra { intro; apply gis.id; reflexivity } end - noncomputable hott def rga.eqv' (G : Group) + noncomputable hott definition rga.eqv' (G : Group) (H : hset M) : rga M G ≃ gis M G := @transport Group (λ H, @rga M H ≃ gis M G) Gᵒᵖ G (Id.inv (Iso.ua Op.iso)) (rga.eqv H) - hott def reversing.ι (f : M → M) (H : reversing L L f) : + hott lemma reversing.ι (f : M → M) (H : reversing L L f) : Π a b, L.ι a (f b) = L.ι a (f a) * (L.ι a b)⁻¹ := begin intros a b; transitivity; symmetry; apply L.trans a (f a); @@ -516,56 +516,4 @@ namespace GroundZero.Algebra (H : reversing L L f) (m : M) : biinv f := transport Equiv.biinv (Theorems.funext (reversing.desc L f H m)) (ρ.biinv L m (f m)) end gis - - namespace Dodecaphony - - -- In case of A = {C, C♯, D, D♯, E, F, ...}, - -- this is 12 ordered notes - abbrev P (A : 0-Type) := A ≃₀ A - - def L (A : Type u) := Σ n, Finite n → A - - def L.length {A : Type u} : L A → ℕ := Sigma.fst - def L.nth {A : Type u} (xs : L A) : Finite xs.length → A := xs.snd - - hott def L.all {A : Type u} (π : A → Prop) (xs : L A) : Prop := - ⟨Π n, (π (xs.nth n)).fst, begin apply piProp; intro; apply (π _).2 end⟩ - - -- Set of (12 × n) ordered notes, where n ∈ ℕ - def M (A : 0-Type) := L (P A) - - def Tr (A : 0-Type) := - zeroeqv (Theorems.Equiv.zeroEquiv.hset A A) - - -- Set of *all* tone row transformations - abbrev T (A : 0-Type) := S (Tr A) - - section - variable {A : 0-Type} (φ : (T A).subgroup) - - -- Tone row transformations in terms of φ ≤ T A - def tr := (@S.ap (Tr A)).cut φ - - -- Set of tone rows - def R := Orbits (tr φ) - - hott def M.dodecaphonic (xs : M A) (r : P A) : Prop := - xs.all (λ x, ⟨x ∈ orbit (tr φ) r, Ens.prop x _⟩) - - noncomputable hott def R.dodecaphonic (xs : M A) (r : R φ) : Prop := - begin - fapply Relquot.rec _ _ _ r; - { exact M.dodecaphonic φ xs }; - { intros x y p; fapply Theorems.Equiv.propset.Id; - apply GroundZero.ua; apply equivFunext; - intro z; apply propEquivLemma; - change prop (_ ∈ orbit (tr φ) x); apply Ens.prop; - change prop (_ ∈ orbit (tr φ) y); apply Ens.prop; - apply orbit.subset; exact p; - apply orbit.subset; apply leftAction.symm; exact p }; - { apply Theorems.Equiv.propsetIsSet } - end - end - - end Dodecaphony end GroundZero.Algebra diff --git a/pictures/dependency-map.svg b/pictures/dependency-map.svg index 6ea4c5e..b852496 100644 --- a/pictures/dependency-map.svg +++ b/pictures/dependency-map.svg @@ -4,52 +4,52 @@ - + dependencyMap - + Algebra/Basic - -Algebra/Basic + +Algebra/Basic Algebra/Category - -Algebra/Category + +Algebra/Category Algebra/Basic->Algebra/Category - - + + Algebra/Geometry - -Algebra/Geometry + +Algebra/Geometry Algebra/Basic->Algebra/Geometry - - + + Algebra/Group/Basic - -Algebra/Group/Basic + +Algebra/Group/Basic Algebra/Basic->Algebra/Group/Basic - - + + @@ -60,1406 +60,1388 @@ Algebra/Basic->Algebra/Monoid - + Algebra/Group/Automorphism - -Algebra/Group/Automorphism + +Algebra/Group/Automorphism Algebra/Group/Basic->Algebra/Group/Automorphism - - + + Algebra/EilenbergMacLane - -Algebra/EilenbergMacLane + +Algebra/EilenbergMacLane Algebra/Group/Basic->Algebra/EilenbergMacLane - - + + Algebra/Group/Absolutizer - -Algebra/Group/Absolutizer + +Algebra/Group/Absolutizer Algebra/Group/Basic->Algebra/Group/Absolutizer - - + + Algebra/Group/Finite - -Algebra/Group/Finite + +Algebra/Group/Finite Algebra/Group/Basic->Algebra/Group/Finite - - + + Algebra/Group/Free - -Algebra/Group/Free + +Algebra/Group/Free Algebra/Group/Basic->Algebra/Group/Free - - + + Algebra/Group/Homotopy - -Algebra/Group/Homotopy + +Algebra/Group/Homotopy Algebra/Group/Basic->Algebra/Group/Homotopy - - + + Algebra/Group/Periodic - -Algebra/Group/Periodic + +Algebra/Group/Periodic Algebra/Group/Basic->Algebra/Group/Periodic - - + + Algebra/Group/Product - -Algebra/Group/Product + +Algebra/Group/Product Algebra/Group/Basic->Algebra/Group/Product - - + + Algebra/Group/Subgroup - -Algebra/Group/Subgroup + +Algebra/Group/Subgroup Algebra/Group/Basic->Algebra/Group/Subgroup - - + + Algebra/Group/Action - -Algebra/Group/Action + +Algebra/Group/Action Algebra/Transformational - -Algebra/Transformational + +Algebra/Transformational Algebra/Group/Action->Algebra/Transformational - - + + Algebra/Group/Semidirect - -Algebra/Group/Semidirect + +Algebra/Group/Semidirect Algebra/Group/Automorphism->Algebra/Group/Semidirect - - + + Algebra/Group/Presentation - -Algebra/Group/Presentation + +Algebra/Group/Presentation Algebra/Group/Free->Algebra/Group/Presentation - - + + Algebra/Group/Product->Algebra/Transformational - - + + Algebra/Group/Factor - -Algebra/Group/Factor + +Algebra/Group/Factor Algebra/Group/Subgroup->Algebra/Group/Factor - - + + Algebra/Group/Differential - -Algebra/Group/Differential + +Algebra/Group/Differential Algebra/Group/Subgroup->Algebra/Group/Differential - - + + Algebra/Group/Lemmas - -Algebra/Group/Lemmas + +Algebra/Group/Lemmas Algebra/Group/Subgroup->Algebra/Group/Lemmas - - + + Algebra/Group/Symmetric - -Algebra/Group/Symmetric + +Algebra/Group/Symmetric Algebra/Group/Subgroup->Algebra/Group/Symmetric - - + + Algebra/Group/Alternating - -Algebra/Group/Alternating + +Algebra/Group/Alternating Algebra/Group/Factor->Algebra/Group/Alternating - - + + Algebra/Group/Isomorphism - -Algebra/Group/Isomorphism + +Algebra/Group/Isomorphism Algebra/Group/Factor->Algebra/Group/Isomorphism - - + + Algebra/Ring - -Algebra/Ring + +Algebra/Ring Algebra/Group/Factor->Algebra/Ring - - + + Algebra/Group/Isomorphism->Algebra/Group/Presentation - - + + - + Algebra/Orgraph - -Algebra/Orgraph + +Algebra/Orgraph - + Algebra/Ring->Algebra/Orgraph - - + + - + Algebra/Boolean - -Algebra/Boolean + +Algebra/Boolean - + Algebra/Ring->Algebra/Boolean - - + + Algebra/Group/Symmetric->Algebra/Group/Action - - + + Algebra/Group/Symmetric->Algebra/Group/Isomorphism - - - - - -Algebra/Group/Limited - -Algebra/Group/Limited - - - -Algebra/Group/Symmetric->Algebra/Group/Limited - - + + - + Algebra/Group/Z - -Algebra/Group/Z + +Algebra/Group/Z - + Algebra/Group/Symmetric->Algebra/Group/Z - - + + - + Algebra/Reals - -Algebra/Reals + +Algebra/Reals - + Algebra/Orgraph->Algebra/Reals - - - - - -Algebra/Reals->Algebra/Group/Limited - - + + - + HITs/Topologization - -HITs/Topologization + +HITs/Topologization - + Algebra/Reals->HITs/Topologization - - + + - + Cubical/Path - -Cubical/Path + +Cubical/Path - + Cubical/Connection - -Cubical/Connection + +Cubical/Connection - + Cubical/Path->Cubical/Connection - - + + - + Cubical/V - -Cubical/V + +Cubical/V - + Cubical/Path->Cubical/V - - + + - + Cubical/Example - -Cubical/Example + +Cubical/Example - + Cubical/V->Cubical/Example - - + + - + Exercises/Chap1 - -Exercises/Chap1 + +Exercises/Chap1 - + Exercises/Chap3 - -Exercises/Chap3 + +Exercises/Chap3 - + Exercises/Chap1->Exercises/Chap3 - - + + - + Exercises/Chap2 - -Exercises/Chap2 + +Exercises/Chap2 - + Exercises/Chap4 - -Exercises/Chap4 + +Exercises/Chap4 - + Exercises/Chap2->Exercises/Chap4 - - + + - + Exercises/Chap5 - -Exercises/Chap5 + +Exercises/Chap5 - + Exercises/Chap4->Exercises/Chap5 - - + + - + HITs/Circle - -HITs/Circle + +HITs/Circle - + HITs/Circle->Algebra/Group/Z - - + + - + HITs/Circle->Exercises/Chap4 - - + + - + HITs/Moebius - -HITs/Moebius + +HITs/Moebius - + HITs/Circle->HITs/Moebius - - + + - + HITs/Reals - -HITs/Reals + +HITs/Reals - + HITs/Circle->HITs/Reals - - + + - + HITs/Sphere - -HITs/Sphere + +HITs/Sphere - + HITs/Circle->HITs/Sphere - - + + - + Theorems/Hopf - -Theorems/Hopf + +Theorems/Hopf - + HITs/Circle->Theorems/Hopf - - + + - + Types/CellComplex - -Types/CellComplex + +Types/CellComplex - + HITs/Sphere->Types/CellComplex - - + + - + HITs/Coequalizer - -HITs/Coequalizer + +HITs/Coequalizer - + HITs/Flattening - -HITs/Flattening + +HITs/Flattening - + HITs/Coequalizer->HITs/Flattening - - + + - + HITs/Colimit - -HITs/Colimit + +HITs/Colimit - + HITs/Merely - -HITs/Merely + +HITs/Merely - + HITs/Colimit->HITs/Merely - - + + - + Theorems/Equiv - -Theorems/Equiv + +Theorems/Equiv - + HITs/Merely->Theorems/Equiv - - + + - + HITs/Simplicial - -HITs/Simplicial + +HITs/Simplicial - + HITs/Merely->HITs/Simplicial - - + + - + HITs/Trunc - -HITs/Trunc + +HITs/Trunc - + HITs/Merely->HITs/Trunc - - + + - + Theorems/Functions - -Theorems/Functions + +Theorems/Functions - + HITs/Merely->Theorems/Functions - - + + - + HITs/Generalized - -HITs/Generalized + +HITs/Generalized - + HITs/Generalized->HITs/Merely - - + + - + HITs/Interval - -HITs/Interval + +HITs/Interval - + HITs/Interval->Cubical/Path - - + + - + Cubical/Cubes - -Cubical/Cubes + +Cubical/Cubes - + HITs/Interval->Cubical/Cubes - - + + - + HITs/Interval->Theorems/Equiv - - + + - + Theorems/Fibration - -Theorems/Fibration + +Theorems/Fibration - + HITs/Interval->Theorems/Fibration - - + + - + Theorems/Equiv->Exercises/Chap3 - - + + - + Theorems/Equiv->Exercises/Chap4 - - + + - + Theorems/Pullback - -Theorems/Pullback + +Theorems/Pullback - + Theorems/Equiv->Theorems/Pullback - - + + - + Theorems/Univalence - -Theorems/Univalence + +Theorems/Univalence - + Theorems/Equiv->Theorems/Univalence - - + + - + Types/Precategory - -Types/Precategory + +Types/Precategory - + Theorems/Equiv->Types/Precategory - - + + - + Theorems/Fibration->Theorems/Hopf - - + + - + HITs/Trunc->Algebra/Monoid - + - + HITs/Trunc->Algebra/EilenbergMacLane - - + + - + HITs/Trunc->Algebra/Group/Homotopy - - + + - + HITs/Trunc->HITs/Sphere - - + + - + HITs/Setquot - -HITs/Setquot + +HITs/Setquot - + HITs/Trunc->HITs/Setquot - - + + - + Theorems/Connectedness Theorems/Connectedness - + HITs/Trunc->Theorems/Connectedness - + - + Theorems/Functions->Exercises/Chap4 - - + + - + Modal/Etale - -Modal/Etale + +Modal/Etale - + Theorems/Functions->Modal/Etale - - + + - + Theorems/Functions->Theorems/Univalence - - + + - + Theorems/Functions->Types/Precategory - - + + - + HITs/Pushout - -HITs/Pushout + +HITs/Pushout - + HITs/Suspension - -HITs/Suspension + +HITs/Suspension - + HITs/Pushout->HITs/Suspension - - + + - + HITs/Wedge - -HITs/Wedge + +HITs/Wedge - + HITs/Pushout->HITs/Wedge - - + + - + HITs/Suspension->Algebra/EilenbergMacLane - - + + - + HITs/Suspension->HITs/Circle - - + + - + HITs/Join - -HITs/Join + +HITs/Join - + HITs/Suspension->HITs/Join - - + + - + HITs/Quotient - -HITs/Quotient + +HITs/Quotient - + HITs/Quotient->HITs/Coequalizer - - + + - + HITs/Quotient->HITs/Colimit - - + + - + HITs/Quotient->HITs/Generalized - - + + - + HITs/Quotient->HITs/Pushout - - + + - + HITs/Setquot->Algebra/Group/Action - - + + - + HITs/Setquot->Algebra/Group/Absolutizer - - + + - + HITs/Setquot->Algebra/Group/Factor - - + + - + Meta/Basic - -Meta/Basic + +Meta/Basic - + Proto - -Proto + +Proto - + Meta/Basic->Proto - - + + - + Theorems/Ontological - -Theorems/Ontological + +Theorems/Ontological - + Proto->Theorems/Ontological - - + + - + Types/Id - -Types/Id + +Types/Id - + Proto->Types/Id - - + + - + Meta/HottTheory - -Meta/HottTheory + +Meta/HottTheory - + Meta/HottTheory->Meta/Basic - - + + - + Meta/Notation - -Meta/Notation + +Meta/Notation - + Meta/Notation->Meta/Basic - - + + - + Meta/Tactic - -Meta/Tactic + +Meta/Tactic - + Meta/Tactic->Meta/Basic - - + + - + Meta/Trust - -Meta/Trust + +Meta/Trust - + Types/Equiv - -Types/Equiv + +Types/Equiv - + Meta/Trust->Types/Equiv - - + + - + Modal/Infinitesimal - -Modal/Infinitesimal + +Modal/Infinitesimal - + Types/Equiv->Modal/Infinitesimal - - + + - + Types/Coproduct - -Types/Coproduct + +Types/Coproduct - + Types/Equiv->Types/Coproduct - - + + - + Types/HEq - -Types/HEq + +Types/HEq - + Types/Equiv->Types/HEq - - + + - + Types/Lost - -Types/Lost + +Types/Lost - + Types/Equiv->Types/Lost - - + + - + Types/Sigma - -Types/Sigma + +Types/Sigma - + Types/Equiv->Types/Sigma - - + + - + Types/Unit - -Types/Unit + +Types/Unit - + Types/Equiv->Types/Unit - - + + - + Modal/Disc - -Modal/Disc + +Modal/Disc - + Modal/Disc->Modal/Etale - - + + - + Modal/Infinitesimal->Modal/Disc - - + + - + Types/Id->Meta/Trust - - + + - + Structures - -Structures + +Structures - + Structures->HITs/Merely - - + + - + Structures->HITs/Interval - - + + - + Structures->Modal/Disc - - + + - + Theorems/Weak - -Theorems/Weak + +Theorems/Weak - + Structures->Theorems/Weak - - + + - + Types/Nat - -Types/Nat + +Types/Nat - + Structures->Types/Nat - - + + - + Theorems/Nat - -Theorems/Nat + +Theorems/Nat - + Types/Nat->Theorems/Nat - - + + - + Theorems/Classical - -Theorems/Classical + +Theorems/Classical - + Theorems/Classical->Algebra/Category - - + + - + Theorems/Classical->Algebra/Orgraph - - + + - + Theorems/Pullback->Exercises/Chap2 - - + + - + Theorems/Univalence->Cubical/V - - + + - + Theorems/Univalence->Exercises/Chap2 - - + + - + Theorems/Univalence->HITs/Circle - - + + - + Theorems/Univalence->HITs/Flattening - - + + - + Theorems/Univalence->Theorems/Connectedness - - + + - + Theorems/Univalence->Theorems/Classical - - + + - + Theorems/Univalence->Theorems/Nat - - + + - + Types/Ens - -Types/Ens + +Types/Ens - + Theorems/Univalence->Types/Ens - - + + - + Types/Category - -Types/Category + +Types/Category - + Types/Precategory->Types/Category - - + + - + Theorems/Funext - -Theorems/Funext + +Theorems/Funext - + Types/Product - -Types/Product + +Types/Product - + Theorems/Funext->Types/Product - - + + - + Types/Product->Exercises/Chap1 - - + + - + Types/Product->Exercises/Chap4 - - + + - + Types/Product->Structures - - + + - + Theorems/Nat->Algebra/Group/Finite - - + + - + Theorems/Nat->Algebra/Group/Lemmas - - + + - + Theorems/Nat->Algebra/Reals - - + + - + Theorems/Nat->Exercises/Chap1 - - + + - + Theorems/Nat->Exercises/Chap4 - - + + - + HITs/Int - -HITs/Int + +HITs/Int - + Theorems/Nat->HITs/Int - - + + - + Types/Integer - -Types/Integer + +Types/Integer - + Theorems/Nat->Types/Integer - - + + - + Types/Integer->HITs/Circle - - + + - + Types/Ens->Algebra/Basic - - + + - + Types/Setquot - -Types/Setquot + +Types/Setquot - + Types/Ens->Types/Setquot - - + + - + Types/Coproduct->Structures - - + + - + Types/HEq->HITs/Quotient - - + + - + Types/HEq->Theorems/Funext - - + + - + Types/Lost->Exercises/Chap3 - - + + - + Types/Lost->Exercises/Chap5 - - + + - + Types/Sigma->Exercises/Chap1 - - + + - + Types/Sigma->Exercises/Chap4 - - + + - + Types/Sigma->Structures - - + + - + Types/Unit->HITs/Suspension - - + + - + Types/Unit->HITs/Wedge - - + + - + Types/Unit->Structures - - + +