NYLL
Module

Basic.lean

Nyll.ProCGroups.CrowellExactSequence.Basic
13 declarations indexed from sourceView source ↗

Module documentation

ProCGroups.CrowellExactSequence.Basic

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.

Imports2
Imported by3

Declarations

abbrev

blanchfieldLyndonFiniteFamilyMap

L34 ↗
CrowellExactSequence.blanchfieldLyndonFiniteFamilyMap
Documentation

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

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace CrowellExactSequence
noncomputable section
open scoped BigOperators
open FoxDifferential
section BlanchfieldLyndonFiniteFamilyMap
variable {R : Type*} [Semiring R]
variable {M : Type*} [AddCommMonoid M] [Module R M]
variable {X : Type*} [Fintype X] [DecidableEq X]
Lean source · statement
abbrev blanchfieldLyndonFiniteFamilyMap (generators : X → M) :
    (X → R) →ₗ[R] M
theorem

blanchfieldLyndonFiniteFamilyMap_apply

L43 ↗
CrowellExactSequence.blanchfieldLyndonFiniteFamilyMap_apply
Documentation

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

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace CrowellExactSequence
noncomputable section
open scoped BigOperators
open FoxDifferential
section BlanchfieldLyndonFiniteFamilyMap
variable {R : Type*} [Semiring R]
variable {M : Type*} [AddCommMonoid M] [Module R M]
variable {X : Type*} [Fintype X] [DecidableEq X]
omit [DecidableEq X] in
Lean source · statement
theorem blanchfieldLyndonFiniteFamilyMap_apply (generators : X → M) (x : X → R) :
    blanchfieldLyndonFiniteFamilyMap (R := R) generators x = ∑ i, x i • generators i
theorem

blanchfieldLyndonFiniteFamilyMap_single

L48 ↗
CrowellExactSequence.blanchfieldLyndonFiniteFamilyMap_single
Documentation

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

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace CrowellExactSequence
noncomputable section
open scoped BigOperators
open FoxDifferential
section BlanchfieldLyndonFiniteFamilyMap
variable {R : Type*} [Semiring R]
variable {M : Type*} [AddCommMonoid M] [Module R M]
variable {X : Type*} [Fintype X] [DecidableEq X]
Lean source · statement
theorem blanchfieldLyndonFiniteFamilyMap_single (generators : X → M) (i : X) :
    blanchfieldLyndonFiniteFamilyMap (R := R) generators (Pi.single i 1) = generators i
structure

FourTermLinearSequence

L58 ↗
CrowellExactSequence.FourTermLinearSequence
Documentation

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.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace CrowellExactSequence
noncomputable section
open scoped BigOperators
open FoxDifferential
Lean source · full declaration
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
def

IsExact

