progress on derived exact couples
This commit is contained in:
Egbert Rijke
parent
b57eadc56a
commit
81e6c07f23
2 changed files with 77 additions and 17 deletions
|
|
@ -6,29 +6,29 @@ Authors: Egbert Rijke
|
|||
Exact couple, derived couples, and so on
|
||||
-/
|
||||
|
||||
import algebra.group_theory hit.set_quotient types.sigma types.list types.sum
|
||||
import algebra.group_theory hit.set_quotient types.sigma types.list types.sum .quotient_group .subgroup
|
||||
|
||||
open eq algebra is_trunc set_quotient relation sigma sigma.ops prod prod.ops sum list trunc function group
|
||||
open eq algebra is_trunc set_quotient relation sigma sigma.ops prod prod.ops sum list trunc function group trunc
|
||||
equiv
|
||||
|
||||
definition kernel.{l1} {A B : CommGroup.{l1}} (f : A →g B) : CommGroup.{l1} :=
|
||||
begin
|
||||
fapply CommGroup.mk,
|
||||
{ exact fiber f 1},
|
||||
fapply comm_group.mk,
|
||||
{ intro x, induction x with a p, intro y, induction y with b q, fapply fiber.mk, exact a*b, rewrite respect_mul, rewrite p, rewrite q, apply mul_one},
|
||||
{ exact sorry },
|
||||
{ intros x y z, induction x with a p, induction y with b q, induction z with c r, esimp, exact sorry }, repeat exact sorry
|
||||
end
|
||||
|
||||
structure is_exact {A B C : CommGroup} (f : A →g B) (g : B →g C) :=
|
||||
( im_in_ker : Π(a:A), g (f a) = 1)
|
||||
( ker_in_im : Π(b:B), (g b = 1) → Σ(a:A), f a = b)
|
||||
( ker_in_im : Π(b:B), (g b = 1) → ∃(a:A), f a = b)
|
||||
|
||||
definition isBoundary {B : CommGroup} (d : B →g B) := Π(b:B), d b = 1
|
||||
definition is_boundary {B : CommGroup} (d : B →g B) := Π(b:B), d (d b) = 1
|
||||
|
||||
-- definition homology {B : CommGroup} (d : B →g B) (H : isBoundary d) :=
|
||||
-- quotient_group (kernel d) (image d)
|
||||
definition image_subgroup_of_bd {B : CommGroup} (d : B →g B) (H : is_boundary d) : subgroup_rel (comm_kernel d) :=
|
||||
subgroup_rel_of_subgroup (image_subgroup d) (kernel_subgroup d)
|
||||
begin
|
||||
intro g p,
|
||||
induction p with f, induction f with h p,
|
||||
rewrite [p⁻¹],
|
||||
esimp,
|
||||
exact H h
|
||||
end
|
||||
|
||||
definition homology {B : CommGroup} (d : B →g B) (H : is_boundary d) : CommGroup :=
|
||||
@quotient_comm_group (comm_kernel d) (image_subgroup_of_bd d H)
|
||||
|
||||
structure exact_couple (A B : CommGroup) : Type :=
|
||||
( i : A →g A) (j : A →g B) (k : B →g A)
|
||||
|
|
@ -36,7 +36,34 @@ structure exact_couple (A B : CommGroup) : Type :=
|
|||
( exact_jk : is_exact j k)
|
||||
( exact_ki : is_exact k i)
|
||||
|
||||
definition boundary {A B : CommGroup} (CC : exact_couple A B) : B →g B := (exact_couple.j CC) ∘g (exact_couple.k CC)
|
||||
definition boundary {A B : CommGroup} (CC : exact_couple A B) : B →g B :=
|
||||
(exact_couple.j CC) ∘g (exact_couple.k CC)
|
||||
|
||||
definition boundary_is_boundary {A B : CommGroup} (CC : exact_couple A B) : is_boundary (boundary CC) :=
|
||||
begin
|
||||
induction CC,
|
||||
induction exact_jk,
|
||||
intro b,
|
||||
exact (ap (group_fun j) (im_in_ker (group_fun k b))) ⬝ (respect_one j)
|
||||
end
|
||||
|
||||
section derived_couple
|
||||
|
||||
variables {A B : CommGroup} (CC : exact_couple A B)
|
||||
|
||||
definition derived_couple_A : CommGroup :=
|
||||
comm_subgroup (image_subgroup (exact_couple.i CC))
|
||||
|
||||
definition derived_couple_B : CommGroup :=
|
||||
homology (boundary CC) (boundary_is_boundary CC)
|
||||
|
||||
definition derived_couple_i : derived_couple_A CC →g derived_couple_A CC :=
|
||||
(image_lift (exact_couple.i CC)) ∘g (image_incl (exact_couple.i CC))
|
||||
|
||||
definition derived_couple_j : derived_couple_A CC →g derived_couple_B CC :=
|
||||
begin
|
||||
-- refine (comm_gq_map (comm_kernel (boundary CC)) (image_subgroup_of_bd (boundary CC) (boundary_is_boundary CC))) ∘g _,
|
||||
exact sorry
|
||||
end
|
||||
|
||||
end derived_couple
|
||||
|
|
|
|||
|
|
@ -232,6 +232,8 @@ namespace group
|
|||
|
||||
definition kernel {G H : Group} (f : G →g H) : Group := subgroup (kernel_subgroup f)
|
||||
|
||||
definition comm_kernel {G H : CommGroup} (f : G →g H) : CommGroup := comm_subgroup (kernel_subgroup f)
|
||||
|
||||
definition incl_of_subgroup [constructor] {G : Group} (H : subgroup_rel G) : subgroup H →g G :=
|
||||
begin
|
||||
fapply homomorphism.mk,
|
||||
|
|
@ -252,4 +254,35 @@ namespace group
|
|||
-- closed under inverses
|
||||
(λ h p, subgroup_respect_inv H1 p)
|
||||
|
||||
definition image {G H : Group} (f : G →g H) : Group :=
|
||||
subgroup (image_subgroup f)
|
||||
|
||||
definition image_incl {G H : Group} (f : G →g H) : image f →g H :=
|
||||
incl_of_subgroup (image_subgroup f)
|
||||
|
||||
definition hom_lift {G H : Group} (f : G →g H) (K : subgroup_rel H) (Hyp : Π (g : G), K (f g)) : G →g subgroup K :=
|
||||
begin
|
||||
fapply homomorphism.mk,
|
||||
intro g,
|
||||
fapply sigma.mk,
|
||||
exact f g,
|
||||
fapply Hyp,
|
||||
intro g h, apply subtype_eq, esimp, apply respect_mul
|
||||
end
|
||||
|
||||
definition image_lift {G H : Group} (f : G →g H) : G →g image f :=
|
||||
begin
|
||||
fapply hom_lift f,
|
||||
intro g,
|
||||
apply tr,
|
||||
fapply fiber.mk,
|
||||
exact g, reflexivity
|
||||
end
|
||||
|
||||
definition image_factor {G H : Group} (f : G →g H) : f = (image_incl f) ∘g (image_lift f) :=
|
||||
begin
|
||||
fapply homomorphism_eq,
|
||||
reflexivity
|
||||
end
|
||||
|
||||
end group
|
||||
|
|
|
|||
Loading…
Reference in a new issue