michael/Spectral
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

rename ordinary_theory to ordinary_cohomology_theory

Browse source
This commit is contained in:
Floris van Doorn 2017-06-08 11:51:49 -04:00
parent 664d971d4b
commit 5b384882f8
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
homotopy/cohomology.hlean
View file

@ -189,7 +189,7 @@ structure cohomology_theory.{u} : Type.{u+1} :=
(Hadditive : Π(n : ℤ) {I : Type.{u}} (X : I → Type*), has_choice 0 I →
is_equiv (Group_pi_intro (λi, Hh n (pinl i)) : HH n (⋁ X) → Πᵍ i, HH n (X i)))
structure ordinary_theory.{u} extends cohomology_theory.{u} : Type.{u+1} :=
structure ordinary_cohomology_theory.{u} extends cohomology_theory.{u} : Type.{u+1} :=
(Hdimension : Π(n : ℤ), n ≠ 0 → is_contr (HH n (plift pbool)))
attribute cohomology_theory.HH [coercion]
@ -270,7 +270,7 @@ cohomology_theory.mk
-- print has_choice_lift
-- print equiv_lift
-- print has_choice_equiv_closed
definition ordinary_theory_EM [constructor] (G : AbGroup) : ordinary_theory :=
definition ordinary_cohomology_theory_EM [constructor] (G : AbGroup) : ordinary_theory :=
⦃ordinary_theory, cohomology_theory_spectrum (EM_spectrum G), Hdimension := EM_dimension G ⦄
end cohomology