L83 ↗
CrowellExactSequence.FourTermLinearSequence.IsExact
Documentation

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.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace CrowellExactSequence
noncomputable section
open scoped BigOperators
open FoxDifferential
namespace FourTermLinearSequence
variable {R A B C D : Type*} [Semiring R]
variable [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [AddCommMonoid D]
variable [Module R A] [Module R B] [Module R C] [Module R D]
Lean source · statement
def IsExact (S : FourTermLinearSequence R A B C D) : Prop
def

ofExact

L89 ↗
CrowellExactSequence.FourTermLinearSequence.ofExact
Documentation

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

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace CrowellExactSequence
noncomputable section
open scoped BigOperators
open FoxDifferential
namespace FourTermLinearSequence
variable {R A B C D : Type*} [Semiring R]
variable [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [AddCommMonoid D]
variable [Module R A] [Module R B] [Module R C] [Module R D]
Lean source · full declaration
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
theorem

ofExact_isExact

L108 ↗
CrowellExactSequence.FourTermLinearSequence.ofExact_isExact
Documentation

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

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace CrowellExactSequence
noncomputable section
open scoped BigOperators
open FoxDifferential
namespace FourTermLinearSequence
variable {R A B C D : Type*} [Semiring R]
variable [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [AddCommMonoid D]
variable [Module R A] [Module R B] [Module R C] [Module R D]
Lean source · statement
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
theorem

linearEquiv_symm_comp_comp

L125 ↗
CrowellExactSequence.Function.Exact.linearEquiv_symm_comp_comp
Documentation

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

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace CrowellExactSequence
noncomputable section
open scoped BigOperators
open FoxDifferential
section LinearEquivTransport
variable {R : Type*} [Semiring R]
variable {A B B' C D : Type*}
variable [AddCommMonoid B] [Module R B]
variable [AddCommMonoid B'] [Module R B']
variable [Zero C] [Zero D]
Lean source · full declaration
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)) := by
  intro y
  constructor
  · intro hy
    rcases (hexact (e y)).1 hy with ⟨x, hx⟩
    exact ⟨x, by simp only [hx, LinearEquiv.symm_apply_apply]⟩
  · rintro ⟨x, hx⟩
    have hxy : f x = e y := by
      have hcongr := congrArg e hx
      simpa using hcongr
    exact (hexact (e y)).2 ⟨x, hxy⟩
theorem

linearEquiv_symm_comp_comp_iff

L144 ↗
CrowellExactSequence.Function.Exact.linearEquiv_symm_comp_comp_iff
Documentation

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

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace CrowellExactSequence
noncomputable section
open scoped BigOperators
open FoxDifferential
section LinearEquivTransport
variable {R : Type*} [Semiring R]
variable {A B B' C D : Type*}
variable [AddCommMonoid B] [Module R B]
variable [AddCommMonoid B'] [Module R B']
variable [Zero C] [Zero D]
Lean source · full declaration
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 := by
  constructor
  · intro hexact
    simpa using
      (Function.Exact.linearEquiv_symm_comp_comp
        (e := e.symm)
        (f := fun x : A => e.symm (f x))
        (g := fun y : B => g (e y))
        hexact)
  · exact Function.Exact.linearEquiv_symm_comp_comp e
theorem

comp_linearEquiv

L163 ↗
CrowellExactSequence.Function.Exact.comp_linearEquiv
Documentation

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

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace CrowellExactSequence
noncomputable section
open scoped BigOperators
open FoxDifferential
section LinearEquivTransport
variable {R : Type*} [Semiring R]
variable {A B B' C D : Type*}
variable [AddCommMonoid B] [Module R B]
variable [AddCommMonoid B'] [Module R B']
variable [Zero C] [Zero D]
omit [Zero C] in
Lean source · full declaration
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 := by
  intro z
  constructor
  · intro hz
    rcases (hexact z).1 hz with ⟨y', hy'⟩
    rcases e.surjective y' with ⟨y, rfl⟩
    exact ⟨y, hy'⟩
  · rintro ⟨y, hy⟩
    exact (hexact z).2 ⟨e y, hy⟩
def

reindexMiddle

L191 ↗
CrowellExactSequence.FourTermLinearSequence.reindexMiddle
Documentation

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.

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace CrowellExactSequence
noncomputable section
open scoped BigOperators
open FoxDifferential
namespace FourTermLinearSequence
variable {R : Type*} [Semiring R]
variable {A B B' C D : Type*}
variable [AddCommMonoid A] [Module R A]
variable [AddCommMonoid B] [Module R B]
variable [AddCommMonoid B'] [Module R B']
variable [AddCommMonoid C] [Module R C]
variable [AddCommMonoid D] [Module R D]
Lean source · full declaration
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
theorem

reindexMiddle_isExact

L207 ↗
CrowellExactSequence.FourTermLinearSequence.reindexMiddle_isExact
Documentation

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

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace CrowellExactSequence
noncomputable section
open scoped BigOperators
open FoxDifferential
namespace FourTermLinearSequence
variable {R : Type*} [Semiring R]
variable {A B B' C D : Type*}
variable [AddCommMonoid A] [Module R A]
variable [AddCommMonoid B] [Module R B]
variable [AddCommMonoid B'] [Module R B']
variable [AddCommMonoid C] [Module R C]
variable [AddCommMonoid D] [Module R D]
Lean source · statement
theorem reindexMiddle_isExact
    (S : FourTermLinearSequence R A B' C D) (e : B ≃ₗ[R] B')
    (hexact : S.IsExact) : (S.reindexMiddle e).IsExact
theorem

reindexMiddle_isExact_iff

L217 ↗
CrowellExactSequence.FourTermLinearSequence.reindexMiddle_isExact_iff
Documentation

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

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace CrowellExactSequence
noncomputable section
open scoped BigOperators
open FoxDifferential
namespace FourTermLinearSequence
variable {R : Type*} [Semiring R]
variable {A B B' C D : Type*}
variable [AddCommMonoid A] [Module R A]
variable [AddCommMonoid B] [Module R B]
variable [AddCommMonoid B'] [Module R B']
variable [AddCommMonoid C] [Module R C]
variable [AddCommMonoid D] [Module R D]
Lean source · statement
theorem reindexMiddle_isExact_iff
    (S : FourTermLinearSequence R A B' C D) (e : B ≃ₗ[R] B') :
    (S.reindexMiddle e).IsExact ↔ S.IsExact

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.