Merge branch 'master' of https://github.com/cmu-phil/Spectral
This commit is contained in:
Egbert Rijke
commit
4559ee6218
18 changed files with 357 additions and 216 deletions
18
Notes/lessons.md
Normal file
18
Notes/lessons.md
Normal file
|
|
@ -0,0 +1,18 @@
|
|||
In this file I (Floris) will collect some lessons learned from building and working with a HoTT library.
|
||||
Some of these things still need to be changes, some of them are already changed, and some of them are not worth the effort to change.
|
||||
|
||||
- Spheres should be indexed by ℕ, it is not worth the effort to start counting at -1 (pointed spheres are much more useful anyway).
|
||||
- Don't have both susp and psusp. psusp should be the default (otherwise there is a distinction between iterate susp and iterate psusp)
|
||||
- Pointed maps should be special cases of dependent pointed maps. Pointed homotopies (between dependent pointed maps) should be special cases of dependent pointed maps, and pointed homotopies should be related themselves by pointed homotopies.
|
||||
- Type classes don't work well together with bundled structures and coercions in Lean (the instance is_contr_unit will not unify with (is_contr punit).
|
||||
- Overloading doesn't work well in Lean (mostly by degrading error messages)
|
||||
- It is useful to do categorical properties more uniformly. Define a 1-coherent ∞-category, which is a precategory (or category?) where the homs are not assumed to be sets. Examples include
|
||||
+ `Type` (with `→`),
|
||||
+ `A → B` (with `~`),
|
||||
+ `Type*` (with `→*`),
|
||||
+ `A →* B` (with `~*`),
|
||||
+ `A` (with `=`),
|
||||
+ spectrum (with `→ₛ`)
|
||||
+ ...
|
||||
You cannot formulate everything in this, but it would be useful to compose natural transformations (instead of composing functions and manually show naturality).
|
||||
Disadvantage: doesn't work
|
||||
119
README.md
119
README.md
|
|
@ -2,61 +2,100 @@
|
|||
|
||||
Formalization project of the CMU HoTT group towards formalizing the Serre spectral sequence.
|
||||
|
||||
This repository also contains the contents of the MRC group on formalizing homology in Lean.
|
||||
|
||||
#### Participants
|
||||
Jeremy Avigad, Steve Awodey, Ulrik Buchholtz, Floris van Doorn, Clive Newstead, Egbert Rijke, Mike Shulman.
|
||||
|
||||
## Resources
|
||||
- [Mike's blog post](http://homotopytypetheory.org/2013/08/08/spectral-sequences/) at the HoTT blog.
|
||||
- [Mike's blog post](https://golem.ph.utexas.edu/category/2013/08/what_is_a_spectral_sequence.html) at the n-category café.
|
||||
- [Mike's blog posts on ncatlab](https://ncatlab.org/homotopytypetheory/show/spectral+sequences).
|
||||
- The [Licata-Finster article](http://dlicata.web.wesleyan.edu/pubs/lf14em/lf14em.pdf) about Eilenberg-Mac Lane spaces.
|
||||
- We learned about the Serre spectral sequence from [Hatcher's chapter about spectral sequences](https://www.math.cornell.edu/~hatcher/SSAT/SSATpage.html).
|
||||
- Lang's algebra (revised 3rd edition) contains a chapter on general homology theory, with a section on spectral sequences. Thus, we can use this book at least as an outline for the algebraic part of the project.
|
||||
- Mac Lane's Homology contains a lot of homological algebra and a chapter on spectral sequences, including exact couples.
|
||||
|
||||
## Things to do for Lean spectral sequences project
|
||||
## Contents for Lean spectral sequences project
|
||||
|
||||
### Algebra To Do:
|
||||
- [R-modules](http://ncatlab.org/nlab/show/module), [vector spaces](http://ncatlab.org/nlab/show/vector+space),
|
||||
- some basic theory: product, tensor, hom, projective,
|
||||
- categories of algebras, [abelian categories](http://ncatlab.org/nlab/show/abelian+category),
|
||||
- exact sequences, short and long
|
||||
- [snake lemma](http://ncatlab.org/nlab/show/snake+lemma)
|
||||
- [5-lemma](http://ncatlab.org/nlab/show/five+lemma)
|
||||
- [chain complexes](http://ncatlab.org/nlab/show/chain+complex) and [homology](http://ncatlab.org/nlab/show/homology)
|
||||
- [exact couples](http://ncatlab.org/nlab/show/exact+couple), probably just of Z-graded objects, and derived exact couples
|
||||
- spectral sequence of an exact couple
|
||||
- [convergence of spectral sequences](http://ncatlab.org/nlab/show/spectral+sequence#ConvergenceOfSpectralSequences)
|
||||
### Outline
|
||||
|
||||
### Topology To Do:
|
||||
These projects are mostly done
|
||||
|
||||
- Given a sequence of spectra and maps, indexed over `ℤ`, we get an exact couple, indexed over `ℤ × ℤ`.
|
||||
- We can derive an exact couple.
|
||||
- If the exact couple is bounded, we repeat this process to get a convergent spectral sequence.
|
||||
- We construct the Atiyah-Hirzebruch and Serre spectral sequences for cohomology.
|
||||
|
||||
### Future directions
|
||||
- Hurewicz Theorem and Hurewicz theorem modulo a Serre class. There is a proof in Hatcher. Also, [this](http://www.math.uni-frankfurt.de/~johannso/SkriptAll/SkriptTopAlg/SkriptTopCW/homotop12.pdf) might be useful.
|
||||
- Homological Serre spectral sequence.
|
||||
- Interaction between steenrod squares and cup product with spectral sequences
|
||||
- ...
|
||||
|
||||
### Algebra
|
||||
|
||||
#### To do
|
||||
- Constructions: tensor, hom, projective, Tor (at least on groups)
|
||||
- Finite groups, Finitely generated groups, torsion groups
|
||||
- Serre classes
|
||||
- [vector spaces](http://ncatlab.org/nlab/show/vector+space),
|
||||
|
||||
#### In Progress
|
||||
|
||||
|
||||
#### Done
|
||||
- groups, rings, fields, [R-modules](http://ncatlab.org/nlab/show/module), graded R-modules.
|
||||
- Constructions on groups and abelian groups:: subgroup, quotient, product, free groups.
|
||||
- Constructions on ablian groups: direct sum, sequential colimi.
|
||||
- exact sequences, short and long.
|
||||
- [chain complexes](http://ncatlab.org/nlab/show/chain+complex) and [homology](http://ncatlab.org/nlab/show/homology).
|
||||
- [exact couples](http://ncatlab.org/nlab/show/exact+couple) graded over an arbitrary indexing set.
|
||||
- spectral sequence of an exact couple.
|
||||
- [convergence of spectral sequences](http://ncatlab.org/nlab/show/spectral+sequence#ConvergenceOfSpectralSequences).
|
||||
|
||||
### Topology
|
||||
|
||||
#### To do
|
||||
- cofiber sequences
|
||||
+ Hom'ing out gives a fiber sequence: if `A → B → coker f` cofiber
|
||||
sequences, then `X^A → X^B → X^(coker f)` is a fiber sequence.
|
||||
- fiber and cofiber sequences of spectra, stability
|
||||
+ limits are levelwise
|
||||
+ colimits need to be spectrified
|
||||
- long exact sequence from cofiber sequences of spectra
|
||||
+ indexed on ℤ, need to splice together LES's
|
||||
- Cup product on cohomology groups
|
||||
- Parametrized and unreduced homology
|
||||
- Steenrod squares
|
||||
- ...
|
||||
|
||||
#### In Progress
|
||||
- [prespectra](http://ncatlab.org/nlab/show/spectrum+object) and [spectra](http://ncatlab.org/nlab/show/spectrum), indexed over an arbitrary type with a successor
|
||||
+ think about equivariant spectra indexed by representations of `G`
|
||||
- [spectrification](http://ncatlab.org/nlab/show/higher+inductive+type#spectrification)
|
||||
+ adjoint to forgetful
|
||||
+ as sequential colimit, prove induction principle
|
||||
+ connective spectrum: `is_conn n.-2 Eₙ`
|
||||
- Postnikov towers of spectra.
|
||||
+ basic definition already there
|
||||
+ fibers of Postnikov sequence unstably and stably
|
||||
- [parametrized spectra](http://ncatlab.org/nlab/show/parametrized+spectrum), parametrized smash and hom between types and spectra.
|
||||
- Check Eilenberg-Steenrod axioms for reduced homology.
|
||||
|
||||
|
||||
#### Done
|
||||
- Most things in the HoTT Book up to Section 8.9 (see [this file](https://github.com/leanprover/lean/blob/master/hott/book.md))
|
||||
- pointed types, maps, homotopies and equivalences
|
||||
- [Eilenberg-MacLane spaces](http://ncatlab.org/nlab/show/Eilenberg-Mac+Lane+space) and EM-spectrum
|
||||
- fiber sequence
|
||||
+ already have the LES
|
||||
+ need shift isomorphism
|
||||
+ Hom'ing into a fiber sequence gives another fiber sequence.
|
||||
- cofiber sequences
|
||||
+ Hom'ing out gives a fiber sequence: if `A → B → coker f` cofiber
|
||||
sequences, then `X^A → X^B → X^(coker f)` is a fiber sequence.
|
||||
- [prespectra](http://ncatlab.org/nlab/show/spectrum+object) and [spectra](http://ncatlab.org/nlab/show/spectrum), suspension
|
||||
+ try indexing on arbitrary successor structure
|
||||
+ think about equivariant spectra indexed by representations of `G`
|
||||
- [spectrification](http://ncatlab.org/nlab/show/higher+inductive+type#spectrification)
|
||||
+ adjoint to forgetful
|
||||
+ as sequential colimit, prove induction principle (if useful)
|
||||
+ connective spectrum: `is_conn n.-2 Eₙ`
|
||||
- [parametrized spectra](http://ncatlab.org/nlab/show/parametrized+spectrum), parametrized smash and hom between types and spectra
|
||||
- fiber and cofiber sequences of spectra, stability
|
||||
+ limits are levelwise
|
||||
+ colimits need to be spectrified
|
||||
- long exact sequences from (co)fiber sequences of spectra
|
||||
+ indexed on ℤ, need to splice together LES's
|
||||
- Postnikov towers of spectra
|
||||
+ basic definition already there
|
||||
+ fibers of Postnikov sequence unstably and stably
|
||||
- long exact sequence of homotopy groups of spectra, indexed on ℤ
|
||||
- exact couple of a tower of spectra
|
||||
+ need to splice together LES's
|
||||
|
||||
### Already Done:
|
||||
- Most things in the HoTT Book up to Section 8.9 (see [this file](https://github.com/leanprover/lean/blob/master/hott/book.md))
|
||||
- pointed types, maps, homotopies and equivalences
|
||||
- definition of algebraic structures such as groups, rings, fields
|
||||
- some algebra: quotient, product, free groups.
|
||||
- [Eilenberg-MacLane spaces](http://ncatlab.org/nlab/show/Eilenberg-Mac+Lane+space) and EM-spectrum
|
||||
## Contributing
|
||||
- We will try to make sure that this repository compiles with the newest version of Lean 2.
|
||||
- Installation instructions for Lean 2 can be found [here](https://github.com/leanprover/lean2).
|
||||
- Some notes on the Emacs mode can be found [here](https://github.com/leanprover/lean2/blob/master/src/emacs/README.md) (for example if some unicode characters don't show up, or increase the spacing between lines by a lot).
|
||||
- If you contribute, please use rebase instead off merge (e.g. `git pull -r`).
|
||||
|
|
|
|||
34
TODO.txt
34
TODO.txt
|
|
@ -1,34 +0,0 @@
|
|||
- reindex spheres
|
||||
- define pmap in terms of ppi
|
||||
|
||||
- move move_to_lib and pointed to library
|
||||
|
||||
talk with Favonia about:
|
||||
- dependent pointed maps
|
||||
- higher cube filling strategies
|
||||
- HIT equivalences
|
||||
- algebra
|
||||
|
||||
|
||||
/-
|
||||
Adjointness:
|
||||
Σ X ⟶ Y X ∧ Y → Z
|
||||
======= ===========
|
||||
X → Ω Y X → (Y → Z)
|
||||
|
||||
Spectrum: Y : ℕ → Type* with e : Ω Yₙ₊₁ ≃* Yₙ.
|
||||
|
||||
|
||||
HOMOLOGY:
|
||||
Hₙ(X, Y) :≡? ∥ X ∧ Ω² (Y (n+2)) ∥₀ ≃ ∥ X ∧ Y n ∥₀
|
||||
|
||||
Eilenberg Steenrod-axioms:
|
||||
H : ℤ → Type* → AbGroup
|
||||
- functorial in second argument
|
||||
- (optional): respects pointed equivalences and pointed homotopies
|
||||
axioms:
|
||||
- the canonical map
|
||||
-
|
||||
- Given (Xᵢ)ᵢ : I → Type* (satisfying AC?) the canonical functor
|
||||
⊕ hₙ
|
||||
-/
|
||||
|
|
@ -6,7 +6,7 @@ Authors: Floris van Doorn, Egbert Rijke, Favonia
|
|||
Constructions with groups
|
||||
-/
|
||||
|
||||
import .quotient_group .free_commutative_group .product_group
|
||||
import .quotient_group .free_abelian_group .product_group
|
||||
|
||||
open eq is_equiv algebra is_trunc set_quotient relation sigma prod sum list trunc function equiv sigma.ops lift
|
||||
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
--Authors: Robert Rose, Liz Vidaurre
|
||||
|
||||
import .direct_sum .quotient_group ..move_to_lib
|
||||
import .direct_sum ..move_to_lib
|
||||
|
||||
open eq algebra is_trunc set_quotient relation sigma prod sum list trunc function equiv sigma.ops nat
|
||||
|
||||
|
|
|
|||
|
|
@ -1,15 +0,0 @@
|
|||
/- The serre spectral sequence -/
|
||||
|
||||
-- Author: Floris van Doorn
|
||||
|
||||
import .module_exact_couple
|
||||
|
||||
namespace left_module
|
||||
|
||||
/- The Atiyah-Hirzebruch spectral sequence (with local coefficents) -/
|
||||
|
||||
|
||||
|
||||
/- The Serre Spectral Sequence -/
|
||||
|
||||
end left_module
|
||||
|
|
@ -3,10 +3,10 @@ Copyright (c) 2015 Floris van Doorn. All rights reserved.
|
|||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Floris van Doorn, Egbert Rijke
|
||||
|
||||
Constructions with groups
|
||||
Tensor group
|
||||
-/
|
||||
|
||||
import .free_commutative_group
|
||||
import .free_abelian_group
|
||||
|
||||
open eq algebra is_trunc sigma sigma.ops prod trunc function equiv
|
||||
namespace group
|
||||
|
|
@ -1,7 +1,7 @@
|
|||
-- Authors: Floris van Doorn
|
||||
|
||||
import homotopy.EM algebra.category.functor.equivalence types.pointed2 ..pointed_pi ..pointed
|
||||
..move_to_lib
|
||||
..move_to_lib .susp
|
||||
|
||||
open eq equiv is_equiv algebra group nat pointed EM.ops is_trunc trunc susp function is_conn
|
||||
|
||||
|
|
@ -518,33 +518,6 @@ namespace EM
|
|||
equivalence.mk (EM_cfunctor (n+2)) (is_equivalence_EM_cfunctor n)
|
||||
end category
|
||||
|
||||
/- move -/
|
||||
|
||||
open trunc_index
|
||||
definition is_trunc_succ_of_is_trunc_loop (n : ℕ₋₂) (A : Type*) (H : is_trunc (n.+1) (Ω A))
|
||||
(H2 : is_conn 0 A) : is_trunc (n.+2) A :=
|
||||
begin
|
||||
apply is_trunc_succ_of_is_trunc_loop, apply minus_one_le_succ,
|
||||
refine is_conn.elim -1 _ _, exact H
|
||||
end
|
||||
|
||||
lemma is_trunc_of_is_trunc_loopn (m n : ℕ) (A : Type*) (H : is_trunc n (Ω[m] A))
|
||||
(H2 : is_conn m A) : is_trunc (m + n) A :=
|
||||
begin
|
||||
revert A H H2; induction m with m IH: intro A H H2,
|
||||
{ rewrite [nat.zero_add], exact H },
|
||||
rewrite [succ_add],
|
||||
apply is_trunc_succ_of_is_trunc_loop,
|
||||
{ apply IH,
|
||||
{ apply is_trunc_equiv_closed _ !loopn_succ_in },
|
||||
apply is_conn_loop },
|
||||
exact is_conn_of_le _ (zero_le_of_nat (succ m))
|
||||
end
|
||||
|
||||
lemma is_trunc_of_is_set_loopn (m : ℕ) (A : Type*) (H : is_set (Ω[m] A))
|
||||
(H2 : is_conn m A) : is_trunc m A :=
|
||||
is_trunc_of_is_trunc_loopn m 0 A H H2
|
||||
|
||||
definition pequiv_EMadd1_of_loopn_pequiv_EM1 {G : AbGroup} {X : Type*} (n : ℕ) (e : Ω[n] X ≃* EM1 G)
|
||||
[H1 : is_conn n X] : X ≃* EMadd1 G n :=
|
||||
begin
|
||||
|
|
@ -563,6 +536,25 @@ namespace EM
|
|||
abstract (EM1_functor_gcompose φ φ⁻¹ᵍ)⁻¹* ⬝* EM1_functor_phomotopy proof right_inv φ qed ⬝*
|
||||
EM1_functor_gid H end
|
||||
|
||||
definition is_contr_EM1 {G : Group} (H : is_contr G) : is_contr (EM1 G) :=
|
||||
is_contr_of_is_conn_of_is_trunc
|
||||
(is_trunc_succ_succ_of_is_trunc_loop _ _ (is_trunc_equiv_closed _ !loop_EM1) _) !is_conn_EM1
|
||||
|
||||
definition is_contr_EMadd1 (n : ℕ) {G : AbGroup} (H : is_contr G) : is_contr (EMadd1 G n) :=
|
||||
begin
|
||||
induction n with n IH,
|
||||
{ exact is_contr_EM1 H },
|
||||
{ have is_contr (ptrunc (n+2) (psusp (EMadd1 G n))), from _,
|
||||
exact this }
|
||||
end
|
||||
|
||||
definition is_contr_EM (n : ℕ) {G : AbGroup} (H : is_contr G) : is_contr (K G n) :=
|
||||
begin
|
||||
cases n with n,
|
||||
{ exact H },
|
||||
{ exact is_contr_EMadd1 n H }
|
||||
end
|
||||
|
||||
definition EMadd1_pequiv_EMadd1 (n : ℕ) {G H : AbGroup} (φ : G ≃g H) : EMadd1 G n ≃* EMadd1 H n :=
|
||||
pequiv.MK (EMadd1_functor φ n) (EMadd1_functor φ⁻¹ᵍ n)
|
||||
abstract (EMadd1_functor_gcompose φ⁻¹ᵍ φ n)⁻¹* ⬝* EMadd1_functor_phomotopy proof left_inv φ qed n ⬝*
|
||||
|
|
@ -577,4 +569,12 @@ namespace EM
|
|||
{ exact EMadd1_pequiv_EMadd1 n φ }
|
||||
end
|
||||
|
||||
definition ppi_EMadd1 {X : Type*} (Y : X → Type*) (n : ℕ) :
|
||||
(Π*(x : X), EMadd1 (πag[n+2] (Y x)) (n+1)) ≃* EMadd1 (πag[n+2] (Π*(x : X), Y x)) (n+1) :=
|
||||
begin
|
||||
exact sorry
|
||||
end
|
||||
--EM_spectrum (πₛ[s] (spi X Y)) k ≃* spi X (λx, EM_spectrum (πₛ[s] (Y x))) k
|
||||
|
||||
|
||||
end EM
|
||||
|
|
|
|||
|
|
@ -43,7 +43,7 @@ definition ordinary_parametrized_cohomology [reducible] {X : Type*} (G : X → A
|
|||
parametrized_cohomology (λx, EM_spectrum (G x)) n
|
||||
|
||||
definition unreduced_parametrized_cohomology {X : Type} (Y : X → spectrum) (n : ℤ) : AbGroup :=
|
||||
@parametrized_cohomology X₊ (λx, option.cases_on x sunit Y) n
|
||||
@parametrized_cohomology X₊ (add_point_spectrum Y) n
|
||||
|
||||
definition unreduced_ordinary_parametrized_cohomology [reducible] {X : Type} (G : X → AbGroup)
|
||||
(n : ℤ) : AbGroup :=
|
||||
|
|
@ -78,7 +78,6 @@ definition parametrized_cohomology_isomorphism_shomotopy_group_spi {X : Type*} (
|
|||
{n m : ℤ} (p : -m = n) : pH^n[(x : X), Y x] ≃g πₛ[m] (spi X Y) :=
|
||||
sorry
|
||||
|
||||
|
||||
/- functoriality -/
|
||||
|
||||
definition cohomology_functor [constructor] {X X' : Type*} (f : X' →* X) (Y : spectrum)
|
||||
|
|
@ -118,7 +117,7 @@ definition cohomology_isomorphism_right (X : Type*) {Y Y' : spectrum} (e : Πn,
|
|||
: H^n[X, Y] ≃g H^n[X, Y'] :=
|
||||
sorry
|
||||
|
||||
definition parametrized_cohomology_isomorphism_right (X : Type*) {Y Y' : X → spectrum}
|
||||
definition parametrized_cohomology_isomorphism_right {X : Type*} {Y Y' : X → spectrum}
|
||||
(e : Πx n, Y x n ≃* Y' x n) (n : ℤ)
|
||||
: pH^n[(x : X), Y x] ≃g pH^n[(x : X), Y' x] :=
|
||||
sorry
|
||||
|
|
@ -127,9 +126,19 @@ definition ordinary_cohomology_isomorphism_right (X : Type*) {G G' : AbGroup} (e
|
|||
(n : ℤ) : oH^n[X, G] ≃g oH^n[X, G'] :=
|
||||
cohomology_isomorphism_right X (EM_spectrum_pequiv e) n
|
||||
|
||||
definition ordinary_parametrized_cohomology_isomorphism_right (X : Type*) {G G' : X → AbGroup}
|
||||
definition ordinary_parametrized_cohomology_isomorphism_right {X : Type*} {G G' : X → AbGroup}
|
||||
(e : Πx, G x ≃g G' x) (n : ℤ) : opH^n[(x : X), G x] ≃g opH^n[(x : X), G' x] :=
|
||||
parametrized_cohomology_isomorphism_right X (λx, EM_spectrum_pequiv (e x)) n
|
||||
parametrized_cohomology_isomorphism_right (λx, EM_spectrum_pequiv (e x)) n
|
||||
|
||||
definition uopH_isomorphism_opH {X : Type} (G : X → AbGroup) (n : ℤ) :
|
||||
uopH^n[(x : X), G x] ≃g opH^n[(x : X₊), add_point_AbGroup G x] :=
|
||||
parametrized_cohomology_isomorphism_right
|
||||
begin
|
||||
intro x n, induction x with x,
|
||||
{ symmetry, apply EM_spectrum_trivial, },
|
||||
{ reflexivity }
|
||||
end
|
||||
n
|
||||
|
||||
/- suspension axiom -/
|
||||
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
import ..algebra.module_exact_couple .strunc .cohomology
|
||||
import ..algebra.spectral_sequence .strunc .cohomology
|
||||
|
||||
open eq spectrum trunc is_trunc pointed int EM algebra left_module fiber lift equiv is_equiv
|
||||
cohomology group sigma unit
|
||||
cohomology group sigma unit is_conn
|
||||
set_option pp.binder_types true
|
||||
|
||||
/- Eilenberg MacLane spaces are the fibers of the Postnikov system of a type -/
|
||||
|
|
@ -19,7 +19,7 @@ begin
|
|||
end
|
||||
|
||||
section
|
||||
open nat is_conn group
|
||||
open nat group
|
||||
definition pfiber_postnikov_map (A : Type*) (n : ℕ) :
|
||||
pfiber (postnikov_map A n) ≃* EM_type A (n+1) :=
|
||||
begin
|
||||
|
|
@ -76,10 +76,30 @@ definition postnikov_smap [constructor] (X : spectrum) (k : ℤ) :
|
|||
strunc k X →ₛ strunc (k - 1) X :=
|
||||
strunc_elim (str (k - 1) X) (is_strunc_strunc_pred X k)
|
||||
|
||||
/-
|
||||
we could try to prove that postnikov_smap is homotopic to postnikov_map, although the types
|
||||
are different enough, that even stating it will be quite annoying
|
||||
-/
|
||||
|
||||
definition pfiber_postnikov_smap (A : spectrum) (n : ℤ) (k : ℤ) :
|
||||
pfiber (postnikov_smap A n k) ≃* EM_spectrum (πₛ[n] A) k :=
|
||||
sfiber (postnikov_smap A n) k ≃* EM_spectrum (πₛ[n] A) k :=
|
||||
begin
|
||||
exact sorry
|
||||
/- symmetry, apply spectrum_pequiv_of_nat_succ_succ, clear k, intro k,
|
||||
apply EMadd1_pequiv k,
|
||||
{ exact sorry
|
||||
-- refine _ ⬝g shomotopy_group_strunc n A,
|
||||
-- exact chain_complex.LES_isomorphism_of_trivial_cod _ _
|
||||
-- (trivial_homotopy_group_of_is_trunc _ (self_lt_succ n))
|
||||
-- (trivial_homotopy_group_of_is_trunc _ (le_succ _))
|
||||
},
|
||||
{ exact sorry --apply is_conn_fun_trunc_elim, apply is_conn_fun_tr
|
||||
},
|
||||
{ -- have is_trunc (n+1) (ptrunc n.+1 A), from !is_trunc_trunc,
|
||||
-- have is_trunc ((n+1).+1) (ptrunc n A), by do 2 apply is_trunc_succ, apply is_trunc_trunc,
|
||||
-- apply is_trunc_pfiber
|
||||
exact sorry
|
||||
}-/
|
||||
end
|
||||
|
||||
section atiyah_hirzebruch
|
||||
|
|
@ -121,8 +141,8 @@ section atiyah_hirzebruch
|
|||
(λn s, πₛ[n] (sfiber (postnikov_smap (spi X Y) s))) ⟹ᵍ (λn, πₛ[n] (strunc s₀ (spi X Y))) :=
|
||||
converges_to_sequence _ s₀ (λn, n - 1) atiyah_hirzebruch_lb atiyah_hirzebruch_ub
|
||||
|
||||
lemma spi_EM_spectrum (k s : ℤ) :
|
||||
EM_spectrum (πₛ[s] (spi X Y)) k ≃* spi X (λx, EM_spectrum (πₛ[s] (Y x))) k :=
|
||||
lemma spi_EM_spectrum (k n : ℤ) :
|
||||
EM_spectrum (πₛ[n] (spi X Y)) k ≃* spi X (λx, EM_spectrum (πₛ[n] (Y x))) k :=
|
||||
sorry
|
||||
|
||||
definition atiyah_hirzebruch_convergence :
|
||||
|
|
@ -144,6 +164,24 @@ section atiyah_hirzebruch
|
|||
|
||||
end atiyah_hirzebruch
|
||||
|
||||
section unreduced_atiyah_hirzebruch
|
||||
|
||||
definition unreduced_atiyah_hirzebruch_convergence {X : Type} (Y : X → spectrum) (s₀ : ℤ)
|
||||
(H : Πx, is_strunc s₀ (Y x)) :
|
||||
(λn s, uopH^-n[(x : X), πₛ[s] (Y x)]) ⟹ᵍ (λn, upH^-n[(x : X), Y x]) :=
|
||||
converges_to_g_isomorphism
|
||||
(@atiyah_hirzebruch_convergence X₊ (add_point_spectrum Y) s₀ (is_strunc_add_point_spectrum H))
|
||||
begin
|
||||
intro n s, refine _ ⬝g !uopH_isomorphism_opH⁻¹ᵍ,
|
||||
apply ordinary_parametrized_cohomology_isomorphism_right,
|
||||
intro x,
|
||||
apply shomotopy_group_add_point_spectrum
|
||||
end
|
||||
begin
|
||||
intro n, reflexivity
|
||||
end
|
||||
end unreduced_atiyah_hirzebruch
|
||||
|
||||
section serre
|
||||
variables {X : Type} (F : X → Type) (Y : spectrum) (s₀ : ℤ) (H : is_strunc s₀ Y)
|
||||
|
||||
|
|
@ -153,28 +191,28 @@ section serre
|
|||
|
||||
postfix `₊ₒ`:(max+1) := add_point_over
|
||||
|
||||
/- NOTE: we need unreduced cohomology, maybe also define aityah_hirzebruch for unreduced cohomology -/
|
||||
include H
|
||||
definition serre_convergence :
|
||||
(λn s, opH^-n[(x : X₊), H^-s[F₊ₒ x, Y]]) ⟹ᵍ (λn, H^-n[(Σ(x : X), F x)₊, Y]) :=
|
||||
-- definition serre_convergence :
|
||||
-- (λn s, uopH^-n[(x : X), uH^-s[F x, Y]]) ⟹ᵍ (λn, uH^-n[Σ(x : X), F x, Y]) :=
|
||||
proof
|
||||
converges_to_g_isomorphism
|
||||
(atiyah_hirzebruch_convergence (λx, sp_cotensor (F₊ₒ x) Y) s₀
|
||||
(λx, is_strunc_sp_cotensor s₀ (F₊ₒ x) H))
|
||||
begin
|
||||
intro n s,
|
||||
apply ordinary_parametrized_cohomology_isomorphism_right,
|
||||
intro x,
|
||||
exact (cohomology_isomorphism_shomotopy_group_sp_cotensor _ _ idp)⁻¹ᵍ,
|
||||
end
|
||||
begin
|
||||
intro n, exact sorry
|
||||
-- refine parametrized_cohomology_isomorphism_shomotopy_group_spi _ idp ⬝g _,
|
||||
-- refine _ ⬝g (cohomology_isomorphism_shomotopy_group_sp_cotensor _ _ idp)⁻¹ᵍ,
|
||||
-- apply shomotopy_group_isomorphism_of_pequiv, intro k,
|
||||
end
|
||||
qed
|
||||
-- proof
|
||||
-- converges_to_g_isomorphism
|
||||
-- (unreduced_atiyah_hirzebruch_convergence
|
||||
-- (λx, sp_cotensor (F x) Y) s₀
|
||||
-- (λx, is_strunc_sp_cotensor s₀ (F x) H))
|
||||
-- begin
|
||||
-- exact sorry
|
||||
-- -- intro n s,
|
||||
-- -- apply ordinary_parametrized_cohomology_isomorphism_right,
|
||||
-- -- intro x,
|
||||
-- -- exact (cohomology_isomorphism_shomotopy_group_sp_cotensor _ _ idp)⁻¹ᵍ,
|
||||
-- end
|
||||
-- begin
|
||||
-- intro n, exact sorry
|
||||
-- -- refine parametrized_cohomology_isomorphism_shomotopy_group_spi _ idp ⬝g _,
|
||||
-- -- refine _ ⬝g (cohomology_isomorphism_shomotopy_group_sp_cotensor _ _ idp)⁻¹ᵍ,
|
||||
-- -- apply shomotopy_group_isomorphism_of_pequiv, intro k,
|
||||
-- end
|
||||
-- qed
|
||||
end serre
|
||||
|
||||
/- TODO: πₛ[n] (strunc 0 (spi X Y)) ≃g H^n[X, λx, Y x] -/
|
||||
|
|
|
|||
|
|
@ -253,11 +253,34 @@ namespace spectrum
|
|||
-- Equivalences of prespectra
|
||||
------------------------------
|
||||
|
||||
definition spectrum_pequiv_of_pequiv_succ {E F : spectrum} (n : ℤ) (e : E (n + 1) ≃* F (n + 1)) :
|
||||
E n ≃* F n :=
|
||||
equiv_glue E n ⬝e* loop_pequiv_loop e ⬝e* (equiv_glue F n)⁻¹ᵉ*
|
||||
|
||||
definition spectrum_pequiv_of_nat {E F : spectrum} (e : Π(n : ℕ), E n ≃* F n) (n : ℤ) :
|
||||
E n ≃* F n :=
|
||||
begin
|
||||
have Πn, E (n + 1) ≃* F (n + 1) → E n ≃* F n,
|
||||
from λk f, equiv_glue E k ⬝e* loop_pequiv_loop f ⬝e* (equiv_glue F k)⁻¹ᵉ*,
|
||||
induction n with n n,
|
||||
exact e n,
|
||||
induction n with n IH,
|
||||
{ exact spectrum_pequiv_of_pequiv_succ -[1+0] (e 0) },
|
||||
{ exact spectrum_pequiv_of_pequiv_succ -[1+succ n] IH }
|
||||
end
|
||||
|
||||
-- definition spectrum_pequiv_of_nat_add {E F : spectrum} (m : ℕ)
|
||||
-- (e : Π(n : ℕ), E (n + m) ≃* F (n + m)) : Π(n : ℤ), E n ≃* F n :=
|
||||
-- begin
|
||||
-- apply spectrum_pequiv_of_nat,
|
||||
-- refine nat.rec_down _ m e _,
|
||||
-- intro n f m, cases m with m,
|
||||
|
||||
-- end
|
||||
|
||||
definition is_contr_spectrum_of_nat {E : spectrum} (e : Π(n : ℕ), is_contr (E n)) (n : ℤ) :
|
||||
is_contr (E n) :=
|
||||
begin
|
||||
have Πn, is_contr (E (n + 1)) → is_contr (E n),
|
||||
from λn H, @(is_trunc_equiv_closed_rev -2 !equiv_glue) (is_contr_loop_of_is_contr H),
|
||||
induction n with n n,
|
||||
exact e n,
|
||||
induction n with n IH,
|
||||
|
|
@ -338,13 +361,6 @@ namespace spectrum
|
|||
definition psp_sphere : gen_prespectrum +ℕ :=
|
||||
psp_susp bool.pbool
|
||||
|
||||
------------------------------
|
||||
-- Contractible spectrum
|
||||
------------------------------
|
||||
|
||||
definition sunit.{u} [constructor] : spectrum.{u} :=
|
||||
spectrum.MK (λn, plift punit) (λn, pequiv_of_is_contr _ _ _ _)
|
||||
|
||||
/---------------------
|
||||
Homotopy groups
|
||||
---------------------/
|
||||
|
|
@ -751,6 +767,29 @@ spectrify_fun (smash_prespectrum_fun f g)
|
|||
|
||||
/- Cofibers and stability -/
|
||||
|
||||
|
||||
------------------------------
|
||||
-- Contractible spectrum
|
||||
------------------------------
|
||||
|
||||
definition sunit.{u} [constructor] : spectrum.{u} :=
|
||||
spectrum.MK (λn, plift punit) (λn, pequiv_of_is_contr _ _ _ _)
|
||||
|
||||
definition shomotopy_group_sunit.{u} (n : ℤ) : πₛ[n] sunit.{u} ≃g trivial_ab_group_lift.{u} :=
|
||||
have H : 0 <[ℕ] 2, from !zero_lt_succ,
|
||||
isomorphism_of_is_contr (@trivial_homotopy_group_of_is_trunc _ _ _ !is_trunc_lift H)
|
||||
!is_trunc_lift
|
||||
|
||||
open option
|
||||
definition add_point_spectrum [unfold 3] {X : Type} (Y : X → spectrum) : X₊ → spectrum
|
||||
| (some x) := Y x
|
||||
| none := sunit
|
||||
|
||||
definition shomotopy_group_add_point_spectrum {X : Type} (Y : X → spectrum) (n : ℤ) :
|
||||
Π(x : X₊), πₛ[n] (add_point_spectrum Y x) ≃g add_point_AbGroup (λ (x : X), πₛ[n] (Y x)) x
|
||||
| (some x) := by reflexivity
|
||||
| none := shomotopy_group_sunit n
|
||||
|
||||
/- The Eilenberg-MacLane spectrum -/
|
||||
|
||||
definition EM_spectrum /-[constructor]-/ (G : AbGroup) : spectrum :=
|
||||
|
|
@ -760,6 +799,12 @@ spectrify_fun (smash_prespectrum_fun f g)
|
|||
EM_spectrum G n ≃* EM_spectrum H n :=
|
||||
spectrum_pequiv_of_nat (λk, EM_pequiv_EM k e) n
|
||||
|
||||
definition EM_spectrum_trivial.{u} (n : ℤ) :
|
||||
EM_spectrum trivial_ab_group_lift.{u} n ≃* trivial_ab_group_lift.{u} :=
|
||||
pequiv_of_is_contr _ _
|
||||
(is_contr_spectrum_of_nat (λk, is_contr_EM k !is_trunc_lift) n)
|
||||
!is_trunc_lift
|
||||
|
||||
/- Wedge of prespectra -/
|
||||
|
||||
open fwedge
|
||||
|
|
|
|||
|
|
@ -173,6 +173,17 @@ definition strunc_functor [constructor] (k : ℤ) {E F : spectrum} (f : E →ₛ
|
|||
strunc k E →ₛ strunc k F :=
|
||||
strunc_elim (str k F ∘ₛ f) (is_strunc_strunc k F)
|
||||
|
||||
definition is_strunc_sunit (n : ℤ) : is_strunc n sunit :=
|
||||
begin
|
||||
intro k, apply is_trunc_lift, apply is_trunc_unit
|
||||
end
|
||||
|
||||
open option
|
||||
definition is_strunc_add_point_spectrum {X : Type} {Y : X → spectrum} {s₀ : ℤ}
|
||||
(H : Πx, is_strunc s₀ (Y x)) : Π(x : X₊), is_strunc s₀ (add_point_spectrum Y x)
|
||||
| (some x) := H x
|
||||
| none := is_strunc_sunit s₀
|
||||
|
||||
definition is_strunc_EM_spectrum (G : AbGroup)
|
||||
: is_strunc 0 (EM_spectrum G) :=
|
||||
begin
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
import homotopy.susp types.pointed2
|
||||
import homotopy.susp types.pointed2 ..move_to_lib
|
||||
|
||||
open susp eq pointed function is_equiv lift equiv
|
||||
open susp eq pointed function is_equiv lift equiv is_trunc
|
||||
|
||||
namespace susp
|
||||
variables {X X' Y Y' Z : Type*}
|
||||
|
|
@ -90,4 +90,42 @@ namespace susp
|
|||
... ≃* psusp (plift.{u v} A) : by exact psusp_pequiv (pequiv_plift.{u v} A)
|
||||
end
|
||||
|
||||
definition is_contr_susp [instance] (A : Type) [H : is_contr A] : is_contr (susp A) :=
|
||||
begin
|
||||
apply is_contr.mk north,
|
||||
intro x, induction x,
|
||||
reflexivity,
|
||||
exact merid !center,
|
||||
apply eq_pathover_constant_left_id_right, apply square_of_eq,
|
||||
exact whisker_left idp (ap merid !eq_of_is_contr)
|
||||
end
|
||||
|
||||
definition is_contr_psusp [instance] (A : Type) [H : is_contr A] : is_contr (psusp A) :=
|
||||
is_contr_susp A
|
||||
|
||||
definition psusp_pelim2 {X Y : Type*} {f g : ⅀ X →* Y} (p : f ~* g) : ((loop_psusp_pintro X Y) f) ~* ((loop_psusp_pintro X Y) g) :=
|
||||
pwhisker_right (loop_psusp_unit X) (Ω⇒ p)
|
||||
|
||||
variables {A₀₀ A₂₀ A₀₂ A₂₂ : Type*}
|
||||
{f₁₀ : A₀₀ →* A₂₀} {f₁₂ : A₀₂ →* A₂₂}
|
||||
{f₀₁ : A₀₀ →* A₀₂} {f₂₁ : A₂₀ →* A₂₂}
|
||||
|
||||
-- rename: psusp_functor_psquare
|
||||
definition suspend_psquare (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : psquare (⅀→ f₁₀) (⅀→ f₁₂) (⅀→ f₀₁) (⅀→ f₂₁) :=
|
||||
sorry
|
||||
|
||||
definition susp_to_loop_psquare (f₁₀ : A₀₀ →* A₂₀) (f₁₂ : A₀₂ →* A₂₂) (f₀₁ : psusp A₀₀ →* A₀₂) (f₂₁ : psusp A₂₀ →* A₂₂) : (psquare (⅀→ f₁₀) f₁₂ f₀₁ f₂₁) → (psquare f₁₀ (Ω→ f₁₂) ((loop_psusp_pintro A₀₀ A₀₂) f₀₁) ((loop_psusp_pintro A₂₀ A₂₂) f₂₁)) :=
|
||||
begin
|
||||
intro p,
|
||||
refine pvconcat _ (ap1_psquare p),
|
||||
exact loop_psusp_unit_natural f₁₀
|
||||
end
|
||||
|
||||
definition loop_to_susp_square (f₁₀ : A₀₀ →* A₂₀) (f₁₂ : A₀₂ →* A₂₂) (f₀₁ : A₀₀ →* Ω A₀₂) (f₂₁ : A₂₀ →* Ω A₂₂) : (psquare f₁₀ (Ω→ f₁₂) f₀₁ f₂₁) → (psquare (⅀→ f₁₀) f₁₂ ((psusp_pelim A₀₀ A₀₂) f₀₁) ((psusp_pelim A₂₀ A₂₂) f₂₁)) :=
|
||||
begin
|
||||
intro p,
|
||||
refine pvconcat (suspend_psquare p) _,
|
||||
exact psquare_transpose (loop_psusp_counit_natural f₁₂)
|
||||
end
|
||||
|
||||
end susp
|
||||
|
|
|
|||
|
|
@ -1,7 +1,6 @@
|
|||
-- definitions, theorems and attributes which should be moved to files in the HoTT library
|
||||
|
||||
import homotopy.sphere2 homotopy.cofiber homotopy.wedge hit.prop_trunc hit.set_quotient eq2 types.pointed2
|
||||
.homotopy.susp
|
||||
|
||||
open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc pi group
|
||||
is_trunc function sphere unit prod bool
|
||||
|
|
@ -294,9 +293,6 @@ namespace trunc
|
|||
{ apply idp_con }
|
||||
end
|
||||
|
||||
definition is_trunc_of_eq {n m : ℕ₋₂} (p : n = m) {A : Type} (H : is_trunc n A) : is_trunc m A :=
|
||||
transport (λk, is_trunc k A) p H
|
||||
|
||||
definition is_trunc_ptrunc_of_is_trunc [instance] [priority 500] (A : Type*)
|
||||
(n m : ℕ₋₂) [H : is_trunc n A] : is_trunc n (ptrunc m A) :=
|
||||
is_trunc_trunc_of_is_trunc A n m
|
||||
|
|
@ -326,6 +322,38 @@ namespace trunc
|
|||
|
||||
end trunc
|
||||
|
||||
namespace is_trunc
|
||||
|
||||
open trunc_index is_conn
|
||||
|
||||
definition is_trunc_of_eq {n m : ℕ₋₂} (p : n = m) {A : Type} (H : is_trunc n A) : is_trunc m A :=
|
||||
transport (λk, is_trunc k A) p H
|
||||
|
||||
definition is_trunc_succ_succ_of_is_trunc_loop (n : ℕ₋₂) (A : Type*) (H : is_trunc (n.+1) (Ω A))
|
||||
(H2 : is_conn 0 A) : is_trunc (n.+2) A :=
|
||||
begin
|
||||
apply is_trunc_succ_of_is_trunc_loop, apply minus_one_le_succ,
|
||||
refine is_conn.elim -1 _ _, exact H
|
||||
end
|
||||
|
||||
lemma is_trunc_of_is_trunc_loopn (m n : ℕ) (A : Type*) (H : is_trunc n (Ω[m] A))
|
||||
(H2 : is_conn m A) : is_trunc (m + n) A :=
|
||||
begin
|
||||
revert A H H2; induction m with m IH: intro A H H2,
|
||||
{ rewrite [nat.zero_add], exact H },
|
||||
rewrite [succ_add],
|
||||
apply is_trunc_succ_succ_of_is_trunc_loop,
|
||||
{ apply IH,
|
||||
{ apply is_trunc_equiv_closed _ !loopn_succ_in },
|
||||
apply is_conn_loop },
|
||||
exact is_conn_of_le _ (zero_le_of_nat (succ m))
|
||||
end
|
||||
|
||||
lemma is_trunc_of_is_set_loopn (m : ℕ) (A : Type*) (H : is_set (Ω[m] A))
|
||||
(H2 : is_conn m A) : is_trunc m A :=
|
||||
is_trunc_of_is_trunc_loopn m 0 A H H2
|
||||
|
||||
end is_trunc
|
||||
namespace sigma
|
||||
|
||||
-- definition sigma_pathover_equiv_of_is_prop {A : Type} {B : A → Type} {C : Πa, B a → Type}
|
||||
|
|
@ -381,6 +409,14 @@ namespace group
|
|||
reflexivity
|
||||
end
|
||||
|
||||
open option
|
||||
definition add_point_AbGroup [unfold 3] {X : Type} (G : X → AbGroup) : X₊ → AbGroup
|
||||
| (some x) := G x
|
||||
| none := trivial_ab_group_lift
|
||||
|
||||
definition isomorphism_of_is_contr {G H : Group} (hG : is_contr G) (hH : is_contr H) : G ≃g H :=
|
||||
trivial_group_of_is_contr G ⬝g (trivial_group_of_is_contr H)⁻¹ᵍ
|
||||
|
||||
end group open group
|
||||
|
||||
namespace function
|
||||
|
|
@ -419,35 +455,6 @@ namespace is_conn
|
|||
|
||||
end is_conn
|
||||
|
||||
namespace is_trunc
|
||||
|
||||
open trunc_index is_conn
|
||||
|
||||
definition is_trunc_succ_succ_of_is_trunc_loop (n : ℕ₋₂) (A : Type*) (H : is_trunc (n.+1) (Ω A))
|
||||
(H2 : is_conn 0 A) : is_trunc (n.+2) A :=
|
||||
begin
|
||||
apply is_trunc_succ_of_is_trunc_loop, apply minus_one_le_succ,
|
||||
refine is_conn.elim -1 _ _, exact H
|
||||
end
|
||||
lemma is_trunc_of_is_trunc_loopn (m n : ℕ) (A : Type*) (H : is_trunc n (Ω[m] A))
|
||||
(H2 : is_conn m A) : is_trunc (m +[ℕ] n) A :=
|
||||
begin
|
||||
revert A H H2; induction m with m IH: intro A H H2,
|
||||
{ rewrite [nat.zero_add], exact H },
|
||||
rewrite [succ_add],
|
||||
apply is_trunc_succ_succ_of_is_trunc_loop,
|
||||
{ apply IH,
|
||||
{ apply is_trunc_equiv_closed _ !loopn_succ_in },
|
||||
apply is_conn_loop },
|
||||
exact is_conn_of_le _ (zero_le_of_nat (succ m))
|
||||
end
|
||||
|
||||
lemma is_trunc_of_is_set_loopn (m : ℕ) (A : Type*) (H : is_set (Ω[m] A))
|
||||
(H2 : is_conn m A) : is_trunc m A :=
|
||||
is_trunc_of_is_trunc_loopn m 0 A H H2
|
||||
|
||||
end is_trunc
|
||||
|
||||
namespace misc
|
||||
open is_conn
|
||||
|
||||
|
|
@ -801,34 +808,16 @@ begin
|
|||
rewrite trans_refl
|
||||
end
|
||||
|
||||
definition psusp_pelim2 {X Y : Type*} {f g : ⅀ X →* Y} (p : f ~* g) : ((loop_psusp_pintro X Y) f) ~* ((loop_psusp_pintro X Y) g) :=
|
||||
pwhisker_right (loop_psusp_unit X) (Ω⇒ p)
|
||||
|
||||
namespace pointed
|
||||
definition to_homotopy_pt_mk {A B : Type*} {f g : A →* B} (h : f ~ g)
|
||||
(p : h pt ⬝ respect_pt g = respect_pt f) : to_homotopy_pt (phomotopy.mk h p) = p :=
|
||||
to_right_inv !eq_con_inv_equiv_con_eq p
|
||||
|
||||
|
||||
variables {A₀₀ A₂₀ A₀₂ A₂₂ : Type*}
|
||||
{f₁₀ : A₀₀ →* A₂₀} {f₁₂ : A₀₂ →* A₂₂}
|
||||
{f₀₁ : A₀₀ →* A₀₂} {f₂₁ : A₂₀ →* A₂₂}
|
||||
|
||||
definition psquare_transpose (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : psquare f₀₁ f₂₁ f₁₀ f₁₂ := p⁻¹*
|
||||
|
||||
definition suspend_psquare (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : psquare (⅀→ f₁₀) (⅀→ f₁₂) (⅀→ f₀₁) (⅀→ f₂₁) :=
|
||||
sorry
|
||||
|
||||
definition susp_to_loop_psquare (f₁₀ : A₀₀ →* A₂₀) (f₁₂ : A₀₂ →* A₂₂) (f₀₁ : psusp A₀₀ →* A₀₂) (f₂₁ : psusp A₂₀ →* A₂₂) : (psquare (⅀→ f₁₀) f₁₂ f₀₁ f₂₁) → (psquare f₁₀ (Ω→ f₁₂) ((loop_psusp_pintro A₀₀ A₀₂) f₀₁) ((loop_psusp_pintro A₂₀ A₂₂) f₂₁)) :=
|
||||
begin
|
||||
intro p,
|
||||
refine pvconcat _ (ap1_psquare p),
|
||||
exact loop_psusp_unit_natural f₁₀
|
||||
end
|
||||
|
||||
definition loop_to_susp_square (f₁₀ : A₀₀ →* A₂₀) (f₁₂ : A₀₂ →* A₂₂) (f₀₁ : A₀₀ →* Ω A₀₂) (f₂₁ : A₂₀ →* Ω A₂₂) : (psquare f₁₀ (Ω→ f₁₂) f₀₁ f₂₁) → (psquare (⅀→ f₁₀) f₁₂ ((psusp_pelim A₀₀ A₀₂) f₀₁) ((psusp_pelim A₂₀ A₂₂) f₂₁)) :=
|
||||
begin
|
||||
intro p,
|
||||
refine pvconcat (suspend_psquare p) _,
|
||||
exact psquare_transpose (loop_psusp_counit_natural f₁₂)
|
||||
end
|
||||
end pointed
|
||||
|
|
|
|||
|
|
@ -195,6 +195,9 @@ namespace pointed
|
|||
definition is_contr_loop (A : Type*) [is_set A] : is_contr (Ω A) :=
|
||||
is_contr.mk idp (λa, !is_prop.elim)
|
||||
|
||||
definition is_contr_loop_of_is_contr {A : Type*} (H : is_contr A) : is_contr (Ω A) :=
|
||||
is_contr_loop A
|
||||
|
||||
definition is_contr_punit [instance] : is_contr punit :=
|
||||
is_contr_unit
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue