continue convergence theorem
This commit is contained in:
Floris van Doorn
parent
43f9edf82b
commit
daedc1dc48
5 changed files with 190 additions and 29 deletions
|
|
@ -424,7 +424,7 @@ definition graded_quotient_map [constructor] (S : Πi, submodule_rel (M i)) :
|
|||
graded_hom.mk erfl (λi, quotient_map (S i))
|
||||
|
||||
definition graded_homology (g : M₂ →gm M₃) (f : M₁ →gm M₂) : graded_module R I :=
|
||||
λi, homology (g i) (f ↘ (to_right_inv (deg f) i))
|
||||
λi, homology (g i) (f ← i)
|
||||
|
||||
definition graded_homology_intro [constructor] (g : M₂ →gm M₃) (f : M₁ →gm M₂) :
|
||||
graded_kernel g →gm graded_homology g f :=
|
||||
|
|
@ -484,10 +484,10 @@ namespace left_module
|
|||
definition E' : graded_module R I := graded_homology d d
|
||||
|
||||
definition is_contr_E' {x : I} (H : is_contr (E x)) : is_contr (E' x) :=
|
||||
sorry
|
||||
!is_contr_homology
|
||||
|
||||
definition is_contr_D' {x : I} (H : is_contr (D x)) : is_contr (D' x) :=
|
||||
sorry
|
||||
!is_contr_image_module
|
||||
|
||||
definition i' : D' →gm D' :=
|
||||
graded_image_lift i ∘gm graded_submodule_incl _
|
||||
|
|
@ -595,10 +595,10 @@ namespace left_module
|
|||
ij := i'j' X, jk := j'k' X, ki := k'i' X⦄
|
||||
|
||||
parameters {R : Ring} {I : Set} (X : exact_couple R I) (B : I → ℕ)
|
||||
(Dub : Π⦃x y⦄ ⦃s : ℕ⦄, B x ≤ s → deg (j X) (iterate (deg (i X)) s x) = y → is_contr (D X y))
|
||||
(Dlb : Π⦃x y⦄ ⦃s : ℕ⦄, B x ≤ s → deg (j X) (iterate (deg (i X))⁻¹ s x) = y → is_contr (D X y))
|
||||
(Eub : Π⦃x y⦄ ⦃s : ℕ⦄, B x ≤ s → deg (j X) (iterate (deg (i X)) s x) = y → is_contr (E X y))
|
||||
(Elb : Π⦃x y⦄ ⦃s : ℕ⦄, B x ≤ s → deg (j X) (iterate (deg (i X))⁻¹ s x) = y → is_contr (E X y))
|
||||
(Dub : Π⦃x y⦄ ⦃s : ℕ⦄, B x ≤ s → (deg (k X))⁻¹ (iterate (deg (i X)) s ((deg (j X))⁻¹ x)) = y → is_contr (D X y))
|
||||
(Eub : Π⦃x y⦄ ⦃s : ℕ⦄, B x ≤ s → (deg (k X))⁻¹ (iterate (deg (i X)) s ((deg (j X))⁻¹ x)) = y → is_contr (E X y))
|
||||
(Dlb : Π⦃x y⦄ ⦃s : ℕ⦄, B x ≤ s → deg (j X) (iterate (deg (i X))⁻¹ s (deg (k X) x)) = y → is_contr (D X y))
|
||||
(Elb : Π⦃x y⦄ ⦃s : ℕ⦄, B x ≤ s → deg (j X) (iterate (deg (i X))⁻¹ s (deg (k X) x)) = y → is_contr (E X y))
|
||||
-- also need a single deg j and/or deg k here
|
||||
|
||||
-- we start counting pages at 0, not at 2.
|
||||
|
|
@ -642,13 +642,48 @@ namespace left_module
|
|||
deg (d (page r)) ~ deg (j X) ∘ iterate (deg (i X))⁻¹ r ∘ deg (k X) :=
|
||||
compose2 (deg_j r) (deg_k r)
|
||||
|
||||
definition Eub' (x : I) (r : ℕ) (h : B (deg (k X) x) ≤ r) :
|
||||
definition deg_d_inv (r : ℕ) :
|
||||
(deg (d (page r)))⁻¹ ~ (deg (k X))⁻¹ ∘ iterate (deg (i X)) r ∘ (deg (j X))⁻¹ :=
|
||||
sorry --inv_homotopy_inv (deg_d r) ⬝hty _ --compose2 (deg_j r) (deg_k r)
|
||||
|
||||
include Elb Eub
|
||||
definition Eub' (x : I) (r : ℕ) (h : B x ≤ r) :
|
||||
is_contr (E (page r) (deg (d (page r)) x)) :=
|
||||
is_contr_E _ _ (Elb h (deg_d r x)⁻¹)
|
||||
|
||||
definition Estable {x : I} {r : ℕ} (H : B (deg (k X) x) ≤ r) :
|
||||
E (page (r + 1)) x ≃ E (page r) x :=
|
||||
sorry
|
||||
definition Elb' (x : I) (r : ℕ) (h : B x ≤ r) :
|
||||
is_contr (E (page r) ((deg (d (page r)))⁻¹ x)) :=
|
||||
is_contr_E _ _ (Eub h (deg_d_inv r x)⁻¹)
|
||||
|
||||
-- definition Dub' (x : I) (r : ℕ) (h : B x ≤ r) :
|
||||
-- is_contr (D (page r) (deg (d (page r)) x)) :=
|
||||
-- is_contr_D _ _ (Dlb h (deg_d r x)⁻¹)
|
||||
|
||||
-- definition Dlb' (x : I) (r : ℕ) (h : B x ≤ r) :
|
||||
-- is_contr (D (page r) ((deg (d (page r)))⁻¹ x)) :=
|
||||
-- is_contr_D _ _ (Dub h (deg_d_inv r x)⁻¹)
|
||||
|
||||
definition Estable {x : I} {r : ℕ} (H : B x ≤ r) :
|
||||
E (page (r + 1)) x ≃lm E (page r) x :=
|
||||
begin
|
||||
change homology (d (page r) x) (d (page r) ← x) ≃lm E (page r) x,
|
||||
apply homology_isomorphism,
|
||||
exact Elb' _ _ H, exact Eub' _ _ H
|
||||
end
|
||||
|
||||
definition is_equiv_i {x y : I} {r : ℕ} (H : B y ≤ r) (p : deg (i (page r)) x = y) :
|
||||
is_equiv (i (page r) ↘ p) :=
|
||||
begin
|
||||
induction p,
|
||||
exact sorry
|
||||
end
|
||||
|
||||
definition Dstable {x : I} {r : ℕ} (H : B x ≤ r) :
|
||||
D (page (r + 1)) x ≃lm D (page r) x :=
|
||||
begin
|
||||
change image_module (i (page r) ← x) ≃lm D (page r) x,
|
||||
exact image_module_isomorphism (isomorphism.mk (i (page r) ← x) (is_equiv_i H _))
|
||||
end
|
||||
|
||||
definition inf_page : graded_module R I :=
|
||||
λx, E (page (B (deg (k X) x))) x
|
||||
|
|
|
|||
|
|
@ -144,11 +144,7 @@ namespace group
|
|||
homomorphism.mk class_of (λ g h, idp)
|
||||
|
||||
definition ab_qg_map {G : AbGroup} (N : subgroup_rel G) : G →g quotient_ab_group N :=
|
||||
begin
|
||||
fapply homomorphism.mk,
|
||||
exact class_of,
|
||||
exact λ g h, idp
|
||||
end
|
||||
qg_map _
|
||||
|
||||
definition is_surjective_ab_qg_map {A : AbGroup} (N : subgroup_rel A) : is_surjective (ab_qg_map N) :=
|
||||
begin
|
||||
|
|
|
|||
|
|
@ -243,11 +243,7 @@ namespace group
|
|||
end
|
||||
|
||||
definition is_embedding_incl_of_subgroup {G : Group} (H : subgroup_rel G) : is_embedding (incl_of_subgroup H) :=
|
||||
begin
|
||||
fapply function.is_embedding_of_is_injective,
|
||||
intro h h',
|
||||
fapply subtype_eq
|
||||
end
|
||||
function.is_embedding_pr1 _
|
||||
|
||||
definition ab_kernel_incl {G H : AbGroup} (f : G →g H) : ab_kernel f →g G :=
|
||||
begin
|
||||
|
|
@ -447,8 +443,8 @@ definition hom_lift [constructor] {G H : Group} (f : G →g H) (K : subgroup_rel
|
|||
|
||||
definition ab_subgroup_of_subgroup_incl {A : AbGroup} {R S : subgroup_rel A} (H : Π (a : A), R a -> S a) : ab_subgroup R →g ab_subgroup S
|
||||
:=
|
||||
ab_subgroup_functor (gid A) H
|
||||
|
||||
ab_subgroup_functor (gid A) H
|
||||
|
||||
definition is_embedding_ab_subgroup_of_subgroup_incl {A : AbGroup} {R S : subgroup_rel A} (H : Π (a : A), R a -> S a) : is_embedding (ab_subgroup_of_subgroup_incl H) :=
|
||||
begin
|
||||
fapply is_embedding_subgroup_of_subgroup_incl,
|
||||
|
|
|
|||
|
|
@ -1,12 +1,39 @@
|
|||
|
||||
import .left_module .quotient_group
|
||||
|
||||
open algebra eq group sigma is_trunc function trunc
|
||||
open algebra eq group sigma is_trunc function trunc equiv is_equiv
|
||||
|
||||
-- move to subgroup
|
||||
attribute normal_subgroup_rel._trans_of_to_subgroup_rel [unfold 2]
|
||||
attribute normal_subgroup_rel.to_subgroup_rel [constructor]
|
||||
|
||||
definition is_equiv_incl_of_subgroup {G : Group} (H : subgroup_rel G) (h : Πg, H g) :
|
||||
is_equiv (incl_of_subgroup H) :=
|
||||
have is_surjective (incl_of_subgroup H),
|
||||
begin intro g, exact image.mk ⟨g, h g⟩ idp end,
|
||||
have is_embedding (incl_of_subgroup H), from is_embedding_incl_of_subgroup H,
|
||||
function.is_equiv_of_is_surjective_of_is_embedding (incl_of_subgroup H)
|
||||
|
||||
definition subgroup_isomorphism [constructor] {G : Group} (H : subgroup_rel G) (h : Πg, H g) :
|
||||
subgroup H ≃g G :=
|
||||
isomorphism.mk _ (is_equiv_incl_of_subgroup H h)
|
||||
|
||||
definition is_equiv_qg_map {G : Group} (H : normal_subgroup_rel G) (H₂ : Π⦃g⦄, H g → g = 1) :
|
||||
is_equiv (qg_map H) :=
|
||||
set_quotient.is_equiv_class_of _ (λg h r, eq_of_mul_inv_eq_one (H₂ r))
|
||||
|
||||
definition quotient_group_isomorphism [constructor] {G : Group} (H : normal_subgroup_rel G)
|
||||
(h : Πg, H g → g = 1) : quotient_group H ≃g G :=
|
||||
(isomorphism.mk _ (is_equiv_qg_map H h))⁻¹ᵍ
|
||||
|
||||
definition is_equiv_ab_qg_map {G : AbGroup} (H : subgroup_rel G) (h : Π⦃g⦄, H g → g = 1) :
|
||||
is_equiv (ab_qg_map H) :=
|
||||
proof is_equiv_qg_map _ h qed
|
||||
|
||||
definition ab_quotient_group_isomorphism [constructor] {G : AbGroup} (H : subgroup_rel G)
|
||||
(h : Πg, H g → g = 1) : quotient_ab_group H ≃g G :=
|
||||
(isomorphism.mk _ (is_equiv_ab_qg_map H h))⁻¹ᵍ
|
||||
|
||||
namespace left_module
|
||||
/- submodules -/
|
||||
variables {R : Ring} {M M₁ M₂ M₃ : LeftModule R} {m m₁ m₂ : M}
|
||||
|
|
@ -105,7 +132,7 @@ definition incl_smul (S : submodule_rel M) (r : R) (m : M) (h : S m) :
|
|||
r • ⟨m, h⟩ = ⟨_, contains_smul S r h⟩ :> submodule S :=
|
||||
by reflexivity
|
||||
|
||||
definition submodule_rel_of_submodule [constructor] (S₂ S₁ : submodule_rel M) :
|
||||
definition submodule_rel_submodule [constructor] (S₂ S₁ : submodule_rel M) :
|
||||
submodule_rel (submodule S₂) :=
|
||||
submodule_rel.mk (λm, S₁ (submodule_incl S₂ m))
|
||||
(contains_zero S₁)
|
||||
|
|
@ -114,6 +141,23 @@ submodule_rel.mk (λm, S₁ (submodule_incl S₂ m))
|
|||
intro m r p, induction m with m hm, exact contains_smul S₁ r p
|
||||
end
|
||||
|
||||
definition submodule_rel_submodule_trivial [constructor] {S₂ S₁ : submodule_rel M}
|
||||
(h : Π⦃m⦄, S₁ m → m = 0) ⦃m : submodule S₂⦄ (Sm : submodule_rel_submodule S₂ S₁ m) : m = 0 :=
|
||||
begin
|
||||
fapply subtype_eq,
|
||||
apply h Sm
|
||||
end
|
||||
|
||||
definition is_prop_submodule (S : submodule_rel M) [H : is_prop M] : is_prop (submodule S) :=
|
||||
begin apply @is_trunc_sigma, exact H end
|
||||
local attribute is_prop_submodule [instance]
|
||||
definition is_contr_submodule [instance] (S : submodule_rel M) [is_contr M] : is_contr (submodule S) :=
|
||||
is_contr_of_inhabited_prop 0
|
||||
|
||||
definition submodule_isomorphism [constructor] (S : submodule_rel M) (h : Πg, S g) :
|
||||
submodule S ≃lm M :=
|
||||
isomorphism.mk (submodule_incl S) (is_equiv_incl_of_subgroup (subgroup_rel_of_submodule_rel S) h)
|
||||
|
||||
/- quotient modules -/
|
||||
|
||||
definition quotient_module' (S : submodule_rel M) : AddAbGroup :=
|
||||
|
|
@ -123,7 +167,7 @@ definition quotient_module_smul [constructor] (S : submodule_rel M) (r : R) :
|
|||
quotient_module' S →a quotient_module' S :=
|
||||
quotient_ab_group_functor (smul_homomorphism M r) (λg, contains_smul S r)
|
||||
|
||||
set_option formatter.hide_full_terms false
|
||||
|
||||
|
||||
definition quotient_module_smul_right_distrib (r s : R) (n : quotient_module' S) :
|
||||
quotient_module_smul S (r + s) n = quotient_module_smul S r n + quotient_module_smul S s n :=
|
||||
|
|
@ -172,6 +216,18 @@ lm_homomorphism_of_group_homomorphism
|
|||
exact to_respect_smul φ r m
|
||||
end
|
||||
|
||||
definition is_prop_quotient_module (S : submodule_rel M) [H : is_prop M] : is_prop (quotient_module S) :=
|
||||
begin apply @set_quotient.is_trunc_set_quotient, exact H end
|
||||
local attribute is_prop_quotient_module [instance]
|
||||
|
||||
definition is_contr_quotient_module [instance] (S : submodule_rel M) [is_contr M] :
|
||||
is_contr (quotient_module S) :=
|
||||
is_contr_of_inhabited_prop 0
|
||||
|
||||
definition quotient_module_isomorphism [constructor] (S : submodule_rel M) (h : Π⦃m⦄, S m → m = 0) :
|
||||
quotient_module S ≃lm M :=
|
||||
(isomorphism.mk (quotient_map S) (is_equiv_ab_qg_map (subgroup_rel_of_submodule_rel S) h))⁻¹ˡᵐ
|
||||
|
||||
/- specific submodules -/
|
||||
definition has_scalar_image (φ : M₁ →lm M₂) ⦃m : M₂⦄ (r : R)
|
||||
(h : image φ m) : image φ (r • m) :=
|
||||
|
|
@ -186,6 +242,14 @@ submodule_rel_of_subgroup_rel
|
|||
(image_subgroup (group_homomorphism_of_lm_homomorphism φ))
|
||||
(has_scalar_image φ)
|
||||
|
||||
definition image_rel_trivial (φ : M₁ →lm M₂) [H : is_contr M₁] ⦃m : M₂⦄ (h : image_rel φ m) : m = 0 :=
|
||||
begin
|
||||
refine image.rec _ h,
|
||||
intro x p,
|
||||
refine p⁻¹ ⬝ ap φ _ ⬝ to_respect_zero φ,
|
||||
apply @is_prop.elim, apply is_trunc_succ, exact H
|
||||
end
|
||||
|
||||
definition image_module [constructor] (φ : M₁ →lm M₂) : LeftModule R := submodule (image_rel φ)
|
||||
|
||||
-- unfortunately this is note definitionally equal:
|
||||
|
|
@ -213,21 +277,50 @@ begin
|
|||
reflexivity
|
||||
end
|
||||
|
||||
definition is_contr_image_module [instance] (φ : M₁ →lm M₂) [is_contr M₂] :
|
||||
is_contr (image_module φ) :=
|
||||
!is_contr_submodule
|
||||
|
||||
definition is_contr_image_module_of_is_contr_dom (φ : M₁ →lm M₂) [is_contr M₁] :
|
||||
is_contr (image_module φ) :=
|
||||
is_contr.mk 0
|
||||
begin
|
||||
have Π(x : image_module φ), is_prop (0 = x), from _,
|
||||
apply @total_image.rec,
|
||||
exact this,
|
||||
intro m,
|
||||
induction (is_prop.elim 0 m), apply subtype_eq,
|
||||
exact (to_respect_zero φ)⁻¹
|
||||
end
|
||||
|
||||
definition image_module_isomorphism [constructor] (φ : M₁ ≃lm M₂) : image_module φ ≃lm M₂ :=
|
||||
submodule_isomorphism _ (λm, image.mk (φ⁻¹ˡᵐ m) proof to_right_inv (equiv_of_isomorphism φ) m qed)
|
||||
|
||||
definition has_scalar_kernel (φ : M₁ →lm M₂) ⦃m : M₁⦄ (r : R)
|
||||
(p : φ m = 0) : φ (r • m) = 0 :=
|
||||
begin
|
||||
refine to_respect_smul φ r m ⬝ ap (λx, r • x) p ⬝ smul_zero r,
|
||||
end
|
||||
|
||||
definition kernel_rel [constructor](φ : M₁ →lm M₂) : submodule_rel M₁ :=
|
||||
definition kernel_rel [constructor] (φ : M₁ →lm M₂) : submodule_rel M₁ :=
|
||||
submodule_rel_of_subgroup_rel
|
||||
(kernel_subgroup (group_homomorphism_of_lm_homomorphism φ))
|
||||
(has_scalar_kernel φ)
|
||||
|
||||
definition kernel_rel_full (φ : M₁ →lm M₂) [is_contr M₂] (m : M₁) : kernel_rel φ m :=
|
||||
!is_prop.elim
|
||||
|
||||
definition kernel_module [constructor] (φ : M₁ →lm M₂) : LeftModule R := submodule (kernel_rel φ)
|
||||
|
||||
definition is_contr_kernel_module [instance] (φ : M₁ →lm M₂) [is_contr M₁] :
|
||||
is_contr (kernel_module φ) :=
|
||||
!is_contr_submodule
|
||||
|
||||
definition kernel_module_isomorphism [constructor] (φ : M₁ →lm M₂) [is_contr M₂] : kernel_module φ ≃lm M₁ :=
|
||||
submodule_isomorphism _ (kernel_rel_full φ)
|
||||
|
||||
definition homology (ψ : M₂ →lm M₃) (φ : M₁ →lm M₂) : LeftModule R :=
|
||||
@quotient_module R (submodule (kernel_rel ψ)) (submodule_rel_of_submodule _ (image_rel φ))
|
||||
@quotient_module R (submodule (kernel_rel ψ)) (submodule_rel_submodule _ (image_rel φ))
|
||||
|
||||
definition homology.mk (m : M₂) (h : ψ m = 0) : homology ψ φ :=
|
||||
quotient_map _ ⟨m, h⟩
|
||||
|
|
@ -255,6 +348,15 @@ quotient_elim (θ ∘lm submodule_incl _)
|
|||
exact ap θ p⁻¹ ⬝ H m'
|
||||
end
|
||||
|
||||
definition is_contr_homology [instance] (ψ : M₂ →lm M₃) (φ : M₁ →lm M₂) [is_contr M₂] :
|
||||
is_contr (homology ψ φ) :=
|
||||
begin apply @is_contr_quotient_module end
|
||||
|
||||
definition homology_isomorphism [constructor] (ψ : M₂ →lm M₃) (φ : M₁ →lm M₂) [is_contr M₁] [is_contr M₃] :
|
||||
homology ψ φ ≃lm M₂ :=
|
||||
quotient_module_isomorphism _ (submodule_rel_submodule_trivial (image_rel_trivial φ)) ⬝lm
|
||||
!kernel_module_isomorphism
|
||||
|
||||
-- remove:
|
||||
|
||||
-- definition homology.rec (P : homology ψ φ → Type)
|
||||
|
|
|
|||
|
|
@ -1,6 +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
|
||||
import homotopy.sphere2 homotopy.cofiber homotopy.wedge hit.prop_trunc hit.set_quotient
|
||||
|
||||
open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc_index pi group
|
||||
is_trunc function sphere unit sum prod bool
|
||||
|
|
@ -1164,3 +1164,35 @@ structure Ring :=
|
|||
|
||||
attribute Ring.carrier [coercion]
|
||||
attribute Ring.struct [instance]
|
||||
|
||||
namespace set_quotient
|
||||
definition is_prop_set_quotient {A : Type} (R : A → A → Prop) [is_prop A] : is_prop (set_quotient R) :=
|
||||
begin
|
||||
apply is_prop.mk, intro x y,
|
||||
induction x using set_quotient.rec_prop, induction y using set_quotient.rec_prop,
|
||||
exact ap class_of !is_prop.elim
|
||||
end
|
||||
|
||||
local attribute is_prop_set_quotient [instance]
|
||||
definition is_trunc_set_quotient [instance] (n : ℕ₋₂) {A : Type} (R : A → A → Prop) [is_trunc n A] :
|
||||
is_trunc n (set_quotient R) :=
|
||||
begin
|
||||
cases n with n, { apply is_contr_of_inhabited_prop, exact class_of !center },
|
||||
cases n with n, { apply _ },
|
||||
apply is_trunc_succ_succ_of_is_set
|
||||
end
|
||||
|
||||
definition is_equiv_class_of [constructor] {A : Type} [is_set A] (R : A → A → Prop)
|
||||
(p : Π⦃a b⦄, R a b → a = b) : is_equiv (@class_of A R) :=
|
||||
begin
|
||||
fapply adjointify,
|
||||
{ intro x, induction x, exact a, exact p H },
|
||||
{ intro x, induction x using set_quotient.rec_prop, reflexivity },
|
||||
{ intro a, reflexivity }
|
||||
end
|
||||
|
||||
definition equiv_set_quotient [constructor] {A : Type} [is_set A] (R : A → A → Prop)
|
||||
(p : Π⦃a b⦄, R a b → a = b) : A ≃ set_quotient R :=
|
||||
equiv.mk _ (is_equiv_class_of R p)
|
||||
|
||||
end set_quotient
|
||||
|
|
|
|||
Loading…
Reference in a new issue