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

Change the definition of graded morphisms

Browse source 
Now we require them to be automorphisms which are equal to \g, g + d(0)
This commit is contained in:
Floris van Doorn 2018-09-26 13:12:24 +02:00
parent db8402e1af
commit 4d3053daff
4 changed files with 207 additions and 157 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

153
algebra/graded.hlean
View file

@ -12,7 +12,7 @@ definition graded [reducible] (str : Type) (I : Type) : Type := I → str
definition graded_module [reducible] (R : Ring) : Type → Type := graded (LeftModule R)
-- TODO: We can (probably) make I a type everywhere
variables {R : Ring} {I : Set} {M M₁ M₂ M₃ : graded_module R I}
variables {R : Ring} {I : AddGroup} {M M₁ M₂ M₃ : graded_module R I}
/-
morphisms between graded modules.
@ -46,17 +46,31 @@ gmd_constant d M₁ M₂
structure graded_hom (M₁ M₂ : graded_module R I) : Type :=
mk' :: (d : I ≃ I)
(deg_eq : Π(i : I), d i = i + d 0)
(fn' : graded_hom_of_deg d M₁ M₂)
definition deg_eq_id (i : I) : erfl i = i + erfl 0 :=
!add_zero⁻¹
definition deg_eq_inv {d : I ≃ I} (pd : Π(i : I), d i = i + d 0) (i : I) : d⁻¹ᵉ i = i + d⁻¹ᵉ 0 :=
inv_eq_of_eq (!pd ⬝ !neg_add_cancel_right)⁻¹ ⬝
ap (λx, i + x) ((to_left_inv d _)⁻¹ ⬝ ap d⁻¹ᵉ (!pd ⬝ add.left_inv (d 0)))
definition deg_eq_con {d₁ d₂ : I ≃ I} (pd₁ : Π(i : I), d₁ i = i + d₁ 0) (pd₂ : Π(i : I), d₂ i = i + d₂ 0)
(i : I) : (d₁ ⬝e d₂) i = i + (d₁ ⬝e d₂) 0 :=
ap d₂ !pd₁ ⬝ !pd₂ ⬝ !add.assoc ⬝ ap (λx, i + x) !pd₂⁻¹
notation M₁ ` →gm ` M₂ := graded_hom M₁ M₂
abbreviation deg [unfold 5] := @graded_hom.d
abbreviation deg_eq [unfold 5] := @graded_hom.deg_eq
postfix ` ↘`:max := graded_hom.fn' -- there is probably a better character for this? Maybe ↷?
definition graded_hom_fn [reducible] [unfold 5] [coercion] (f : M₁ →gm M₂) (i : I) : M₁ i →lm M₂ (deg f i) :=
f ↘ idp
definition graded_hom_fn_out [reducible] [unfold 5] (f : M₁ →gm M₂) (i : I) : M₁ ((deg f)⁻¹ i) →lm M₂ i :=
definition graded_hom_fn_out [reducible] [unfold 5] (f : M₁ →gm M₂) (i : I) : M₁ ((deg f)⁻¹ᵉ i) →lm M₂ i :=
f ↘ (to_right_inv (deg f) i)
infix ` ← `:max := graded_hom_fn_out -- todo: change notation
@ -91,61 +105,65 @@ infix ` ← `:max := graded_hom_fn_out -- todo: change notation
-- P (f ← i m) :=
-- graded_hom_fn_out_rec f H m
definition graded_hom.mk [constructor] (d : I ≃ I)
definition graded_hom.mk [constructor] (d : I ≃ I) (pd : Π(i : I), d i = i + d 0)
(fn : Πi, M₁ i →lm M₂ (d i)) : M₁ →gm M₂ :=
graded_hom.mk' d (λi j p, homomorphism_of_eq (ap M₂ p) ∘lm fn i)
graded_hom.mk' d pd (λi j p, homomorphism_of_eq (ap M₂ p) ∘lm fn i)
definition graded_hom.mk_out [constructor] (d : I ≃ I)
definition graded_hom.mk_out [constructor] (d : I ≃ I) (pd : Π(i : I), d i = i + d 0)
(fn : Πi, M₁ (d⁻¹ i) →lm M₂ i) : M₁ →gm M₂ :=
graded_hom.mk' d (λi j p, fn j ∘lm homomorphism_of_eq (ap M₁ (eq_inv_of_eq p)))
graded_hom.mk' d pd (λi j p, fn j ∘lm homomorphism_of_eq (ap M₁ (eq_inv_of_eq p)))
definition graded_hom.mk_out' [constructor] (d : I ≃ I)
definition graded_hom.mk_out' [constructor] (d : I ≃ I) (pd : Π(i : I), d i = i + d 0)
(fn : Πi, M₁ (d i) →lm M₂ i) : M₁ →gm M₂ :=
graded_hom.mk' d⁻¹ᵉ (λi j p, fn j ∘lm homomorphism_of_eq (ap M₁ (eq_inv_of_eq p)))
graded_hom.mk' d⁻¹ᵉ (deg_eq_inv pd) (λi j p, fn j ∘lm homomorphism_of_eq (ap M₁ (eq_inv_of_eq p)))
definition graded_hom.mk_out_in [constructor] (d₁ : I ≃ I) (d₂ : I ≃ I)
definition graded_hom.mk_out_in [constructor] (d₁ d₂ : I ≃ I)
(pd₁ : Π(i : I), d₁ i = i + d₁ 0) (pd₂ : Π(i : I), d₂ i = i + d₂ 0)
(fn : Πi, M₁ (d₁ i) →lm M₂ (d₂ i)) : M₁ →gm M₂ :=
graded_hom.mk' (d₁⁻¹ᵉ ⬝e d₂) (λi j p, homomorphism_of_eq (ap M₂ p) ∘lm fn (d₁⁻¹ᵉ i) ∘lm
homomorphism_of_eq (ap M₁ (to_right_inv d₁ i)⁻¹))
graded_hom.mk' (d₁⁻¹ᵉ ⬝e d₂) (deg_eq_con (deg_eq_inv pd₁) pd₂)
(λi j p, homomorphism_of_eq (ap M₂ p) ∘lm fn (d₁⁻¹ᵉ i) ∘lm homomorphism_of_eq (ap M₁ (to_right_inv d₁ i)⁻¹))
definition graded_hom_eq_transport (f : M₁ →gm M₂) {i j : I} (p : deg f i = j) (m : M₁ i) :
f ↘ p m = transport M₂ p (f i m) :=
by induction p; reflexivity
definition graded_hom_mk_refl (d : I ≃ I)
(fn : Πi, M₁ i →lm M₂ (d i)) {i : I} (m : M₁ i) : graded_hom.mk d fn i m = fn i m :=
definition graded_hom_mk_refl (d : I ≃ I) (pd : Π(i : I), d i = i + d 0)
(fn : Πi, M₁ i →lm M₂ (d i)) {i : I} (m : M₁ i) : graded_hom.mk d pd fn i m = fn i m :=
by reflexivity
lemma graded_hom_mk_out'_destruct (d : I ≃ I)
lemma graded_hom_mk_out'_destruct (d : I ≃ I) (pd : Π(i : I), d i = i + d 0)
(fn : Πi, M₁ (d i) →lm M₂ i) {i : I} (m : M₁ (d i)) :
graded_hom.mk_out' d fn ↘ (left_inv d i) m = fn i m :=
graded_hom.mk_out' d pd fn ↘ (left_inv d i) m = fn i m :=
begin
unfold [graded_hom.mk_out'],
apply ap (λx, fn i (cast x m)),
refine !ap_compose⁻¹ ⬝ ap02 _ _,
apply is_set.elim --TODO: we can also prove this if I is not a set
apply is_set.elim --note: we can also prove this if I is not a set
end
lemma graded_hom_mk_out_destruct (d : I ≃ I)
lemma graded_hom_mk_out_destruct (d : I ≃ I) (pd : Π(i : I), d i = i + d 0)
(fn : Πi, M₁ (d⁻¹ i) →lm M₂ i) {i : I} (m : M₁ (d⁻¹ i)) :
graded_hom.mk_out d fn ↘ (right_inv d i) m = fn i m :=
graded_hom.mk_out d pd fn ↘ (right_inv d i) m = fn i m :=
begin
rexact graded_hom_mk_out'_destruct d⁻¹ᵉ fn m
rexact graded_hom_mk_out'_destruct d⁻¹ᵉ (deg_eq_inv pd) fn m
end
lemma graded_hom_mk_out_in_destruct (d₁ : I ≃ I) (d₂ : I ≃ I)
(pd₁ : Π(i : I), d₁ i = i + d₁ 0) (pd₂ : Π(i : I), d₂ i = i + d₂ 0)
(fn : Πi, M₁ (d₁ i) →lm M₂ (d₂ i)) {i : I} (m : M₁ (d₁ i)) :
graded_hom.mk_out_in d₁ d₂ fn ↘ (ap d₂ (left_inv d₁ i)) m = fn i m :=
graded_hom.mk_out_in d₁ d₂ pd₁ pd₂ fn ↘ (ap d₂ (left_inv d₁ i)) m = fn i m :=
begin
unfold [graded_hom.mk_out_in],
rewrite [adj d₁, -ap_inv, - +ap_compose, ],
refine cast_fn_cast_square fn _ _ !con.left_inv m
end
variable (I) -- for some reason Lean needs to know what I is when applying this lemma
definition graded_hom_eq_zero {f : M₁ →gm M₂} {i j k : I} {q : deg f i = j} {p : deg f i = k}
(m : M₁ i) (r : f ↘ q m = 0) : f ↘ p m = 0 :=
have f ↘ p m = transport M₂ (q⁻¹ ⬝ p) (f ↘ q m), begin induction p, induction q, reflexivity end,
this ⬝ ap (transport M₂ (q⁻¹ ⬝ p)) r ⬝ tr_eq_of_pathover (apd (λi, 0) (q⁻¹ ⬝ p))
variable {I}
definition graded_hom_change_image {f : M₁ →gm M₂} {i j k : I} {m : M₂ k} (p : deg f i = k)
(q : deg f j = k) (h : image (f ↘ p) m) : image (f ↘ q) m :=
@ -166,7 +184,7 @@ end
variables {f' : M₂ →gm M₃} {f g h : M₁ →gm M₂}
definition graded_hom_compose [constructor] (f' : M₂ →gm M₃) (f : M₁ →gm M₂) : M₁ →gm M₃ :=
graded_hom.mk' (deg f ⬝e deg f') (λi j p, f' ↘ p ∘lm f i)
graded_hom.mk' (deg f ⬝e deg f') (deg_eq_con (deg_eq f) (deg_eq f')) (λi j p, f' ↘ p ∘lm f i)
infixr ` ∘gm `:75 := graded_hom_compose
@ -188,20 +206,28 @@ definition graded_hom_compose_ext [constructor] (f' : M₂ →gm M₃) (f : M₁
(d : Π⦃i j⦄ (p : (deg f ⬝e deg f') i = j), I)
(pf : Π⦃i j⦄ (p : (deg f ⬝e deg f') i = j), deg f i = d p)
(pf' : Π⦃i j⦄ (p : (deg f ⬝e deg f') i = j), deg f' (d p) = j) : M₁ →gm M₃ :=
graded_hom.mk' (deg f ⬝e deg f') (λi j p, (f' ↘ (pf' p)) ∘lm (f ↘ (pf p)))
graded_hom.mk' (deg f ⬝e deg f') (deg_eq_con (deg_eq f) (deg_eq f')) (λi j p, (f' ↘ (pf' p)) ∘lm (f ↘ (pf p)))
variable (M)
definition graded_hom_id [constructor] [refl] : M →gm M :=
graded_hom.mk erfl (λi, lmid)
graded_hom.mk erfl deg_eq_id (λi, lmid)
variable {M}
abbreviation gmid [constructor] := graded_hom_id M
definition graded_hom_reindex [constructor] {J : Set} (e : J ≃ I) (f : M₁ →gm M₂) :
/- reindexing a graded morphism along a group homomorphism.
We could also reindex along an affine transformation, but don't prove that here
-/
definition graded_hom_reindex [constructor] {J : AddGroup} (e : J ≃g I) (f : M₁ →gm M₂) :
(λy, M₁ (e y)) →gm (λy, M₂ (e y)) :=
graded_hom.mk' (e ⬝e deg f ⬝e e⁻¹ᵉ) (λy₁ y₂ p, f ↘ (eq_of_inv_eq p))
graded_hom.mk' (group.equiv_of_isomorphism e ⬝e deg f ⬝e (group.equiv_of_isomorphism e)⁻¹ᵉ)
begin intro i, exact ap e⁻¹ᵍ (deg_eq f (e i)) ⬝ respect_add e⁻¹ᵍ _ _ ⬝
ap011 add (to_left_inv (group.equiv_of_isomorphism e) i)
(ap (e⁻¹ᵍ ∘ deg f) (respect_zero e)⁻¹) end
(λy₁ y₂ p, f ↘ (to_eq_of_inv_eq (group.equiv_of_isomorphism e) p))
definition gm_constant [constructor] (M₁ M₂ : graded_module R I) (d : I ≃ I) : M₁ →gm M₂ :=
graded_hom.mk' d (gmd_constant d M₁ M₂)
definition gm_constant [constructor] (M₁ M₂ : graded_module R I) (d : I ≃ I) (pd : Π(i : I), d i = i + d 0)
(pd : Π(i : I), d i = i + d 0) : M₁ →gm M₂ :=
graded_hom.mk' d pd (gmd_constant d M₁ M₂)
definition is_surjective_graded_hom_compose ⦃x z⦄
(f' : M₂ →gm M₃) (f : M₁ →gm M₂) (p : deg f' (deg f x) = z)
@ -234,28 +260,29 @@ definition isomorphism_of_graded_iso [constructor] (φ : M₁ ≃gm M₂) (i : I
isomorphism.mk (φ i) _
definition isomorphism_of_graded_iso_out [constructor] (φ : M₁ ≃gm M₂) (i : I) :
M₁ ((deg φ)⁻¹ i) ≃lm M₂ i :=
isomorphism_of_graded_iso' φ !to_right_inv
M₁ ((deg φ)⁻¹ᵉ i) ≃lm M₂ i :=
isomorphism_of_graded_iso' φ (to_right_inv (deg φ) i)
protected definition graded_iso.mk [constructor] (d : I ≃ I) (φ : Πi, M₁ i ≃lm M₂ (d i)) :
M₁ ≃gm M₂ :=
protected definition graded_iso.mk [constructor] (d : I ≃ I) (pd : Π(i : I), d i = i + d 0)
(φ : Πi, M₁ i ≃lm M₂ (d i)) : M₁ ≃gm M₂ :=
begin
apply graded_iso.mk' (graded_hom.mk d φ),
apply graded_iso.mk' (graded_hom.mk d pd φ),
intro i j p, induction p,
exact to_is_equiv (equiv_of_isomorphism (φ i)),
end
protected definition graded_iso.mk_out [constructor] (d : I ≃ I) (φ : Πi, M₁ (d⁻¹ i) ≃lm M₂ i) :
protected definition graded_iso.mk_out [constructor] (d : I ≃ I)
(pd : Π(i : I), d i = i + d 0) (φ : Πi, M₁ (d⁻¹ i) ≃lm M₂ i) :
M₁ ≃gm M₂ :=
begin
apply graded_iso.mk' (graded_hom.mk_out d φ),
apply graded_iso.mk' (graded_hom.mk_out d pd φ),
intro i j p, esimp,
exact @is_equiv_compose _ _ _ _ _ !is_equiv_cast _,
end
definition graded_iso_of_eq [constructor] {M₁ M₂ : graded_module R I} (p : M₁ ~ M₂)
: M₁ ≃gm M₂ :=
graded_iso.mk erfl (λi, isomorphism_of_eq (p i))
graded_iso.mk erfl deg_eq_id (λi, isomorphism_of_eq (p i))
-- definition to_gminv [constructor] (φ : M₁ ≃gm M₂) : M₂ →gm M₁ :=
-- graded_hom.mk_out (deg φ)⁻¹ᵉ
@ -266,16 +293,16 @@ graded_iso.mk erfl (λi, isomorphism_of_eq (p i))
variable (M)
definition graded_iso.refl [refl] [constructor] : M ≃gm M :=
graded_iso.mk equiv.rfl (λi, isomorphism.rfl)
graded_iso.mk equiv.rfl deg_eq_id (λi, isomorphism.rfl)
variable {M}
definition graded_iso.rfl [refl] [constructor] : M ≃gm M := graded_iso.refl M
definition graded_iso.symm [symm] [constructor] (φ : M₁ ≃gm M₂) : M₂ ≃gm M₁ :=
graded_iso.mk_out (deg φ)⁻¹ᵉ (λi, (isomorphism_of_graded_iso φ i)⁻¹ˡᵐ)
graded_iso.mk_out (deg φ)⁻¹ᵉ (deg_eq_inv (deg_eq φ)) (λi, (isomorphism_of_graded_iso φ i)⁻¹ˡᵐ)
definition graded_iso.trans [trans] [constructor] (φ : M₁ ≃gm M₂) (ψ : M₂ ≃gm M₃) : M₁ ≃gm M₃ :=
graded_iso.mk (deg φ ⬝e deg ψ)
graded_iso.mk (deg φ ⬝e deg ψ) (deg_eq_con (deg_eq φ) (deg_eq ψ))
(λi, isomorphism_of_graded_iso φ i ⬝lm isomorphism_of_graded_iso ψ (deg φ i))
definition graded_iso.eq_trans [trans] [constructor]
@ -298,7 +325,7 @@ definition fooff {I : Set} (P : I → Type) {i j : I} (M : P i) (N : P j) := uni
notation M ` ==[`:50 P:0 `] `:0 N:50 := fooff P M N
definition graded_homotopy (f g : M₁ →gm M₂) : Type :=
Π⦃i j k⦄ (p : deg f i = j) (q : deg g i = k) (m : M₁ i), f ↘ p m ==[λi, M₂ i] g ↘ q m
Π⦃i j k⦄ (p : deg f i = j) (q : deg g i = k) (m : M₁ i), f ↘ p m ==[λ(i : Set_of_AddGroup I), M₂ i] g ↘ q m
-- mk' :: (hd : deg f ~ deg g)
-- (hfn : Π⦃i j : I⦄ (pf : deg f i = j) (pg : deg g i = j), f ↘ pf ~ g ↘ pg)
@ -311,7 +338,7 @@ infix ` ~gm `:50 := graded_homotopy
-- exact graded_hom_eq_transport f (hd i) m ⬝ tr_eq_of_pathover (hfn i m),
-- end
definition graded_homotopy.mk (h : Πi m, f i m ==[λi, M₂ i] g i m) : f ~gm g :=
definition graded_homotopy.mk (h : Πi m, f i m ==[λ(i : Set_of_AddGroup I), M₂ i] g i m) : f ~gm g :=
begin
intros i j k p q m, induction q, induction p, constructor --exact h i m
end
@ -432,12 +459,12 @@ definition graded_submodule [constructor] (S : Πi, property (M i)) [Π i, is_su
definition graded_submodule_incl [constructor] (S : Πi, property (M i)) [H : Π i, is_submodule (M i) (S i)] :
graded_submodule S →gm M :=
have Π i, is_submodule (M (to_fun erfl i)) (S i), from H,
graded_hom.mk erfl (λi, submodule_incl (S i))
graded_hom.mk erfl deg_eq_id (λi, submodule_incl (S i))
definition graded_hom_lift [constructor] (S : Πi, property (M₂ i)) [Π i, is_submodule (M₂ i) (S i)]
(φ : M₁ →gm M₂)
(h : Π(i : I) (m : M₁ i), φ i m ∈ S (deg φ i)) : M₁ →gm graded_submodule S :=
graded_hom.mk (deg φ) (λi, hom_lift (φ i) (h i))
graded_hom.mk (deg φ) (deg_eq φ) (λi, hom_lift (φ i) (h i))
definition graded_submodule_functor [constructor]
{S : Πi, property (M₁ i)} [Π i, is_submodule (M₁ i) (S i)]
@ -445,7 +472,7 @@ definition graded_submodule_functor [constructor]
(φ : M₁ →gm M₂)
(h : Π(i : I) (m : M₁ i), S i m → T (deg φ i) (φ i m)) :
graded_submodule S →gm graded_submodule T :=
graded_hom.mk (deg φ) (λi, submodule_functor (φ i) (h i))
graded_hom.mk (deg φ) (deg_eq φ) (λi, submodule_functor (φ i) (h i))
definition graded_image (f : M₁ →gm M₂) : graded_module R I :=
λi, image_module (f ← i)
@ -455,7 +482,7 @@ lemma graded_image_lift_lemma (f : M₁ →gm M₂) {i j: I} (p : deg f i = j) (
graded_hom_change_image p (right_inv (deg f) j) (image.mk m idp)
definition graded_image_lift [constructor] (f : M₁ →gm M₂) : M₁ →gm graded_image f :=
graded_hom.mk' (deg f) (λi j p, hom_lift (f ↘ p) (graded_image_lift_lemma f p))
graded_hom.mk' (deg f) (deg_eq f) (λi j p, hom_lift (f ↘ p) (graded_image_lift_lemma f p))
definition graded_image_lift_destruct (f : M₁ →gm M₂) {i : I}
(m : M₁ ((deg f)⁻¹ᵉ i)) : graded_image_lift f ← i m = image_lift (f ← i) m :=
@ -488,18 +515,19 @@ begin
intro m, apply image_graded_image_lift, exact graded_hom_change_image (right_inv (deg f) y) _ m.2
end
definition graded_image_elim_helper {f : M₁ →gm M₂} (g : M₁ →gm M₃)
(h : Π⦃i m⦄, f i m = 0 → g i m = 0) (i : I) : graded_image f (deg f i) →lm M₃ (deg g i) :=
begin
apply image_elim (g ↘ (ap (deg g) (to_left_inv (deg f) i))),
intro m p,
refine graded_hom_eq_zero I m (h _),
exact graded_hom_eq_zero I m p
end
definition graded_image_elim [constructor] {f : M₁ →gm M₂} (g : M₁ →gm M₃)
(h : Π⦃i m⦄, f i m = 0 → g i m = 0) :
graded_image f →gm M₃ :=
begin
apply graded_hom.mk_out_in (deg f) (deg g),
intro i,
apply image_elim (g ↘ (ap (deg g) (to_left_inv (deg f) i))),
exact abstract begin
intro m p,
refine graded_hom_eq_zero m (h _),
exact graded_hom_eq_zero m p end end
end
graded_hom.mk_out_in (deg f) (deg g) (deg_eq f) (deg_eq g) (graded_image_elim_helper g h)
lemma graded_image_elim_destruct {f : M₁ →gm M₂} {g : M₁ →gm M₃}
(h : Π⦃i m⦄, f i m = 0 → g i m = 0) {i j k : I}
@ -517,7 +545,8 @@ begin
exact !adj_inv⁻¹ },
induction r', clear r,
revert k q m, refine eq.rec_to (ap (deg g) (to_left_inv (deg f) i)) _, intro m,
refine graded_hom_mk_out_in_destruct (deg f) (deg g) _ (graded_image_lift f ← (deg f i) m) ⬝ _,
refine graded_hom_mk_out_in_destruct (deg f) (deg g) (deg_eq f) (deg_eq g)
(graded_image_elim_helper g h) (graded_image_lift f ← (deg f i) m) ⬝ _,
refine ap (image_elim _ _) !graded_image_lift_destruct ⬝ _, reflexivity
end
@ -601,13 +630,13 @@ definition graded_quotient (S : Πi, property (M i)) [Π i, is_submodule (M i) (
definition graded_quotient_map [constructor] (S : Πi, property (M i)) [Π i, is_submodule (M i) (S i)] :
M →gm graded_quotient S :=
graded_hom.mk erfl (λi, quotient_map (S i))
graded_hom.mk erfl deg_eq_id (λi, quotient_map (S i))
definition graded_quotient_elim [constructor]
(S : Πi, property (M i)) [Π i, is_submodule (M i) (S i)]
(φ : M →gm M₂)
(H : Πi ⦃m⦄, S i m → φ i m = 0) : graded_quotient S →gm M₂ :=
graded_hom.mk (deg φ) (λi, quotient_elim (φ i) (H i))
graded_hom.mk (deg φ) (deg_eq φ) (λi, quotient_elim (φ i) (H i))
definition graded_homology (g : M₂ →gm M₃) (f : M₁ →gm M₂) : graded_module R I :=
graded_quotient (λ i, homology_quotient_property (g i) (f ← i))
@ -626,7 +655,7 @@ definition graded_homology_intro [constructor] (g : M₂ →gm M₃) (f : M₁
definition graded_homology_elim {g : M₂ →gm M₃} {f : M₁ →gm M₂} (h : M₂ →gm M)
(H : compose_constant h f) : graded_homology g f →gm M :=
graded_hom.mk (deg h) (λi, homology_elim (h i) (H _ _))
graded_hom.mk (deg h) (deg_eq h) (λi, homology_elim (h i) (H _ _))
definition image_of_graded_homology_intro_eq_zero {g : M₂ →gm M₃} {f : M₁ →gm M₂}
⦃i j : I⦄ (p : deg f i = j) (m : graded_kernel g j) (H : graded_homology_intro g f j m = 0) :
@ -651,9 +680,17 @@ definition gmod_ker_in_im (h : is_exact_gmod f f') ⦃i : I⦄ (m : M₂ i) (p :
image (f ← i) m :=
is_exact.ker_in_im (h (right_inv (deg f) i) idp) m p
definition is_exact_gmod_reindex [constructor] {J : Set} (e : J ≃ I) (h : is_exact_gmod f f') :
definition is_exact_gmod_reindex [constructor] {J : AddGroup} (e : J ≃g I) (h : is_exact_gmod f f') :
is_exact_gmod (graded_hom_reindex e f) (graded_hom_reindex e f') :=
λi j k p q, h (eq_of_inv_eq p) (eq_of_inv_eq q)
definition deg_commute {I : AddAbGroup} {M₁ M₂ M₃ M₄ : graded_module R I} (f : M₁ →gm M₂)
(g : M₃ →gm M₄) : hsquare (deg f) (deg f) (deg g) (deg g) :=
begin
intro i,
refine ap (deg g) (deg_eq f i) ⬝ deg_eq g _ ⬝ _ ⬝ (ap (deg f) (deg_eq g i) ⬝ deg_eq f _)⁻¹,
exact !add.assoc ⬝ ap (λx, i + x) !add.comm ⬝ !add.assoc⁻¹
end
end left_module

172
algebra/spectral_sequence.hlean
View file

@ -7,7 +7,7 @@
import .graded ..spectrum.basic .product_group
open algebra is_trunc left_module is_equiv equiv eq function nat sigma set_quotient
open algebra is_trunc left_module is_equiv equiv eq function nat sigma set_quotient group
/- exact couples -/
@ -71,7 +71,7 @@ namespace left_module
end
structure exact_couple (R : Ring) (I : Set) : Type :=
structure exact_couple (R : Ring) (I : AddAbGroup) : Type :=
(D E : graded_module R I)
(i : D →gm D) (j : D →gm E) (k : E →gm D)
(ij : is_exact_gmod i j)
@ -80,17 +80,21 @@ namespace left_module
open exact_couple
definition exact_couple_reindex [constructor] {R : Ring} {I J : Set} (e : J ≃ I)
definition exact_couple_reindex [constructor] {R : Ring} {I J : AddAbGroup}
(e : AddGroup_of_AddAbGroup J ≃g AddGroup_of_AddAbGroup I)
(X : exact_couple R I) : exact_couple R J :=
⦃exact_couple, D := λy, D X (e y), E := λy, E X (e y),
i := graded_hom_reindex e (i X), j := graded_hom_reindex e (j X),
k := graded_hom_reindex e (k X), ij := is_exact_gmod_reindex e (ij X),
jk := is_exact_gmod_reindex e (jk X), ki := is_exact_gmod_reindex e (ki X)⦄
i := graded_hom_reindex e (i X),
j := graded_hom_reindex e (j X),
k := graded_hom_reindex e (k X),
ij := is_exact_gmod_reindex e (ij X),
jk := is_exact_gmod_reindex e (jk X),
ki := is_exact_gmod_reindex e (ki X)⦄
namespace derived_couple
section
parameters {R : Ring} {I : Set} (X : exact_couple R I)
parameters {R : Ring} {I : AddAbGroup} (X : exact_couple R I)
local abbreviation D := D X
local abbreviation E := E X
local abbreviation i := i X
@ -279,68 +283,61 @@ namespace left_module
open derived_couple
definition derived_couple [constructor] {R : Ring} {I : Set}
definition derived_couple [constructor] {R : Ring} {I : AddAbGroup}
(X : exact_couple R I) : exact_couple R I :=
⦃exact_couple, D := D' X, E := E' X, i := i' X, j := j' X, k := k' X,
ij := i'j' X, jk := j'k' X, ki := k'i' X⦄
/- if an exact couple is bounded, we can prove the convergence theorem for it -/
structure is_bounded {R : Ring} {I : Set} (X : exact_couple R I) : Type :=
structure is_bounded {R : Ring} {I : AddAbGroup} (X : exact_couple R I) : Type :=
mk' :: (B B' : I → ℕ)
(Dub : Π⦃x y⦄ ⦃s : ℕ⦄, (deg (i X))^[s] x = y → B x ≤ s → is_contr (D X y))
(Dlb : Π⦃x y z⦄ ⦃s : ℕ⦄ (p : deg (i X) x = y), (deg (i X))^[s] y = z → B' z ≤ s → is_surjective (i X ↘ p))
(Elb : Π⦃x y⦄ ⦃s : ℕ⦄, (deg (i X))⁻¹ᵉ^[s] x = y → B x ≤ s → is_contr (E X y))
(deg_ik_commute : hsquare (deg (k X)) (deg (k X)) (deg (i X)) (deg (i X)))
(deg_ij_commute : hsquare (deg (j X)) (deg (j X)) (deg (i X)) (deg (i X)))
/- Note: Elb proves Dlb for some bound B', but we want tight control over when B' = 0 -/
protected definition is_bounded.mk [constructor] {R : Ring} {I : Set} {X : exact_couple R I}
protected definition is_bounded.mk [constructor] {R : Ring} {I : AddAbGroup} {X : exact_couple R I}
(B B' B'' : I → ℕ)
(Dub : Π⦃x : I⦄ ⦃s : ℕ⦄, B x ≤ s → is_contr (D X ((deg (i X))^[s] x)))
(Dlb : Π⦃x : I⦄ ⦃s : ℕ⦄, B' x ≤ s → is_surjective (i X (((deg (i X))⁻¹ᵉ^[s + 1] x))))
(Elb : Π⦃x : I⦄ ⦃s : ℕ⦄, B'' x ≤ s → is_contr (E X ((deg (i X))⁻¹ᵉ^[s] x)))
(deg_ik_commute : hsquare (deg (k X)) (deg (k X)) (deg (i X)) (deg (i X)))
(deg_ij_commute : hsquare (deg (j X)) (deg (j X)) (deg (i X)) (deg (i X))) : is_bounded X :=
(Elb : Π⦃x : I⦄ ⦃s : ℕ⦄, B'' x ≤ s → is_contr (E X ((deg (i X))⁻¹ᵉ^[s] x))) : is_bounded X :=
begin
apply is_bounded.mk' (λx, max (B x) (B'' x)) B',
{ intro x y s p h, induction p, exact Dub (le.trans !le_max_left h) },
{ exact abstract begin intro x y z s p q h, induction p, induction q,
refine transport (λx, is_surjective (i X x)) _ (Dlb h),
rewrite [-iterate_succ], apply iterate_left_inv end end },
{ intro x y s p h, induction p, exact Elb (le.trans !le_max_right h) },
{ assumption },
{ assumption }
{ intro x y s p h, induction p, exact Elb (le.trans !le_max_right h) }
end
open is_bounded
definition is_bounded_reindex [constructor] {R : Ring} {I J : Set} (e : J ≃ I)
definition is_bounded_reindex [constructor] {R : Ring} {I J : AddAbGroup}
(e : AddGroup_of_AddAbGroup J ≃g AddGroup_of_AddAbGroup I)
{X : exact_couple R I} (HH : is_bounded X) : is_bounded (exact_couple_reindex e X) :=
begin
apply is_bounded.mk' (B HH ∘ e) (B' HH ∘ e),
{ intros x y s p h, refine Dub HH _ h,
refine (iterate_hsquare e _ s x)⁻¹ ⬝ ap e p, intro x, exact to_right_inv e _ },
refine (iterate_hsquare e _ s x)⁻¹ ⬝ ap e p, intro x,
exact to_right_inv (group.equiv_of_isomorphism e) _ },
{ intros x y z s p q h, refine Dlb HH _ _ h,
refine (iterate_hsquare e _ s y)⁻¹ ⬝ ap e q, intro x, exact to_right_inv e _ },
refine (iterate_hsquare e _ s y)⁻¹ ⬝ ap e q, intro x,
exact to_right_inv (group.equiv_of_isomorphism e) _ },
{ intro x y s p h, refine Elb HH _ h,
refine (iterate_hsquare e _ s x)⁻¹ ⬝ ap e p, intro x, exact to_right_inv e _ },
{ intro y, exact ap e⁻¹ᵉ (ap (deg (i X)) (to_right_inv e _) ⬝
deg_ik_commute HH (e y) ⬝ ap (deg (k X)) (to_right_inv e _)⁻¹) },
{ intro y, exact ap e⁻¹ᵉ (ap (deg (i X)) (to_right_inv e _) ⬝
deg_ij_commute HH (e y) ⬝ ap (deg (j X)) (to_right_inv e _)⁻¹) }
refine (iterate_hsquare e _ s x)⁻¹ ⬝ ap e p, intro x,
exact to_right_inv (group.equiv_of_isomorphism e) _ },
end
namespace convergence_theorem
section
parameters {R : Ring} {I : Set} (X : exact_couple R I) (HH : is_bounded X)
parameters {R : Ring} {I : AddAbGroup} (X : exact_couple R I) (HH : is_bounded X)
local abbreviation B := B HH
local abbreviation B' := B' HH
local abbreviation Dub := Dub HH
local abbreviation Dlb := Dlb HH
local abbreviation Elb := Elb HH
local abbreviation deg_ik_commute := deg_ik_commute HH
local abbreviation deg_ij_commute := deg_ij_commute HH
/- We start counting pages at 0, which corresponds to what is usually called the second page -/
definition page (r : ℕ) : exact_couple R I :=
@ -415,11 +412,11 @@ namespace left_module
definition deg_iterate_ik_commute (n : ℕ) :
hsquare (deg (k X)) (deg (k X)) ((deg (i X))^[n]) ((deg (i X))^[n]) :=
iterate_commute n deg_ik_commute
iterate_commute n (deg_commute (k X) (i X))
definition deg_iterate_ij_commute (n : ℕ) :
hsquare (deg (j X)) (deg (j X)) ((deg (i X))⁻¹ᵉ^[n]) ((deg (i X))⁻¹ᵉ^[n]) :=
iterate_commute n (hvinverse deg_ij_commute)
iterate_commute n (deg_commute (j X) (i X))⁻¹ʰᵗʸᵛ
definition B2 (x : I) : ℕ := max (B (deg (k X) x)) (B ((deg (j X))⁻¹ x))
definition Eub ⦃x y : I⦄ ⦃s : ℕ⦄ (p : (deg (i X))^[s] x = y) (h : B2 x ≤ s) :
@ -427,8 +424,8 @@ namespace left_module
begin
induction p,
refine @(is_contr_middle_of_is_exact (exact_couple.jk X (right_inv (deg (j X)) _) idp)) _ _ _,
exact Dub (iterate_commute s (hhinverse deg_ij_commute) x) (le.trans !le_max_right h),
exact Dub !deg_iterate_ik_commute (le.trans !le_max_left h)
exact Dub (iterate_commute s (deg_commute (j X) (i X))⁻¹ʰᵗʸʰ x) (le.trans !le_max_right h),
exact Dub (deg_iterate_ik_commute s x) (le.trans !le_max_left h)
end
definition B3 (x : I) : ℕ :=
@ -549,7 +546,7 @@ namespace left_module
refine short_exact_mod_isomorphism _ _ _ (short_exact_mod_page_r n),
{ exact Einfstable !rb2 idp },
{ exact Dinfstable !rb3 !deg_k },
{ exact Dinfstable !rb4 (!deg_i ⬝ ap (deg (i X)) !deg_k ⬝ !deg_ik_commute) }
{ exact Dinfstable !rb4 (!deg_i ⬝ ap (deg (i X)) !deg_k ⬝ deg_commute (k X) (i X) _) }
end
definition Dinfdiag0 (bound_zero : B' (deg (k X) x) = 0) : Dinfdiag 0 ≃lm D X (deg (k X) x) :=
@ -580,68 +577,76 @@ namespace left_module
open int group prod convergence_theorem prod.ops
definition Z2 [constructor] : Set := gℤ ×g gℤ
definition Z2 [constructor] : AddAbGroup := agℤ ×ag agℤ
-- set_option pp.coercions true
-- set_option pp.binder_types true
-- todo: move
definition AddAbGroup.struct2 [instance] (G : AddAbGroup) :
add_ab_group (algebra._trans_of_Group_of_AbGroup_2 G) :=
AddAbGroup.struct G
/- TODO: redefine/generalize converges_to so that it supports the usual indexing on ℤ × ℤ -/
structure converges_to.{u v w} {R : Ring} (E' : gℤ → gℤ → LeftModule.{u v} R)
(Dinf : gℤ → LeftModule.{u w} R) : Type.{max u (v+1) (w+1)} :=
structure converges_to.{u v w} {R : Ring} (E' : agℤ → agℤ → LeftModule.{u v} R)
(Dinf : agℤ → LeftModule.{u w} R) : Type.{max u (v+1) (w+1)} :=
(X : exact_couple.{u 0 w v} R Z2)
(HH : is_bounded X)
(s₀ : gℤ → gℤ)
(HB : Π(n : gℤ), is_bounded.B' HH (deg (k X) (n, s₀ n)) = 0)
(s₀ : agℤ → agℤ)
(HB : Π(n : agℤ), is_bounded.B' HH (deg (k X) (n, s₀ n)) = 0)
(e : Π(x : Z2), exact_couple.E X x ≃lm E' x.1 x.2)
(f : Π(n : gℤ), exact_couple.D X (deg (k X) (n, s₀ n)) ≃lm Dinf n)
(deg_d1 : ℕ → gℤ) (deg_d2 : ℕ → gℤ)
(deg_d_eq : Π(r : ℕ) (n s : gℤ), deg (d (page X r)) (n, s) = (n + deg_d1 r, s + deg_d2 r))
(f : Π(n : agℤ), exact_couple.D X (deg (k X) (n, s₀ n)) ≃lm Dinf n)
(deg_d1 : ℕ → agℤ) (deg_d2 : ℕ → agℤ)
(deg_d_eq : Π(r : ℕ) (n s : agℤ), deg (d (page X r)) (n, s) = (n, s) + (deg_d1 r, deg_d2 r))
structure converging_spectral_sequence.{u v w} {R : Ring} (E' : gℤ → gℤ → LeftModule.{u v} R)
(Dinf : gℤ → LeftModule.{u w} R) : Type.{max u (v+1) (w+1)} :=
structure converging_spectral_sequence.{u v w} {R : Ring} (E' : agℤ → agℤ → LeftModule.{u v} R)
(Dinf : agℤ → LeftModule.{u w} R) : Type.{max u (v+1) (w+1)} :=
(E : ℕ → graded_module.{u 0 v} R Z2)
(d : Π(n : ℕ), E n →gm E n)
(α : Π(n : ℕ) (x : Z2), E (n+1) x ≃lm graded_homology (d n) (d n) x)
(e : Π(n : ℕ) (x : Z2), E 0 x ≃lm E' x.1 x.2)
(s₀ : Z2 → ℕ)
(f : Π{n : ℕ} {x : Z2} (h : s₀ x ≤ n), E (s₀ x) x ≃lm E n x)
(HDinf : Π(n : gℤ), is_built_from (Dinf n) (λ(k : ℕ), (λx, E (s₀ x) x) (k, n - k)))
(HDinf : Π(n : agℤ), is_built_from (Dinf n) (λ(k : ℕ), (λx, E (s₀ x) x) (k, n - k)))
infix ` ⟹ `:25 := converges_to
definition converges_to_g [reducible] (E' : gℤ → gℤ → AbGroup) (Dinf : gℤ → AbGroup) : Type :=
definition converges_to_g [reducible] (E' : agℤ → agℤ → AbGroup) (Dinf : agℤ → AbGroup) : Type :=
(λn s, LeftModule_int_of_AbGroup (E' n s)) ⟹ (λn, LeftModule_int_of_AbGroup (Dinf n))
infix ` ⟹ᵍ `:25 := converges_to_g
section
open converges_to
parameters {R : Ring} {E' : gℤ → gℤ → LeftModule R} {Dinf : gℤ → LeftModule R} (c : E' ⟹ Dinf)
parameters {R : Ring} {E' : agℤ → agℤ → LeftModule R} {Dinf : agℤ → LeftModule R} (c : E' ⟹ Dinf)
local abbreviation X := X c
local abbreviation i := i X
local abbreviation HH := HH c
local abbreviation s₀ := s₀ c
local abbreviation Dinfdiag (n : gℤ) (k : ℕ) := Dinfdiag HH (n, s₀ n) k
local abbreviation Einfdiag (n : gℤ) (k : ℕ) := Einfdiag HH (n, s₀ n) k
local abbreviation Dinfdiag (n : agℤ) (k : ℕ) := Dinfdiag HH (n, s₀ n) k
local abbreviation Einfdiag (n : agℤ) (k : ℕ) := Einfdiag HH (n, s₀ n) k
definition deg_d_inv_eq (r : ℕ) (n s : gℤ) :
definition deg_d_inv_eq (r : ℕ) (n s : agℤ) :
(deg (d (page X r)))⁻¹ᵉ (n, s) = (n - deg_d1 c r, s - deg_d2 c r) :=
inv_eq_of_eq (!deg_d_eq ⬝ prod_eq !sub_add_cancel !sub_add_cancel)⁻¹
definition converges_to_isomorphism {E'' : gℤ → gℤ → LeftModule R} {Dinf' : graded_module R gℤ}
definition converges_to_isomorphism {E'' : agℤ → agℤ → LeftModule R} {Dinf' : graded_module R agℤ}
(e' : Πn s, E' n s ≃lm E'' n s) (f' : Πn, Dinf n ≃lm Dinf' n) : E'' ⟹ Dinf' :=
converges_to.mk X HH s₀ (HB c)
begin intro x, induction x with n s, exact e c (n, s) ⬝lm e' n s end
(λn, f c n ⬝lm f' n)
(deg_d1 c) (deg_d2 c) (λr n s, deg_d_eq c r n s)
/- definition converges_to_reindex {E'' : gℤ → gℤ → LeftModule R} {Dinf' : graded_module R gℤ}
(i : gℤ ×g gℤ ≃ gℤ × gℤ) (e' : Πp q, E' p q ≃lm E'' (i (p, q)).1 (i (p, q)).2)
(i2 : gℤ ≃ gℤ) (f' : Πn, Dinf n ≃lm Dinf' (i2 n)) :
/- definition converges_to_reindex {E'' : agℤ → agℤ → LeftModule R} {Dinf' : graded_module R agℤ}
(i : agℤ ×g agℤ ≃ agℤ × agℤ) (e' : Πp q, E' p q ≃lm E'' (i (p, q)).1 (i (p, q)).2)
(i2 : agℤ ≃ agℤ) (f' : Πn, Dinf n ≃lm Dinf' (i2 n)) :
(λp q, E'' p q) ⟹ λn, Dinf' n :=
converges_to.mk (exact_couple_reindex i X) (is_bounded_reindex i HH) s₀
sorry --(λn, ap (B' HH) (to_right_inv i _ ⬝ begin end) ⬝ HB c n)
sorry --begin intro x, induction x with p q, exact e c (p, q) ⬝lm e' p q end
sorry-/
/- definition converges_to_reindex_neg {E'' : gℤ → gℤ → LeftModule R} {Dinf' : graded_module R gℤ}
/- definition converges_to_reindex_neg {E'' : agℤ → agℤ → LeftModule R} {Dinf' : graded_module R agℤ}
(e' : Πp q, E' p q ≃lm E'' (-p) (-q))
(f' : Πn, Dinf n ≃lm Dinf' (-n)) :
(λp q, E'' p q) ⟹ λn, Dinf' n :=
@ -655,8 +660,8 @@ namespace left_module
is_built_from_isomorphism_left (f c n) (is_built_from_infpage HH (n, s₀ n) (HB c n))
/- TODO: reprove this using is_built_of -/
theorem is_contr_converges_to_precise (n : gℤ)
(H : Π(n : gℤ) (l : ℕ), is_contr (E' ((deg i)^[l] (n, s₀ n)).1 ((deg i)^[l] (n, s₀ n)).2)) :
theorem is_contr_converges_to_precise (n : agℤ)
(H : Π(n : agℤ) (l : ℕ), is_contr (E' ((deg i)^[l] (n, s₀ n)).1 ((deg i)^[l] (n, s₀ n)).2)) :
is_contr (Dinf n) :=
begin
assert H2 : Π(l : ℕ), is_contr (Einfdiag n l),
@ -673,30 +678,30 @@ namespace left_module
exact equiv_of_isomorphism (Dinfdiag0 HH (n, s₀ n) (HB c n) ⬝lm f c n)
end
theorem is_contr_converges_to (n : gℤ) (H : Π(n s : gℤ), is_contr (E' n s)) : is_contr (Dinf n) :=
theorem is_contr_converges_to (n : agℤ) (H : Π(n s : agℤ), is_contr (E' n s)) : is_contr (Dinf n) :=
is_contr_converges_to_precise n (λn s, !H)
definition E_isomorphism {r₁ r₂ : ℕ} {n s : gℤ} (H : r₁ ≤ r₂)
definition E_isomorphism {r₁ r₂ : ℕ} {n s : agℤ} (H : r₁ ≤ r₂)
(H1 : Π⦃r⦄, r₁ ≤ r → r < r₂ → is_contr (E X (n - deg_d1 c r, s - deg_d2 c r)))
(H2 : Π⦃r⦄, r₁ ≤ r → r < r₂ → is_contr (E X (n + deg_d1 c r, s + deg_d2 c r))) :
E (page X r₂) (n, s) ≃lm E (page X r₁) (n, s) :=
E_isomorphism' X H (λr Hr₁ Hr₂, transport (is_contr ∘ E X) (deg_d_inv_eq r n s)⁻¹ᵖ (H1 Hr₁ Hr₂))
(λr Hr₁ Hr₂, transport (is_contr ∘ E X) (deg_d_eq c r n s)⁻¹ᵖ (H2 Hr₁ Hr₂))
definition E_isomorphism0 {r : ℕ} {n s : gℤ}
definition E_isomorphism0 {r : ℕ} {n s : agℤ}
(H1 : Πr, is_contr (E X (n - deg_d1 c r, s - deg_d2 c r)))
(H2 : Πr, is_contr (E X (n + deg_d1 c r, s + deg_d2 c r))) :
E (page X r) (n, s) ≃lm E' n s :=
E_isomorphism (zero_le r) _ _ ⬝lm e c (n, s)
definition Einf_isomorphism (r₁ : ℕ) {n s : gℤ}
definition Einf_isomorphism (r₁ : ℕ) {n s : agℤ}
(H1 : Π⦃r⦄, r₁ ≤ r → is_contr (E X (n - deg_d1 c r, s - deg_d2 c r)))
(H2 : Π⦃r⦄, r₁ ≤ r → is_contr (E X (n + deg_d1 c r, s + deg_d2 c r))) :
Einf HH (n, s) ≃lm E (page X r₁) (n, s) :=
Einf_isomorphism' HH r₁ (λr Hr₁, transport (is_contr ∘ E X) (deg_d_inv_eq r n s)⁻¹ᵖ (H1 Hr₁))
(λr Hr₁, transport (is_contr ∘ E X) (deg_d_eq c r n s)⁻¹ᵖ (H2 Hr₁))
definition Einf_isomorphism0 {n s : gℤ}
definition Einf_isomorphism0 {n s : agℤ}
(H1 : Π⦃r⦄, is_contr (E X (n - deg_d1 c r, s - deg_d2 c r)))
(H2 : Π⦃r⦄, is_contr (E X (n + deg_d1 c r, s + deg_d2 c r))) :
Einf HH (n, s) ≃lm E' n s :=
@ -704,8 +709,8 @@ namespace left_module
end
variables {E' : gℤ → gℤ → AbGroup} {Dinf : gℤ → AbGroup} (c : E' ⟹ᵍ Dinf)
definition converges_to_g_isomorphism {E'' : gℤ → gℤ → AbGroup} {Dinf' : gℤ → AbGroup}
variables {E' : agℤ → agℤ → AbGroup} {Dinf : agℤ → AbGroup} (c : E' ⟹ᵍ Dinf)
definition converges_to_g_isomorphism {E'' : agℤ → agℤ → AbGroup} {Dinf' : agℤ → AbGroup}
(e' : Πn s, E' n s ≃g E'' n s) (f' : Πn, Dinf n ≃g Dinf' n) : E'' ⟹ᵍ Dinf' :=
converges_to_isomorphism c (λn s, lm_iso_int.mk (e' n s)) (λn, lm_iso_int.mk (f' n))
@ -768,7 +773,6 @@ namespace spectrum
parameters {A : ℤ → spectrum} (f : Π(s : ℤ), A s →ₛ A (s - 1))
-- protected definition I [constructor] : Set := gℤ ×g gℤ
local abbreviation I [constructor] := Z2
definition D_sequence : graded_module rℤ I :=
@ -778,16 +782,18 @@ namespace spectrum
λv, LeftModule_int_of_AbGroup (πₛ[v.1] (sfiber (f (v.2))))
include f
definition i_sequence : D_sequence →gm D_sequence :=
begin
fapply graded_hom.mk, exact (prod_equiv_prod erfl (add_right_action (- 1))),
fapply graded_hom.mk, exact (prod_equiv_prod erfl (add_right_action (- (1 : ℤ)))),
{ intro i, exact pair_eq !add_zero⁻¹ idp },
intro v,
apply lm_hom_int.mk, esimp,
exact πₛ→[v.1] (f v.2)
rexact πₛ→[v.1] (f v.2)
end
definition deg_j_seq_inv [constructor] : I ≃ I :=
prod_equiv_prod (add_right_action 1) (add_right_action (- 1))
prod_equiv_prod (add_right_action (1 : ℤ)) (add_right_action (- (1 : ℤ)))
definition fn_j_sequence [unfold 3] (x : I) :
D_sequence (deg_j_seq_inv x) →lm E_sequence x :=
@ -798,11 +804,11 @@ namespace spectrum
end
definition j_sequence : D_sequence →gm E_sequence :=
graded_hom.mk_out deg_j_seq_inv⁻¹ᵉ fn_j_sequence
graded_hom.mk_out deg_j_seq_inv⁻¹ᵉ (λi, idp) fn_j_sequence
definition k_sequence : E_sequence →gm D_sequence :=
begin
fapply graded_hom.mk erfl,
fapply graded_hom.mk erfl deg_eq_id,
intro v, induction v with n s,
apply lm_hom_int.mk, esimp,
exact πₛ→[n] (spoint (f s))
@ -816,10 +822,10 @@ namespace spectrum
intro y, induction x with n s, induction y with m t,
refine equiv_rect !pair_eq_pair_equiv⁻¹ᵉ _ _,
intro pq, esimp at pq, induction pq with p q,
revert t q, refine eq.rec_equiv (add_right_action (- 1)) _,
revert t q, refine eq.rec_equiv (add_right_action (-(1 : ℤ))) _,
induction p using eq.rec_symm,
apply is_exact_homotopy homotopy.rfl,
{ symmetry, exact graded_hom_mk_out_destruct deg_j_seq_inv⁻¹ᵉ fn_j_sequence },
{ symmetry, exact graded_hom_mk_out_destruct deg_j_seq_inv⁻¹ᵉ (λi, idp) fn_j_sequence },
rexact is_exact_of_is_exact_at (is_exact_LES_of_shomotopy_groups (f s) (m, 2)),
end
@ -829,7 +835,7 @@ namespace spectrum
revert x y p, refine eq.rec_right_inv (deg j_sequence) _,
intro x, induction x with n s,
apply is_exact_homotopy,
{ symmetry, exact graded_hom_mk_out_destruct deg_j_seq_inv⁻¹ᵉ fn_j_sequence },
{ symmetry, exact graded_hom_mk_out_destruct deg_j_seq_inv⁻¹ᵉ (λi, idp) fn_j_sequence },
{ reflexivity },
rexact is_exact_of_is_exact_at (is_exact_LES_of_shomotopy_groups (f s) (n, 1)),
end
@ -846,7 +852,7 @@ namespace spectrum
open int
parameters (ub : ℤ → ℤ) (lb : ℤ → ℤ)
(Aub : Π(s n : ℤ), s ≥ ub n + 1 → is_equiv (πₛ→[n] (f s)))
(Aub : Π(s n : ℤ), s ≥ ub n + (1 : ℤ) → is_equiv (πₛ→[n] (f s)))
(Alb : Π(s n : ℤ), s ≤ lb n → is_contr (πₛ[n] (A s)))
definition B : I → ℕ
@ -856,7 +862,7 @@ namespace spectrum
| (n, s) := max0 (ub n - s)
definition B'' : I → ℕ
| (n, s) := max0 (max (ub n + 1 - s) (ub (n+1) + 1 - s))
| (n, s) := max0 (max (ub n + (1 : ℤ) - s) (ub (n+(1 : ℤ)) + (1 : ℤ) - s))
lemma iterate_deg_i (n s : ℤ) (m : ℕ) : (deg i_sequence)^[m] (n, s) = (n, s - m) :=
begin
@ -904,11 +910,11 @@ namespace spectrum
definition is_bounded_sequence [constructor] : is_bounded exact_couple_sequence :=
is_bounded.mk B B' B'' Dub Dlb Elb
(by intro x; reflexivity)
begin
intro x, induction x with n s, apply pair_eq, esimp, esimp, esimp [j_sequence, i_sequence],
refine !add.assoc ⬝ ap (add s) !add.comm ⬝ !add.assoc⁻¹,
end
-- (by intro x; reflexivity)
-- begin
-- intro x, induction x with n s, apply pair_eq, esimp, esimp, esimp [j_sequence, i_sequence],
-- refine !add.assoc ⬝ ap (add s) !add.comm ⬝ !add.assoc⁻¹,
-- end
definition converges_to_sequence : (λn s, πₛ[n] (sfiber (f s))) ⟹ᵍ (λn, πₛ[n] (A (ub n))) :=
begin
@ -919,8 +925,8 @@ namespace spectrum
{ intro n, change max0 (ub n - ub n) = 0, exact ap max0 (sub_self (ub n)) },
{ intro ns, reflexivity },
{ intro n, reflexivity },
{ intro r, exact - 1 },
{ intro r, exact r + 1 },
{ intro r, exact - (1 : ℤ) },
{ intro r, exact r + (1 : ℤ) },
{ intro r n s, refine !convergence_theorem.deg_d ⬝ _,
refine ap (deg j_sequence) !iterate_deg_i_inv ⬝ _,
exact prod_eq idp (!add.assoc ⬝ ap (λx, s + (r + x)) !neg_neg) },
@ -933,7 +939,7 @@ namespace spectrum
-- print axioms is_bounded_sequence
-- I think it depends on univalence in an essential way. The reason is that the long exact sequence
-- It depends on univalence in an essential way. The reason is that the long exact sequence
-- of homotopy groups already depends on univalence. Namely, in that proof we need to show that if f
-- : A → B and g : B → C are exact at B, then ∥A∥₀ → ∥B∥₀ → ∥C∥₀ is exact at ∥B∥₀. For this we need
-- that the equality |b|₀ = |b'|₀ is equivalent to ∥b = b'∥₋₁, which requires univalence.

12
cohomology/projective_space.hlean
View file

@ -62,7 +62,7 @@ namespace temp
transport (is_contr ∘ E∞)
begin
induction m with m q, reflexivity, refine ap (deg (exact_couple.i X)) q ⬝ _,
exact prod_eq idp (neg_add m 1)⁻¹
exact prod_eq idp (neg_add m (1 : ℤ))⁻¹ᵖ
end
(fEinfd n m p)
@ -103,20 +103,20 @@ namespace temp
unreduced_ordinary_cohomology_isomorphism_right _ uH0_circle _,
end
definition Ex1 (n : ℕ) : AddGroup_of_AddAbGroup (E (-(n+1),- 1)) ≃g uH^n[K agℤ 2] :=
definition Ex1 (n : ℕ) : AddGroup_of_AddAbGroup (E (-(n+(1 : ℤ)),- (1 : ℤ))) ≃g uH^n[K agℤ 2] :=
begin
refine group_isomorphism_of_lm_isomorphism_int (converges_to.e fserre (-(n+1),- 1)) ⬝g _,
refine group_isomorphism_of_lm_isomorphism_int (converges_to.e fserre (-(n+(1 : ℤ)),- (1 : ℤ))) ⬝g _,
refine cohomology_change_int _ _ (ap neg _ ⬝ !neg_neg) ⬝g
unreduced_ordinary_cohomology_isomorphism_right _ !uH1_circle _,
exact ap (λx, x - - 1) !neg_add ⬝ !add_sub_cancel
exact ap (λx, x - - (1 : ℤ)) !neg_add ⬝ !add_sub_cancel
end
definition uH0 : uH^0[K agℤ 2] ≃g gℤ :=
(Ex0 0)⁻¹ᵍ ⬝g group_isomorphism_of_lm_isomorphism_int fE00
definition fE10 : is_contr (E (- 1,0)) :=
definition fE10 : is_contr (E (- (1 : ℤ),0)) :=
begin
refine @(is_trunc_equiv_closed _ _) (fEinf (- 1) 0 dec_star),
refine @(is_trunc_equiv_closed _ _) (fEinf (- (1 : ℤ)) 0 dec_star),
apply equiv_of_isomorphism,
refine Einf_isomorphism fserre 0 _ _,
intro r H, exact sorry, exact sorry --apply is_contr_fD2, change (- 1) - (- 1) >[ℤ] (- 0) - (r + 1),

21
homotopy/EM.hlean
View file

@ -403,8 +403,20 @@ namespace EM
EM_homomorphism_gloop (deloop X) n
((gloopn_succ_in' n (deloop X))⁻¹ᵍ⁸ ∘∞g Ωg'→[n] (deloop_isomorphism X)⁻¹ᵍ⁸ ∘∞g e)
definition is_mul_hom_EM_functor [constructor] (G H : AbGroup) (n : ℕ) :
is_mul_hom (λ(φ : G →gg H), EM_functor φ n) :=
-- definition is_mul_hom_EM_functor [constructor] (G H : AbGroup) (n : ℕ) :
-- is_mul_hom (λ(φ : G →gg H), EM_functor φ n) :=
-- begin
-- intro φ ψ,
-- apply eq_of_phomotopy,
-- exact sorry
-- -- exact sorry, exact sorry, exact sorry
-- -- refine idpath (φ 0 * ψ 0) ⬝ _,
-- end
/- an enriched homomorphism -/
definition EM_ehomomorphism [constructor] (G H : AbGroup) (n : ℕ) :
InfGroup_of_Group (G →gg H) →∞g InfGroup_of_deloopable (EM G n →** EM H n) :=
inf_homomorphism.mk (λφ, EM_functor φ n)
begin
intro φ ψ,
apply eq_of_phomotopy,
@ -413,11 +425,6 @@ namespace EM
-- refine idpath (φ 0 * ψ 0) ⬝ _,
end
/- an enriched homomorphism -/
definition EM_ehomomorphism [constructor] (G H : AbGroup) (n : ℕ) :
InfGroup_of_Group (G →gg H) →∞g InfGroup_of_deloopable (EM G n →** EM H n) :=
inf_homomorphism.mk (λφ, EM_functor φ n) (is_mul_hom_EM_functor G H n)
-- definition EM_homomorphism [unfold 8] {G : AbGroup} {X : Type*} (Y : Type*) (e : Ω Y ≃* X) (n : ℕ)
-- (e : AbInfGroup_of_AbGroup G →∞g Ωg[succ n] X) [H : is_trunc n X] : gEM G n →∞g X :=
-- _