Presentation.lean`

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.EilenbergGanea.CWPresentation.base line 18
abbrev OAI.EilenbergGanea.CWPresentation.lifted line 19
instance OAI.EilenbergGanea.CWPresentation.baseOuterConnected line 21
instance OAI.EilenbergGanea.CWPresentation.liftedOuterConnected line 24
theorem OAI.EilenbergGanea.CWPresentation.outer_isFree line 29
Source documentation
The actual collar, not an assumed graph presentation, has free π1.
```
theorem outer_isFree [PathConnectedSpace X] (r : (base hd).outer) :
    IsFreeGroup (FundamentalGroup (base hd).outer r) := by
…
```
Mentions: OAI.EilenbergGanea.CWPresentation.base
abbrev OAI.EilenbergGanea.CWPresentation.root line 53
abbrev OAI.EilenbergGanea.CWPresentation.toTotal line 54
abbrev OAI.EilenbergGanea.CWPresentation.fromLift line 57
def OAI.EilenbergGanea.CWPresentation.liftedKernelEquiv line 63
Source documentation
Closed lifting gives the actual kernel, including all (possibly infinitely many) lifted cells and without a cellular-homology assumption.
```
def liftedKernelEquiv : (FundamentalGroup (lifted cov hd).outer e)ᵐᵒᵖ ≃* (toTotal cov hd e).ker :=
…
```
Mentions: OAI.EilenbergGanea.CWPresentation.lifted, OAI.EilenbergGanea.CWPresentation.toTotal
theorem OAI.EilenbergGanea.CWPresentation.liftedKernelEquiv_val line 67
def OAI.EilenbergGanea.CWPresentation.kernelBasis line 76
theorem OAI.EilenbergGanea.CWPresentation.kernelBasis_single line 81
theorem OAI.EilenbergGanea.CWPresentation.project_annulus line 103
def OAI.EilenbergGanea.CWPresentation.projectedAnchor line 107
def OAI.EilenbergGanea.CWPresentation.projectedRelator line 112
theorem OAI.EilenbergGanea.CWPresentation.projectedRelator_eq line 118
def OAI.EilenbergGanea.CWPresentation.relator line 130
theorem OAI.EilenbergGanea.CWPresentation.relator_mem line 132
theorem OAI.EilenbergGanea.CWPresentation.relator_normalClosure line 138
Source documentation
The selected lifted annuli give an actual presentation of the total π1.
```
theorem relator_normalClosure : (toTotal cov hd e).ker =
    Subgroup.normalClosure (Set.range (relator cov hd e q y₀ hs)) := by
…
```
Mentions: OAI.EilenbergGanea.CWPresentation.toTotal, OAI.EilenbergGanea.CWPresentation.relator
def OAI.EilenbergGanea.CWPresentation.deckEquiv line 167
def OAI.EilenbergGanea.CWPresentation.conjugator line 170
theorem OAI.EilenbergGanea.CWPresentation.relator_conjugate line 176
theorem OAI.EilenbergGanea.CWPresentation.conjugator_value line 184
Source documentation
The group-ring coefficient is exactly the deck translate, not its inverse or an arbitrary permutation. This fixes the traversal/left-action convention.
```
theorem conjugator_value (d : deckGroup p) (j : Cell (X:=X) 2) :
…
```
def OAI.EilenbergGanea.CWPresentation.coefficientIndex line 211
Source documentation
Reindexing the genuine lifted-cell basis by monodromy gives the actual integral basis on G×(base2-cells).
```
def coefficientIndex : (FundamentalGroup X (p e.val))ᵐᵒᵖ × Cell (X:=X) 2 ≃ LiftedCell (p:=p) 2 :=
…
```
def OAI.EilenbergGanea.CWPresentation.conjugateBasis line 215
theorem OAI.EilenbergGanea.CWPresentation.conjugateBasis_single line 221
Source documentation
Every basis column is the literal conjugate of a selected annular relation, with a conjugating word having precisely the specified quotient value.
```
theorem conjugateBasis_single (g : (FundamentalGroup X (p e.val))ᵐᵒᵖ) (j : Cell (X:=X) 2) :
…
```
theorem OAI.EilenbergGanea.CWPresentation.ordinary_boundary_basis line 257
Source documentation
The arbitrary ordinary2-dimensional CW presentation theorem, including the full integral boundary basis of its actual contractible cover. There are no finiteness, countability, local finiteness, or cell-universe restrictions.
```
theorem ordinary_boundary_basis {G : Type v} [Group G] (x : X) (χ₀ : FundamentalGroup X x ≃* G) :
    ∃ (A : Type u) (a : A → G), Function.Surjective (wordValue a) ∧
      ∃ (r : Cell (X:=X) 2 → FreeGroup A), (∀ j, wordValue a (r j) = 1) ∧
…
```
Mentions: OAI.EilenbergGanea.wordValue