Documentation

GQ2.Devissage.LESExact

§5.11 dévissage: exactness of the nine-term LES #

Part of the §5.11 dévissage development (split from GQ2/Devissage.lean).

Exactness of the nine-term LES #

Each spot is stated as y ∈ ker(out) ↔ y ∈ range(in) (equivalently at the ends, injectivity / surjectivity), the usual snake-lemma bookkeeping.

source
theorem GQ2.FoxH.H2wMap_g_surjective {C : Type u_1} [Group C] {A : Type u_3} {A'' : Type u_4} [AddCommGroup A] [DistribMulAction C A] [Finite A] [AddCommGroup A''] [DistribMulAction C A''] [Finite A''] [Finite C] (g : A →+ A'') (hg : ∀ (c : C) (a : A), g (c • a) = c • g a) (hsurj : Function.Surjective ⇑g) (t : Marking C) :
Function.Surjective ⇑(H2wMap t g hg)

Exactness at the right end: H²wMap g is surjective.

source
theorem GQ2.FoxH.H2w_exact_mid {C : Type u_1} [Group C] {A' : Type u_2} {A : Type u_3} {A'' : Type u_4} [AddCommGroup A'] [DistribMulAction C A'] [Finite A'] [AddCommGroup A] [DistribMulAction C A] [Finite A] [AddCommGroup A''] [DistribMulAction C A''] [Finite A''] [Finite C] (f : A' →+ A) (g : A →+ A'') (hf : ∀ (c : C) (a : A'), f (c • a) = c • f a) (hg : ∀ (c : C) (a : A), g (c • a) = c • g a) (hsurj : Function.Surjective ⇑g) (hexact : f.range = g.ker) (t : Marking C) (y : H2w t) :
y ∈ (H2wMap t g hg).ker ↔ y ∈ (H2wMap t f hf).range

Exactness at H²w(A): ker(H²wMap g) = range(H²wMap f).

source
theorem GQ2.FoxH.H0w_exact_mid {C : Type u_1} [Group C] {A' : Type u_2} {A : Type u_3} {A'' : Type u_4} [AddCommGroup A'] [DistribMulAction C A'] [AddCommGroup A] [DistribMulAction C A] [AddCommGroup A''] [DistribMulAction C A''] (f : A' →+ A) (g : A →+ A'') (hf : ∀ (c : C) (a : A'), f (c • a) = c • f a) (hg : ∀ (c : C) (a : A), g (c • a) = c • g a) (hinj : Function.Injective ⇑f) (hexact : f.range = g.ker) (t : Marking C) (a : ↥(H0w t)) :
a ∈ (H0wMap t g hg).ker ↔ a ∈ (H0wMap t f hf).range

Exactness at H⁰w(A): ker(H⁰wMap g) = range(H⁰wMap f).

source
theorem GQ2.FoxH.H0w_exact_right {C : Type u_1} [Group C] {A' : Type u_2} {A : Type u_3} {A'' : Type u_4} [AddCommGroup A'] [DistribMulAction C A'] [Finite A'] [AddCommGroup A] [DistribMulAction C A] [Finite A] [AddCommGroup A''] [DistribMulAction C A''] [Finite C] (f : A' →+ A) (g : A →+ A'') (hf : ∀ (c : C) (a : A'), f (c • a) = c • f a) (hg : ∀ (c : C) (a : A), g (c • a) = c • g a) (hinj : Function.Injective ⇑f) (hsurj : Function.Surjective ⇑g) (hexact : f.range = g.ker) (t : Marking C) (ht : t.TameRel) (hw : t.WildRel) (a'' : ↥(H0w t)) :
a'' ∈ (delta0 f g hf hg hinj hsurj hexact t ht hw).ker ↔ a'' ∈ (H0wMap t g hg).range

Exactness at H⁰w(A''): ker δ⁰ = range(H⁰wMap g).

source
theorem GQ2.FoxH.H1w_exact_left {C : Type u_1} [Group C] {A' : Type u_2} {A : Type u_3} {A'' : Type u_4} [AddCommGroup A'] [DistribMulAction C A'] [Finite A'] [AddCommGroup A] [DistribMulAction C A] [Finite A] [AddCommGroup A''] [DistribMulAction C A''] [Finite C] (f : A' →+ A) (g : A →+ A'') (hf : ∀ (c : C) (a : A'), f (c • a) = c • f a) (hg : ∀ (c : C) (a : A), g (c • a) = c • g a) (hinj : Function.Injective ⇑f) (hsurj : Function.Surjective ⇑g) (hexact : f.range = g.ker) (t : Marking C) (ht : t.TameRel) (hw : t.WildRel) (h : H1w t) :
h ∈ (H1wMap t f hf).ker ↔ h ∈ (delta0 f g hf hg hinj hsurj hexact t ht hw).range

Exactness at H¹w(A'): ker(H¹wMap f) = range δ⁰.

source
theorem GQ2.FoxH.H1w_exact_mid {C : Type u_1} [Group C] {A' : Type u_2} {A : Type u_3} {A'' : Type u_4} [AddCommGroup A'] [DistribMulAction C A'] [Finite A'] [AddCommGroup A] [DistribMulAction C A] [Finite A] [AddCommGroup A''] [DistribMulAction C A''] [Finite A''] [Finite C] (f : A' →+ A) (g : A →+ A'') (hf : ∀ (c : C) (a : A'), f (c • a) = c • f a) (hg : ∀ (c : C) (a : A), g (c • a) = c • g a) (hinj : Function.Injective ⇑f) (hsurj : Function.Surjective ⇑g) (hexact : f.range = g.ker) (t : Marking C) (ht : t.TameRel) (hw : t.WildRel) (h : H1w t) :
h ∈ (H1wMap t g hg).ker ↔ h ∈ (H1wMap t f hf).range

Exactness at H¹w(A): ker(H¹wMap g) = range(H¹wMap f).

source
theorem GQ2.FoxH.H1w_exact_right {C : Type u_1} [Group C] {A' : Type u_2} {A : Type u_3} {A'' : Type u_4} [AddCommGroup A'] [DistribMulAction C A'] [Finite A'] [AddCommGroup A] [DistribMulAction C A] [Finite A] [AddCommGroup A''] [DistribMulAction C A''] [Finite A''] [Finite C] (f : A' →+ A) (g : A →+ A'') (hf : ∀ (c : C) (a : A'), f (c • a) = c • f a) (hg : ∀ (c : C) (a : A), g (c • a) = c • g a) (hinj : Function.Injective ⇑f) (hsurj : Function.Surjective ⇑g) (hexact : f.range = g.ker) (t : Marking C) (ht : t.TameRel) (hw : t.WildRel) (h : H1w t) :
h ∈ (delta1 f g hf hg hinj hsurj hexact t ht hw).ker ↔ h ∈ (H1wMap t g hg).range

Exactness at H¹w(A''): ker δ¹ = range(H¹wMap g).

source
theorem GQ2.FoxH.H2w_exact_left {C : Type u_1} [Group C] {A' : Type u_2} {A : Type u_3} {A'' : Type u_4} [AddCommGroup A'] [DistribMulAction C A'] [Finite A'] [AddCommGroup A] [DistribMulAction C A] [Finite A] [AddCommGroup A''] [DistribMulAction C A''] [Finite A''] [Finite C] (f : A' →+ A) (g : A →+ A'') (hf : ∀ (c : C) (a : A'), f (c • a) = c • f a) (hg : ∀ (c : C) (a : A), g (c • a) = c • g a) (hinj : Function.Injective ⇑f) (hsurj : Function.Surjective ⇑g) (hexact : f.range = g.ker) (t : Marking C) (ht : t.TameRel) (hw : t.WildRel) (y : H2w t) :
y ∈ (H2wMap t f hf).ker ↔ y ∈ (delta1 f g hf hg hinj hsurj hexact t ht hw).range

Exactness at H²w(A'): ker(H²wMap f) = range δ¹.