Yamaguchi Lean 4 Library
ProCGroups.CrowellExactSequence.Basic
ProCGroups/CrowellExactSequence/Basic

ProCGroups.CrowellExactSequence.Basic

8 Theorems | 3 Definitions | 1 Abbreviation | 1 Structure

Crowell exact sequences / Basic.

This module contains the common four-term linear-sequence interface, exactness transport lemmas, and the finite Blanchfield--Lyndon coordinate map used by the discrete and profinite theories.

imports
Imported by

Declarations

Abbreviation CrowellExactSequence.blanchfieldLyndonFiniteFamilyMap 
abbrev blanchfieldLyndonFiniteFamilyMap (generators : X → M) :
    (X → R) →ₗ[R] M :=
  finiteFamilyLinearMap (R := R) generators

The Blanchfield--Lyndon finite-family map associated to a chosen boundary-generating family.

Theorem CrowellExactSequence.blanchfieldLyndonFiniteFamilyMap_apply 
omit [DecidableEq X] in
theorem blanchfieldLyndonFiniteFamilyMap_apply (generators : X → M) (x : X → R) :
    blanchfieldLyndonFiniteFamilyMap (R := R) generators x = ∑ i, x i • generators i

The Blanchfield--Lyndon finite-family boundary map is evaluated on the canonical generators and then extended linearly to the coordinate module.

Show Lean proof
Theorem CrowellExactSequence.blanchfieldLyndonFiniteFamilyMap_single 
@[simp]
theorem blanchfieldLyndonFiniteFamilyMap_single (generators : X → M) (i : X) :
    blanchfieldLyndonFiniteFamilyMap (R := R) generators (Pi.single i 1) = generators i

A Blanchfield--Lyndon finite-family map sends a coordinate basis vector to its generator.

Show Lean proof
Structure CrowellExactSequence.FourTermLinearSequence 
structure FourTermLinearSequence (R : Type*) [Semiring R]
    (A B C D : Type*)
    [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [AddCommMonoid D]
    [Module R A] [Module R B] [Module R C] [Module R D] where
  /-- The first linear map, from \(A\) to \(B\). -/
  head : A →ₗ[R] B
  /-- The middle linear map, from \(B\) to \(C\). -/
  middle : B →ₗ[R] C
  /-- The final linear map, from \(C\) to \(D\). -/
  tail : C →ₗ[R] D
  /-- The middle map vanishes after the head map. -/
  middle_comp_head : middle.comp head = 0
  /-- The tail map vanishes after the middle map. -/
  tail_comp_middle : tail.comp middle = 0

A bundled four-term sequence of linear maps. It records the three morphisms and both consecutive-composition equations together. Exactness is imposed separately by FourTermLinearSequence.IsExact, so the same sequence can be constructed before its exactness proof is available.

Definition CrowellExactSequence.FourTermLinearSequence.IsExact 
def IsExact (S : FourTermLinearSequence R A B C D) : Prop :=
  Function.Injective S.head ∧ Function.Exact S.head S.middle ∧
    Function.Exact S.middle S.tail ∧ Function.Surjective S.tail

A four-term exact sequence, formulated at the function level. This packages injectivity of \(f\), exactness at the two middle terms, and surjectivity of the final map.

Definition CrowellExactSequence.FourTermLinearSequence.ofExact 
def ofExact (f : A →ₗ[R] B) (g : B →ₗ[R] C) (h : C →ₗ[R] D)
    (hexact : Function.Injective f ∧ Function.Exact f g ∧
      Function.Exact g h ∧ Function.Surjective h) :
    FourTermLinearSequence R A B C D where
  head := f
  middle := g
  tail := h
  middle_comp_head := by
    ext x
    have hx : g (f x) = 0 := (hexact.2.1 (f x)).2 ⟨x, rfl⟩
    simpa using hx
  tail_comp_middle := by
    ext x
    have hx : h (g x) = 0 := (hexact.2.2.1 (g x)).2 ⟨x, rfl⟩
    simpa using hx

Bundle three linear maps once their four exactness assertions are known.

Theorem CrowellExactSequence.FourTermLinearSequence.ofExact_isExact 
@[simp]
theorem ofExact_isExact (f : A →ₗ[R] B) (g : B →ₗ[R] C) (h : C →ₗ[R] D)
    (hexact : Function.Injective f ∧ Function.Exact f g ∧
      Function.Exact g h ∧ Function.Surjective h) :
    (ofExact f g h hexact).IsExact

The sequence assembled from exact maps retains the supplied injectivity, exactness, and surjectivity witnesses.

Show Lean proof
Theorem CrowellExactSequence.Function.Exact.linearEquiv_symm_comp_comp 
theorem Function.Exact.linearEquiv_symm_comp_comp
    (e : B ≃ₗ[R] B') {f : A → B'} {g : B' → C}
    (hexact : Function.Exact f g) :
    Function.Exact (fun x : A => e.symm (f x)) (fun y : B => g (e y))

Transport function exactness across a linear equivalence on the middle type.

Show Lean proof
Theorem CrowellExactSequence.Function.Exact.linearEquiv_symm_comp_comp_iff 
theorem Function.Exact.linearEquiv_symm_comp_comp_iff
    (e : B ≃ₗ[R] B') {f : A → B'} {g : B' → C} :
    Function.Exact (fun x : A => e.symm (f x)) (fun y : B => g (e y)) ↔
      Function.Exact f g

Transporting exactness through a linear equivalence is equivalent to composing with the equivalence and its inverse.

Show Lean proof
Theorem CrowellExactSequence.Function.Exact.comp_linearEquiv 
omit [Zero C] in
theorem Function.Exact.comp_linearEquiv
    (e : B ≃ₗ[R] B') {g : B' → C} {h : C → D}
    (hexact : Function.Exact g h) :
    Function.Exact (fun y : B => g (e y)) h

Exactness is preserved when the tail map of an exact pair is composed with a linear equivalence on the middle term.

Show Lean proof
Definition CrowellExactSequence.FourTermLinearSequence.reindexMiddle 
def reindexMiddle (S : FourTermLinearSequence R A B' C D) (e : B ≃ₗ[R] B') :
    FourTermLinearSequence R A B C D where
  head := e.symm.toLinearMap.comp S.head
  middle := S.middle.comp e.toLinearMap
  tail := S.tail
  middle_comp_head := by
    ext x
    have hx := congrArg (fun f : A →ₗ[R] C => f x) S.middle_comp_head
    simpa using hx
  tail_comp_middle := by
    ext x
    have hx := congrArg (fun f : B' →ₗ[R] D => f (e x)) S.tail_comp_middle
    simpa using hx

Reindex the first middle object of a bundled four-term sequence along a linear equivalence. Both adjacent maps are transported together, so their composition-zero equations remain part of the resulting object.

Theorem CrowellExactSequence.FourTermLinearSequence.reindexMiddle_isExact 
theorem reindexMiddle_isExact
    (S : FourTermLinearSequence R A B' C D) (e : B ≃ₗ[R] B')
    (hexact : S.IsExact) : (S.reindexMiddle e).IsExact

Exactness is preserved when the first middle object of a bundled sequence is reindexed by a linear equivalence.

Show Lean proof
Theorem CrowellExactSequence.FourTermLinearSequence.reindexMiddle_isExact_iff 
theorem reindexMiddle_isExact_iff
    (S : FourTermLinearSequence R A B' C D) (e : B ≃ₗ[R] B') :
    (S.reindexMiddle e).IsExact ↔ S.IsExact

Reindexing a middle object does not change whether a bundled sequence is exact.

Show Lean proof