diff --git a/GroundZero/Algebra/EilenbergMacLane.lean b/GroundZero/Algebra/EilenbergMacLane.lean index 864ae54..b49276e 100644 --- a/GroundZero/Algebra/EilenbergMacLane.lean +++ b/GroundZero/Algebra/EilenbergMacLane.lean @@ -1,4 +1,7 @@ import GroundZero.Algebra.Group.Basic +import GroundZero.HITs.Suspension +import GroundZero.HITs.Trunc + open GroundZero.Theorems.Functions GroundZero.Theorems.Equiv open GroundZero.Types.Equiv (idtoeqv) open GroundZero.Types.Id (dotted) @@ -200,4 +203,13 @@ namespace K1 end end K1 -end GroundZero.Algebra \ No newline at end of file +hott def ItS (A : Type) : ℕ → Type +| 0 => A +| Nat.succ n => ∑ (ItS A n) + +open GroundZero.HITs (Trunc) + +hott def K (G : Group) (n : ℕ) := +Trunc (hlevel.ofNat (n + 1)) (ItS (K1 G) n) + +end GroundZero.Algebra diff --git a/GroundZero/HITs/Circle.lean b/GroundZero/HITs/Circle.lean index 1dcca73..d7e3b80 100644 --- a/GroundZero/HITs/Circle.lean +++ b/GroundZero/HITs/Circle.lean @@ -332,7 +332,8 @@ namespace Circle apply Sigma.mapFstOverProd end - hott def inv : S¹ → S¹ := Circle.rec base loop⁻¹ + hott def turn : S¹ → S¹ := rec base loop + hott def inv : S¹ → S¹ := rec base loop⁻¹ noncomputable hott def invInv (x : S¹) : inv (inv x) = x := let invₚ := @Id.map S¹ S¹ base base (inv ∘ inv); @@ -513,9 +514,12 @@ namespace Circle def uarec {A : Type u} (φ : A ≃ A) : S¹ → Type u := rec A (ua φ) - hott def Ωrec {A : Type u} (zero : A) (succ pred : A → A) - (p : succ ∘ pred ~ id) (q : pred ∘ succ ~ id) : Ω¹(S¹) → A := - λ r, @transport S¹ (uarec ⟨succ, (⟨pred, q⟩, ⟨pred, p⟩)⟩) base base r zero + abbrev Ωhelix {A : Type u} {succ pred : A → A} (p : succ ∘ pred ~ id) (q : pred ∘ succ ~ id) : S¹ → Type u := + uarec ⟨succ, ⟨pred, q⟩, ⟨pred, p⟩⟩ + + hott def Ωrec {x : S¹} {A : Type u} (zero : A) (succ pred : A → A) + (p : succ ∘ pred ~ id) (q : pred ∘ succ ~ id) : base = x → Ωhelix p q x := + λ r, @transport S¹ (Ωhelix p q) base x r zero section variable {A : Type u} (zero : A) (succ pred : A → A) @@ -588,6 +592,24 @@ namespace Circle apply recβrule₂; apply Id.invComp end + hott def mapLoopEqv {B : Type u} : (S¹ → B) ≃ (Σ (x : B), x = x) := + begin + fapply Sigma.mk; intro φ; exact ⟨φ base, ap φ loop⟩; apply Qinv.toBiinv; + fapply Sigma.mk; intro w; exact rec w.1 w.2; apply Prod.mk; + { intro w; fapply Sigma.prod; exact idp w.1; transitivity; + apply Equiv.transportInvCompComp; transitivity; + apply Id.reflRight; apply recβrule₂ }; + { intro φ; symmetry; apply Theorems.funext; apply mapExt } + end + + hott def recBaseInj (p q : Ω¹(S¹)) (ε : rec base p = rec base q) : p = q := + begin + have θ := ap (subst ε) (recβrule₂ base p)⁻¹ ⬝ apd (λ f, ap f loop) ε ⬝ recβrule₂ base q; + apply transport (p = ·) θ _⁻¹; transitivity; apply Equiv.transportOverHmtpy; + -- somewhat surprisingly commutativity of Ω¹(S¹) arises out of nowhere + transitivity; apply ap (· ⬝ _ ⬝ _); apply Id.mapInv; apply Id.idConjIfComm; apply comm + end + section variable {B : Type u} (b : B) (p q : b = b) (H : p ⬝ q = q ⬝ p) @@ -675,8 +697,7 @@ namespace Circle section variable {A : Type u} {a : A} (B : Π x, a = x → Type v) (w : B a (idp a)) {b : A} (p : a = b) - hott def ΩJ := - transportconst (Interval.happly (apd B p) p) (transportMeet B w p) + hott def ΩJ := transportconst (Interval.happly (apd B p) p) (transportMeet B w p) noncomputable hott def ΩJDef : J₁ B w p = ΩJ B w p := begin induction p; reflexivity end diff --git a/GroundZero/HITs/Suspension.lean b/GroundZero/HITs/Suspension.lean index 65e782b..f84d5e9 100644 --- a/GroundZero/HITs/Suspension.lean +++ b/GroundZero/HITs/Suspension.lean @@ -47,4 +47,4 @@ namespace Suspension end Suspension end HITs -end GroundZero \ No newline at end of file +end GroundZero diff --git a/GroundZero/Types/Equiv.lean b/GroundZero/Types/Equiv.lean index d288fdb..311d540 100644 --- a/GroundZero/Types/Equiv.lean +++ b/GroundZero/Types/Equiv.lean @@ -444,6 +444,14 @@ namespace Equiv transportconst (bimap f p q) u = transport (f a₂) q (transport (f · b₁) p u) := begin induction p; induction q; reflexivity end + hott def transportDiag₁ {A : Type u} (B : A → A → Type v) {a b : A} {p : a = b} (w : B a a) : + transport (λ x, B x x) p w = transport (B b) p (transport (B · a) p w) := + begin induction p; reflexivity end + + hott def transportDiag₂ {A : Type u} (B : A → A → Type v) {a b : A} {p : a = b} (w : B a a) : + transport (λ x, B x x) p w = transport (B · b) p (transport (B a) p w) := + begin induction p; reflexivity end + hott theorem mapOverAS {A : Type u} {a b : A} (f : A → A → A) (g : A → A) (p : a = b) : Id.map (AS f g) p = @bimap A A A a b (g a) (g b) f p (Id.map g p) := begin induction p; reflexivity end @@ -554,4 +562,4 @@ def fib {A : Type u} {B : Type v} (f : A → B) (y : B) := Σ (x : A), f x = y def total {A : Type u} (B : A → Type v) := Σ x, B x def fiberwise {A : Type u} (B : A → Type v) := Π x, B x -end GroundZero.Types \ No newline at end of file +end GroundZero.Types diff --git a/dependency-map.gv b/dependency-map.gv index 08288d7..12626dd 100644 --- a/dependency-map.gv +++ b/dependency-map.gv @@ -141,9 +141,9 @@ digraph dependency_map { } "HITs/Reals" "HITs/Simplicial" - "HITs/Suspension" -> { "HITs/Circle", "HITs/Join" } + "HITs/Suspension" -> { "Algebra/EilenbergMacLane", "HITs/Circle", "HITs/Join" } "HITs/Topologization" - "HITs/Trunc" -> { "Algebra/Monoid", "HITs/Quotient" } + "HITs/Trunc" -> { "Algebra/EilenbergMacLane", "Algebra/Monoid", "HITs/Quotient" } "HITs/Wedge" } diff --git a/pictures/dependency-map.svg b/pictures/dependency-map.svg index 3a82c13..be8171a 100644 --- a/pictures/dependency-map.svg +++ b/pictures/dependency-map.svg @@ -4,1282 +4,1294 @@ - + dependency_map - + Proto - -Proto + +Proto Types/Id - -Types/Id + +Types/Id Proto->Types/Id - - + + Theorems/Ontological - -Theorems/Ontological + +Theorems/Ontological Proto->Theorems/Ontological - - + + Support - -Support + +Support Types/Id->Support - - + + Types/Equiv - -Types/Equiv + +Types/Equiv Support->Types/Equiv - - + + Types/Coproduct - -Types/Coproduct + +Types/Coproduct Types/Equiv->Types/Coproduct - - + + Types/HEq - -Types/HEq + +Types/HEq Types/Equiv->Types/HEq - - + + Modal/Infinitesimal - -Modal/Infinitesimal + +Modal/Infinitesimal Types/Equiv->Modal/Infinitesimal - - + + Types/Lost - -Types/Lost + +Types/Lost Types/Equiv->Types/Lost - - + + Types/Unit - -Types/Unit + +Types/Unit Types/Equiv->Types/Unit - - + + Types/Sigma - -Types/Sigma + +Types/Sigma Types/Equiv->Types/Sigma - - + + Structures - -Structures + +Structures HITs/Interval - -HITs/Interval + +HITs/Interval Structures->HITs/Interval - - + + HITs/Merely - -HITs/Merely + +HITs/Merely Structures->HITs/Merely - - + + HITs/Trunc - -HITs/Trunc + +HITs/Trunc Structures->HITs/Trunc - - + + Types/Nat - -Types/Nat + +Types/Nat Structures->Types/Nat - - + + Modal/Disc - -Modal/Disc + +Modal/Disc Structures->Modal/Disc - - + + Theorems/UA - -Theorems/UA + +Theorems/UA Structures->Theorems/UA - - + + Cubical/Cubes - -Cubical/Cubes + +Cubical/Cubes HITs/Interval->Cubical/Cubes - - + + Cubical/Path - -Cubical/Path + +Cubical/Path HITs/Interval->Cubical/Path - - + + Theorems/Equiv - -Theorems/Equiv + +Theorems/Equiv HITs/Interval->Theorems/Equiv - - + + Theorems/Fibration - -Theorems/Fibration + +Theorems/Fibration HITs/Interval->Theorems/Fibration - - + + HITs/Merely->Theorems/Equiv - - + + HITs/Simplicial - -HITs/Simplicial + +HITs/Simplicial HITs/Merely->HITs/Simplicial - - + + Theorems/Functions - -Theorems/Functions + +Theorems/Functions HITs/Merely->Theorems/Functions - - + + Algebra/Monoid - -Algebra/Monoid + +Algebra/Monoid - + HITs/Trunc->Algebra/Monoid - - + + + + + +Algebra/EilenbergMacLane + +Algebra/EilenbergMacLane + + + +HITs/Trunc->Algebra/EilenbergMacLane + + HITs/Quotient - -HITs/Quotient + +HITs/Quotient - + HITs/Trunc->HITs/Quotient - - + + Theorems/Nat - -Theorems/Nat + +Theorems/Nat Types/Nat->Theorems/Nat - - + + Modal/Etale - -Modal/Etale + +Modal/Etale - + Modal/Disc->Modal/Etale - - + + - + Theorems/UA->Theorems/Nat - - + + HITs/Flattening - -HITs/Flattening + +HITs/Flattening - + Theorems/UA->HITs/Flattening - - + + - + Theorems/UA->Theorems/Equiv - - + + Cubical/V - -Cubical/V + +Cubical/V - + Theorems/UA->Cubical/V - - + + Algebra/Basic - -Algebra/Basic + +Algebra/Basic Algebra/Category - -Algebra/Category + +Algebra/Category Algebra/Basic->Algebra/Category - - + + Algebra/Basic->Algebra/Monoid - - + + Algebra/Geometry - -Algebra/Geometry + +Algebra/Geometry Algebra/Basic->Algebra/Geometry - - + + Algebra/Group/Basic - -Algebra/Group/Basic + +Algebra/Group/Basic Algebra/Basic->Algebra/Group/Basic - - - - - -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/Automorphism - -Algebra/Group/Automorphism + +Algebra/Group/Automorphism Algebra/Group/Basic->Algebra/Group/Automorphism - - + + 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/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/Boolean - -Algebra/Boolean + +Algebra/Boolean Algebra/Orgraph - -Algebra/Orgraph + +Algebra/Orgraph Algebra/Reals - -Algebra/Reals + +Algebra/Reals Algebra/Orgraph->Algebra/Reals - - + + Algebra/Group/Limited - -Algebra/Group/Limited + +Algebra/Group/Limited Algebra/Reals->Algebra/Group/Limited - - + + HITs/Topologization - -HITs/Topologization + +HITs/Topologization Algebra/Reals->HITs/Topologization - - + + Algebra/Ring - -Algebra/Ring + +Algebra/Ring Algebra/Ring->Algebra/Boolean - - + + Algebra/Ring->Algebra/Orgraph - - + + Algebra/Transformational - -Algebra/Transformational + +Algebra/Transformational Algebra/Group/Action - -Algebra/Group/Action + +Algebra/Group/Action Algebra/Group/Action->Algebra/Transformational - - + + Algebra/Group/Alternating - -Algebra/Group/Alternating + +Algebra/Group/Alternating 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/Differential - -Algebra/Group/Differential + +Algebra/Group/Differential Algebra/Group/Subgroup->Algebra/Group/Differential - - + + Algebra/Group/Factor - -Algebra/Group/Factor + +Algebra/Group/Factor Algebra/Group/Subgroup->Algebra/Group/Factor - - + + 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/Factor->Algebra/Ring - - + + Algebra/Group/Factor->Algebra/Group/Alternating - - + + Algebra/Group/Isomorphism - -Algebra/Group/Isomorphism + +Algebra/Group/Isomorphism Algebra/Group/Factor->Algebra/Group/Isomorphism - - + + Algebra/Group/Isomorphism->Algebra/Group/Presentation - - + + Algebra/Group/Symmetric->Algebra/Group/Limited - - + + Algebra/Group/Symmetric->Algebra/Group/Action - - + + Algebra/Group/Symmetric->Algebra/Group/Isomorphism - - + + Algebra/Group/Z - -Algebra/Group/Z + +Algebra/Group/Z Algebra/Group/Symmetric->Algebra/Group/Z - - + + Types/Category - -Types/Category + +Types/Category Types/Coproduct->Structures - - + + Types/Ens - -Types/Ens + +Types/Ens Types/Ens->Algebra/Basic - - + + Types/Setquot - -Types/Setquot + +Types/Setquot Types/Ens->Types/Setquot - - + + HITs/Graph - -HITs/Graph + +HITs/Graph Types/HEq->HITs/Graph - - + + Theorems/Funext - -Theorems/Funext + +Theorems/Funext Types/HEq->Theorems/Funext - - + + - + Modal/Infinitesimal->Modal/Disc - - + + Types/Unit->Structures - - + + HITs/Suspension - -HITs/Suspension + +HITs/Suspension Types/Unit->HITs/Suspension - - + + HITs/Wedge - -HITs/Wedge + +HITs/Wedge Types/Unit->HITs/Wedge - - + + Types/Sigma->Structures - - + + HITs/Coequalizer - -HITs/Coequalizer + +HITs/Coequalizer HITs/Graph->HITs/Coequalizer - - + + HITs/Colimit - -HITs/Colimit + +HITs/Colimit HITs/Graph->HITs/Colimit - - + + HITs/Generalized - -HITs/Generalized + +HITs/Generalized HITs/Graph->HITs/Generalized - - + + HITs/Pushout - -HITs/Pushout + +HITs/Pushout HITs/Graph->HITs/Pushout - - + + HITs/Graph->HITs/Quotient - - + + Types/Product - -Types/Product + +Types/Product - + Theorems/Funext->Types/Product - - + + Types/Integer - -Types/Integer + +Types/Integer HITs/Circle - -HITs/Circle + +HITs/Circle Types/Integer->HITs/Circle - - + + HITs/Circle->Algebra/Group/Z - - + + Theorems/Hopf - -Theorems/Hopf + +Theorems/Hopf HITs/Circle->Theorems/Hopf - - + + HITs/Moebius - -HITs/Moebius + +HITs/Moebius HITs/Circle->HITs/Moebius - - + + HITs/Reals - -HITs/Reals + +HITs/Reals HITs/Circle->HITs/Reals - - + + - + Theorems/Nat->Algebra/Reals - - + + - + Theorems/Nat->Algebra/Group/Finite - - + + - + Theorems/Nat->Algebra/Group/Lemmas - - + + - + Theorems/Nat->Types/Integer - - + + HITs/Int - -HITs/Int + +HITs/Int - + Theorems/Nat->HITs/Int - - + + Types/Precategory - -Types/Precategory + +Types/Precategory Types/Precategory->Types/Category - - + + Types/Product->Structures - - + + - + +HITs/Suspension->Algebra/EilenbergMacLane + + + + + HITs/Suspension->HITs/Circle - - + + HITs/Join - -HITs/Join + +HITs/Join - + HITs/Suspension->HITs/Join - - + + HITs/Coequalizer->HITs/Flattening - - + + HITs/Colimit->HITs/Merely - - + + HITs/Colimit->Types/Nat - - + + HITs/Generalized->HITs/Merely - - + + HITs/Pushout->HITs/Suspension - - + + HITs/Pushout->HITs/Wedge - - + + HITs/Quotient->Algebra/Group/Absolutizer - - + + HITs/Quotient->Algebra/Group/Action - - + + HITs/Quotient->Algebra/Group/Factor - - + + Cubical/Square - -Cubical/Square + +Cubical/Square - + Cubical/Cubes->Cubical/Square - - + + Cubical/Connection - -Cubical/Connection + +Cubical/Connection - + Cubical/Path->Cubical/Connection - - + + - + Cubical/Path->Cubical/Square - - + + - + Cubical/Path->Cubical/V - - + + - + Theorems/Equiv->Types/Ens - - + + - + Theorems/Equiv->HITs/Circle - - + + - + Theorems/Equiv->Types/Precategory - - + + Theorems/Classical - -Theorems/Classical + +Theorems/Classical - + Theorems/Equiv->Theorems/Classical - - + + Theorems/Pullback - -Theorems/Pullback + +Theorems/Pullback - + Theorems/Equiv->Theorems/Pullback - - + + - + Theorems/Fibration->Theorems/Hopf - - + + - + Theorems/Functions->Algebra/Group/Basic - - + + - + Theorems/Functions->Types/Precategory - - + + - + Theorems/Functions->HITs/Reals - - + + - + Theorems/Functions->Modal/Etale - - + + Cubical/Example - -Cubical/Example + +Cubical/Example - + Cubical/V->Cubical/Example - - + + Meta/Basic - -Meta/Basic + +Meta/Basic - + Meta/Basic->Proto - - + + 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 - - + + - + Theorems/Classical->Algebra/Category - - + + - + Theorems/Classical->Algebra/Orgraph - - + +