fix universe level for has_choice
This commit is contained in:
Floris van Doorn
parent
eb8601dc93
commit
5c9927ce2d
3 changed files with 41 additions and 35 deletions
52
choice.hlean
52
choice.hlean
|
|
@ -3,26 +3,35 @@ import types.trunc types.sum types.lift types.unit
|
|||
open pi prod sum unit bool trunc is_trunc is_equiv eq equiv lift pointed
|
||||
|
||||
namespace choice
|
||||
universe variables u v
|
||||
|
||||
-- the following brilliant name is from Agda
|
||||
definition unchoose [unfold 4] (n : ℕ₋₂) {X : Type} (A : X → Type) : trunc n (Πx, A x) → Πx, trunc n (A x) :=
|
||||
trunc.elim (λf x, tr (f x))
|
||||
|
||||
definition has_choice.{u} [class] (n : ℕ₋₂) (X : Type.{u}) : Type.{u+1} :=
|
||||
Π(A : X → Type.{u}), is_equiv (unchoose n A)
|
||||
definition has_choice [class] (n : ℕ₋₂) (X : Type.{u}) : Type.{max u (v+1)} :=
|
||||
Π(A : X → Type.{v}), is_equiv (unchoose n A)
|
||||
|
||||
definition choice_equiv.{u} [constructor] {n : ℕ₋₂} {X : Type.{u}} [H : has_choice n X] (A : X → Type.{u})
|
||||
: trunc n (Πx, A x) ≃ (Πx, trunc n (A x)) :=
|
||||
definition choice_equiv [constructor] {n : ℕ₋₂} {X : Type} [H : has_choice.{u v} n X]
|
||||
(A : X → Type) : trunc n (Πx, A x) ≃ (Πx, trunc n (A x)) :=
|
||||
equiv.mk _ (H A)
|
||||
|
||||
definition has_choice_of_succ (X : Type) (H : Πk, has_choice (k.+1) X) (n : ℕ₋₂) : has_choice n X :=
|
||||
definition has_choice_of_succ (X : Type) (H : Πk, has_choice.{_ v} (k.+1) X) (n : ℕ₋₂) :
|
||||
has_choice.{_ v} n X :=
|
||||
begin
|
||||
cases n with n,
|
||||
{ intro A, exact is_equiv_of_is_contr _ _ _ },
|
||||
{ exact H n }
|
||||
end
|
||||
|
||||
definition has_choice_empty [instance] (n : ℕ₋₂) : has_choice n empty :=
|
||||
/- currently we prove it using univalence, which means we cannot apply it to lift. -/
|
||||
definition has_choice_equiv_closed (n : ℕ₋₂) {A B : Type} (f : A ≃ B) (hA : has_choice.{u v} n B)
|
||||
: has_choice.{u v} n A :=
|
||||
begin
|
||||
induction f using rec_on_ua_idp, exact hA
|
||||
end
|
||||
|
||||
definition has_choice_empty [instance] (n : ℕ₋₂) : has_choice.{_ v} n empty :=
|
||||
begin
|
||||
intro A, fapply adjointify,
|
||||
{ intro f, apply tr, intro x, induction x },
|
||||
|
|
@ -30,7 +39,7 @@ begin
|
|||
{ intro g, induction g with g, apply ap tr, apply eq_of_homotopy, intro x, induction x }
|
||||
end
|
||||
|
||||
definition has_choice_unit [instance] : Πn, has_choice n unit :=
|
||||
definition has_choice_unit [instance] : Πn, has_choice.{_ v} n unit :=
|
||||
begin
|
||||
intro n A, fapply adjointify,
|
||||
{ intro f, induction f ⋆ with a, apply tr, intro u, induction u, exact a },
|
||||
|
|
@ -40,8 +49,8 @@ begin
|
|||
intro u, induction u, reflexivity }
|
||||
end
|
||||
|
||||
definition has_choice_sum.{u} [instance] (n : ℕ₋₂) (A B : Type.{u})
|
||||
[has_choice n A] [has_choice n B] : has_choice n (A ⊎ B) :=
|
||||
definition has_choice_sum [instance] (n : ℕ₋₂) (A B : Type.{u})
|
||||
[has_choice.{_ v} n A] [has_choice.{_ v} n B] : has_choice.{_ v} n (A ⊎ B) :=
|
||||
begin
|
||||
intro P, fapply is_equiv_of_equiv_of_homotopy,
|
||||
{ exact calc
|
||||
|
|
@ -54,25 +63,18 @@ begin
|
|||
{ intro f, induction f, apply eq_of_homotopy, intro x, esimp, induction x with a b: reflexivity }
|
||||
end
|
||||
|
||||
/- currently we prove it using univalence, which means we cannot apply it to lift. TODO: change -/
|
||||
definition has_choice_equiv_closed.{u} (n : ℕ₋₂) {A B : Type.{u}} (f : A ≃ B) (hA : has_choice n B)
|
||||
: has_choice n A :=
|
||||
begin
|
||||
induction f using rec_on_ua_idp, assumption
|
||||
end
|
||||
|
||||
definition has_choice_bool [instance] (n : ℕ₋₂) : has_choice n bool :=
|
||||
definition has_choice_bool [instance] (n : ℕ₋₂) : has_choice.{_ v} n bool :=
|
||||
has_choice_equiv_closed n bool_equiv_unit_sum_unit _
|
||||
|
||||
definition has_choice_lift.{u v} [instance] (n : ℕ₋₂) (A : Type) [has_choice n A] :
|
||||
has_choice n (lift.{u v} A) :=
|
||||
definition has_choice_lift.{u'} [instance] (n : ℕ₋₂) (A : Type) [has_choice.{_ v} n A] :
|
||||
has_choice.{_ v} n (lift.{u u'} A) :=
|
||||
sorry --has_choice_equiv_closed n !equiv_lift⁻¹ᵉ _
|
||||
|
||||
definition has_choice_punit [instance] (n : ℕ₋₂) : has_choice n punit := has_choice_unit n
|
||||
definition has_choice_pbool [instance] (n : ℕ₋₂) : has_choice n pbool := has_choice_bool n
|
||||
definition has_choice_plift [instance] (n : ℕ₋₂) (A : Type*) [has_choice n A]
|
||||
: has_choice n (plift A) := has_choice_lift n A
|
||||
definition has_choice_psum [instance] (n : ℕ₋₂) (A B : Type*) [has_choice n A] [has_choice n B]
|
||||
: has_choice n (psum A B) := has_choice_sum n A B
|
||||
definition has_choice_punit [instance] (n : ℕ₋₂) : has_choice.{_ v} n punit := has_choice_unit n
|
||||
definition has_choice_pbool [instance] (n : ℕ₋₂) : has_choice.{_ v} n pbool := has_choice_bool n
|
||||
definition has_choice_plift [instance] (n : ℕ₋₂) (A : Type*) [has_choice.{_ v} n A]
|
||||
: has_choice.{_ v} n (plift A) := has_choice_lift n A
|
||||
definition has_choice_psum [instance] (n : ℕ₋₂) (A B : Type*) [has_choice.{_ v} n A] [has_choice.{_ v} n B]
|
||||
: has_choice.{_ v} n (psum A B) := has_choice_sum n A B
|
||||
|
||||
end choice
|
||||
|
|
|
|||
|
|
@ -133,7 +133,7 @@ definition cohomology_isomorphism {X X' : Type*} (f : X' ≃* X) (Y : spectrum)
|
|||
H^n[X, Y] ≃g H^n[X', Y] :=
|
||||
Group_trunc_pmap_isomorphism f
|
||||
|
||||
notation `H^≃` n `[`:0 e:0 `, ` Y:0 `]`:0 := cohomology_isomorphism e Y n
|
||||
notation `H^≃` n `[`:0 e:0 `, ` Y:0 `]`:0 := cohomology_isomorphism e Y n
|
||||
|
||||
definition cohomology_isomorphism_refl (X : Type*) (Y : spectrum) (n : ℤ) (x : H^n[X,Y]) :
|
||||
H^≃n[pequiv.refl X, Y] x = x :=
|
||||
|
|
@ -149,6 +149,8 @@ definition unreduced_cohomology_isomorphism {X X' : Type} (f : X' ≃ X) (Y : sp
|
|||
uH^n[X, Y] ≃g uH^n[X', Y] :=
|
||||
cohomology_isomorphism (add_point_pequiv f) Y n
|
||||
|
||||
notation `uH^≃` n `[`:0 e:0 `, ` Y:0 `]`:0 := unreduced_cohomology_isomorphism e Y n
|
||||
|
||||
definition unreduced_cohomology_isomorphism_right (X : Type) {Y Y' : spectrum} (e : Πn, Y n ≃* Y' n)
|
||||
(n : ℤ) : uH^n[X, Y] ≃g uH^n[X, Y'] :=
|
||||
cohomology_isomorphism_right X₊ e n
|
||||
|
|
@ -157,6 +159,8 @@ definition unreduced_ordinary_cohomology_isomorphism {X X' : Type} (f : X' ≃ X
|
|||
(n : ℤ) : uoH^n[X, G] ≃g uoH^n[X', G] :=
|
||||
unreduced_cohomology_isomorphism f (EM_spectrum G) n
|
||||
|
||||
notation `uoH^≃` n `[`:0 e:0 `, ` Y:0 `]`:0 := unreduced_ordinary_cohomology_isomorphism e Y n
|
||||
|
||||
definition unreduced_ordinary_cohomology_isomorphism_right (X : Type) {G G' : AbGroup}
|
||||
(e : G ≃g G') (n : ℤ) : uoH^n[X, G] ≃g uoH^n[X, G'] :=
|
||||
unreduced_cohomology_isomorphism_right X (EM_spectrum_pequiv e) n
|
||||
|
|
@ -355,10 +359,10 @@ definition cohomology_punit (Y : spectrum) (n : ℤ) :
|
|||
is_contr (H^n[punit, Y]) :=
|
||||
@is_trunc_trunc_of_is_trunc _ _ _ !is_contr_punit_pmap
|
||||
|
||||
definition cohomology_wedge (X X' : Type*) (Y : spectrum) (n : ℤ) :
|
||||
definition cohomology_wedge.{u} (X X' : Type*) (Y : spectrum.{u}) (n : ℤ) :
|
||||
H^n[wedge X X', Y] ≃g H^n[X, Y] ×ag H^n[X', Y] :=
|
||||
H^≃n[(wedge_pequiv_fwedge X X')⁻¹ᵉ*, Y] ⬝g
|
||||
cohomology_fwedge (has_choice_pbool 0) _ _ _ ⬝g
|
||||
cohomology_fwedge (has_choice_bool 0) _ _ _ ⬝g
|
||||
Group_pi_isomorphism_Group_pi erfl begin intro b, induction b: reflexivity end ⬝g
|
||||
(product_isomorphism_Group_pi H^n[X, Y] H^n[X', Y])⁻¹ᵍ ⬝g
|
||||
proof !isomorphism.refl qed
|
||||
|
|
@ -406,6 +410,10 @@ is_contr_equiv_closed_rev
|
|||
(equiv_of_isomorphism (unreduced_ordinary_cohomology_nonzero (sphere k) G n q))
|
||||
(ordinary_cohomology_sphere_of_neq G p)
|
||||
|
||||
definition unreduced_ordinary_cohomology_sphere_of_neq_nat (G : AbGroup) {n k : ℕ} (p : n ≠ k)
|
||||
(q : n ≠ 0) : is_contr (uoH^n[sphere k, G]) :=
|
||||
unreduced_ordinary_cohomology_sphere_of_neq G (λh, p (of_nat.inj h)) (λh, q (of_nat.inj h))
|
||||
|
||||
theorem is_contr_cohomology_of_is_contr_spectrum (n : ℤ) (X : Type*) (Y : spectrum)
|
||||
(H : is_contr (Y n)) : is_contr (H^n[X, Y]) :=
|
||||
begin
|
||||
|
|
@ -454,7 +462,7 @@ structure cohomology_theory.{u} : Type.{u+1} :=
|
|||
(Hsusp_natural : Π(n : ℤ) {X Y : Type*} (f : X →* Y),
|
||||
Hsusp n X ∘ Hh (succ n) (susp_functor f) ~ Hh n f ∘ Hsusp n Y)
|
||||
(Hexact : Π(n : ℤ) {X Y : Type*} (f : X →* Y), is_exact_g (Hh n (pcod f)) (Hh n f))
|
||||
(Hadditive : Π(n : ℤ) {I : Type.{u}} (X : I → Type*), has_choice 0 I →
|
||||
(Hadditive : Π(n : ℤ) {I : Type.{u}} (X : I → Type*), has_choice.{u u} 0 I →
|
||||
is_equiv (Group_pi_intro (λi, Hh n (pinl i)) : HH n (⋁ X) → Πᵍ i, HH n (X i)))
|
||||
|
||||
structure ordinary_cohomology_theory.{u} extends cohomology_theory.{u} : Type.{u+1} :=
|
||||
|
|
|
|||
|
|
@ -246,15 +246,11 @@ sorry
|
|||
{ reflexivity }
|
||||
end
|
||||
|
||||
|
||||
|
||||
|
||||
open trunc
|
||||
definition trunc_fwedge_pmap_equiv.{u} {n : ℕ₋₂} {I : Type.{u}} (H : has_choice n I)
|
||||
(F : I → pType.{u}) (X : pType.{u}) : trunc n (⋁F →* X) ≃ Πi, trunc n (F i →* X) :=
|
||||
definition trunc_fwedge_pmap_equiv.{u v w} {n : ℕ₋₂} {I : Type.{u}} (H : has_choice n I)
|
||||
(F : I → pType.{v}) (X : pType.{w}) : trunc n (⋁F →* X) ≃ Πi, trunc n (F i →* X) :=
|
||||
trunc_equiv_trunc n (fwedge_pmap_equiv F X) ⬝e choice_equiv (λi, F i →* X)
|
||||
|
||||
|
||||
definition fwedge_functor [constructor] {I : Type} {F F' : I → Type*} (f : Π i, F i →* F' i)
|
||||
: ⋁ F →* ⋁ F' := fwedge_pmap (λ i, pinl i ∘* f i)
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue