PresentationAlignment.lean`

72 declarations, 0 contain sorry, 0 declared as axioms

Actual word and cycle-basis alignment.

theorem OAI.EilenbergGanea.pathChain_zpow_loop line 15
theorem OAI.EilenbergGanea.realize_relator_chain line 31
Source documentation
Every finitely supported integral relator combination is realized by a finite word in the same normal closure. Surjectivity supplies the finitely many conjugating words; no infinite product of presentation moves occurs.
```
theorem realize_relator_chain (v : S → Γ) (hv : Function.Surjective (wordValue v))
    (r : R → FreeGroup S) (hr : ∀ i, wordValue v (r i) = 1)
    (c : (Γ × R) →₀ ℤ) :
    ∃ w ∈ Subgroup.normalClosure (Set.range r),
      pathChain v w 1 = relatorChainMap v r c := by
…
```
Mentions: OAI.EilenbergGanea.wordValue, OAI.EilenbergGanea.pathChain, OAI.EilenbergGanea.relatorChainMap
theorem OAI.EilenbergGanea.relatorChainMap_equivariant line 60
theorem OAI.EilenbergGanea.normal_relators_trivial line 71
theorem OAI.EilenbergGanea.relatorChainMap_single line 78

theorem OAI.EilenbergGanea.shear_relators line 85

Source documentation

A whole column-finite shear is realized by honest finite relator words, including when the relator alphabets have arbitrary cardinality.

theorem shear_relators (v : S → Γ) (hv : Function.Surjective (wordValue v))
    (r : R → FreeGroup S) (u : I → FreeGroup S)
    (hr : ∀ i, wordValue v (r i) = 1) (hu : ∀ i, wordValue v (u i) = 1)
    (C : BasedChains Γ I →ₗ[ℤ] BasedChains Γ R) (hC : ChainsEquivariant C) :
    ∃ u' : I → FreeGroup S,
      (∀ i, wordValue v (u' i) = 1) ∧
      Subgroup.normalClosure (Set.range r ∪ Set.range u') =
        Subgroup.normalClosure (Set.range r ∪ Set.range u) ∧
      relatorChainMap v u' = relatorChainMap v u + (relatorChainMap v r).comp C := by
…

Mentions: OAI.EilenbergGanea.wordValue, OAI.EilenbergGanea.BasedChains, OAI.EilenbergGanea.ChainsEquivariant, OAI.EilenbergGanea.relatorChainMap

theorem OAI.EilenbergGanea.block_word_alignment line 130

Source documentation

The source's three shears P,Q,P, at the level of relator words rather than merely chain matrices. No infinite product or cardinality restriction.

theorem block_word_alignment (v : S → Γ) (hv : Function.Surjective (wordValue v))
    (r : R → FreeGroup S) (u : I → FreeGroup S)
    (hr : ∀ i, wordValue v (r i) = 1) (hu : ∀ i, wordValue v (u i) = 1)
    (A : BasedChains Γ R ≃ₗ[ℤ] BasedChains Γ I)
    (hA : ChainsEquivariant A.toLinearMap) :
    ∃ (r' : R → FreeGroup S) (u' : I → FreeGroup S),
      (∀ i, wordValue v (r' i) = 1) ∧ (∀ i, wordValue v (u' i) = 1) ∧
      Subgroup.normalClosure (Set.range r' ∪ Set.range u') =
        Subgroup.normalClosure (Set.range r ∪ Set.range u) ∧
      relatorChainMap v r' = -((relatorChainMap v u).comp A.toLinearMap) ∧
      relatorChainMap v u' = (relatorChainMap v r).comp A.symm.toLinearMap := by
…

Mentions: OAI.EilenbergGanea.wordValue, OAI.EilenbergGanea.BasedChains, OAI.EilenbergGanea.ChainsEquivariant, OAI.EilenbergGanea.relatorChainMap

def OAI.EilenbergGanea.edgeBoundary line 171
theorem OAI.EilenbergGanea.edgeBoundary_single line 175
theorem OAI.EilenbergGanea.edgeBoundary_pathChain line 180
abbrev OAI.EilenbergGanea.cycles line 192
theorem OAI.EilenbergGanea.relatorChainMap_boundary line 194
def OAI.EilenbergGanea.relatorCycles line 201
theorem OAI.EilenbergGanea.relatorCycles_coe line 207
theorem OAI.EilenbergGanea.wordValue_substitution line 211
theorem OAI.EilenbergGanea.pathChain_substitution line 221
Source documentation
Naturality of the actual path chain under arbitrary finite-word substitution.
```
theorem pathChain_substitution (v : T → Γ) (f : S → FreeGroup T)
    (w : FreeGroup S) (g : Γ) :
    relatorChainMap v f (pathChain (fun s => wordValue v (f s)) w g) =
      pathChain v (FreeGroup.lift f w) g := by
…
```
Mentions: OAI.EilenbergGanea.relatorChainMap, OAI.EilenbergGanea.pathChain, OAI.EilenbergGanea.wordValue
theorem OAI.EilenbergGanea.relatorChainMap_substitution line 234
theorem OAI.EilenbergGanea.relatorChainMap_of line 242
def OAI.EilenbergGanea.sumChainsEquiv line 255
theorem OAI.EilenbergGanea.sumChainsEquiv_fst line 258
theorem OAI.EilenbergGanea.sumChainsEquiv_snd line 262
theorem OAI.EilenbergGanea.sumChainsEquiv_single_left line 266
theorem OAI.EilenbergGanea.sumChainsEquiv_single_right line 276
theorem OAI.EilenbergGanea.edgeBoundary_sum_trivial line 293
def OAI.EilenbergGanea.cycleSumEquiv line 304
Source documentation
A trivial extra generator contributes an independent free summand to the cycle module, with no cardinality restriction.
```
def cycleSumEquiv (v : S → Γ) :
    cycles (Sum.elim v (fun _ : T => 1)) ≃ₗ[ℤ] cycles v × BasedChains Γ T where
…
```
Mentions: OAI.EilenbergGanea.cycles, OAI.EilenbergGanea.BasedChains
theorem OAI.EilenbergGanea.pathChain_hom line 338
theorem OAI.EilenbergGanea.edgeBoundary_hom line 351
def OAI.EilenbergGanea.wordChainEquiv line 362
Source documentation
An honest free-generator equivalence gives an invertible integral edge-chain map; the path chains, not only their augmented exponent sums, are transported.
```
def wordChainEquiv (v : S → Γ) (w : T → Γ) (e : FreeGroup S ≃* FreeGroup T)
    (he : (wordValue w).comp e.toMonoidHom = wordValue v) :
    BasedChains Γ S ≃ₗ[ℤ] BasedChains Γ T where
…
```
Mentions: OAI.EilenbergGanea.wordValue, OAI.EilenbergGanea.BasedChains
def OAI.EilenbergGanea.wordCycleEquiv line 393
Source documentation
Invertible change of free generators preserves the full cycle module.
```
def wordCycleEquiv (v : S → Γ) (w : T → Γ) (e : FreeGroup S ≃* FreeGroup T)
    (he : (wordValue w).comp e.toMonoidHom = wordValue v) : cycles v ≃ₗ[ℤ] cycles w :=
…
```
Mentions: OAI.EilenbergGanea.wordValue, OAI.EilenbergGanea.cycles
def OAI.EilenbergGanea.eraseExtra line 413
def OAI.EilenbergGanea.unitExtendedRelators line 416
theorem OAI.EilenbergGanea.unitExtendedRelators_trivial line 419
theorem OAI.EilenbergGanea.unitExtension_normalClosure line 434
Source documentation
Adjoining arbitrarily many generators of value one and their unit relators preserves the actual presentation, not merely its abelianization.
```
theorem unitExtension_normalClosure (v : S → Γ) (r : R → FreeGroup S)
    (hp : (wordValue v).ker = Subgroup.normalClosure (Set.range r)) :
    (wordValue (Sum.elim v (fun _ : T => 1))).ker =
      Subgroup.normalClosure (Set.range (unitExtendedRelators r : R ⊕ T → _)) := by
…
```
Mentions: OAI.EilenbergGanea.wordValue, OAI.EilenbergGanea.unitExtendedRelators
theorem OAI.EilenbergGanea.unitExtension_chain line 473
Source documentation
The chain matrix of adjoining unit relators is a block diagonal matrix.
```
theorem unitExtension_chain (v : S → Γ) (r : R → FreeGroup S)
    (c : BasedChains Γ (R ⊕ T)) :
    sumChainsEquiv (relatorChainMap (Sum.elim v (fun _ : T => 1))
      (unitExtendedRelators r) c) =
      (relatorChainMap v r (sumChainsEquiv c).1,(sumChainsEquiv c).2) := by
…
```
Mentions: OAI.EilenbergGanea.BasedChains, OAI.EilenbergGanea.sumChainsEquiv, OAI.EilenbergGanea.relatorChainMap, OAI.EilenbergGanea.unitExtendedRelators
def OAI.EilenbergGanea.unitExtensionBasis line 511
Source documentation
Completely explicit stabilization of a boundary-basis presentation.
```
def unitExtensionBasis (v : S → Γ) (B : BasedChains Γ R ≃ₗ[ℤ] cycles v) :
    BasedChains Γ (R ⊕ T) ≃ₗ[ℤ] cycles (Sum.elim v (fun _ : T => 1)) :=
…
```
Mentions: OAI.EilenbergGanea.BasedChains, OAI.EilenbergGanea.cycles
theorem OAI.EilenbergGanea.unitExtensionBasis_value line 516

theorem OAI.EilenbergGanea.chainBasisCoordinate_equivariant line 530

Source documentation

Equivariance is automatic for an isomorphism whose columns are actual path chains. This derives, rather than assumes, equivariance of its inverse.

theorem chainBasisCoordinate_equivariant (v : S → Γ)
    (r : R → FreeGroup S) (u : T → FreeGroup S)
    (E : BasedChains Γ R ≃ₗ[ℤ] cycles v)
    (B : BasedChains Γ T ≃ₗ[ℤ] cycles v)
    (hE : ∀ c, (E c : BasedChains Γ S) = relatorChainMap v r c)
    (hB : ∀ c, (B c : BasedChains Γ S) = relatorChainMap v u c) :
    ChainsEquivariant (E.trans B.symm).toLinearMap := by
…

Mentions: OAI.EilenbergGanea.BasedChains, OAI.EilenbergGanea.cycles, OAI.EilenbergGanea.relatorChainMap, OAI.EilenbergGanea.ChainsEquivariant

def OAI.EilenbergGanea.nielsenHom line 553
theorem OAI.EilenbergGanea.nielsenHom_of_left line 557
theorem OAI.EilenbergGanea.nielsenHom_of_right line 561
theorem OAI.EilenbergGanea.nielsenHom_left line 566
def OAI.EilenbergGanea.nielsenEquiv line 574
theorem OAI.EilenbergGanea.nielsenEquiv_apply line 590
theorem OAI.EilenbergGanea.nielsen_wordValue line 593
theorem OAI.EilenbergGanea.wordPresentation_transport line 611
def OAI.EilenbergGanea.wordBasisTransport line 633
theorem OAI.EilenbergGanea.wordBasisTransport_value line 639
def OAI.EilenbergGanea.freeGroupCongr line 664
theorem OAI.EilenbergGanea.freeGroupCongr_apply line 670
theorem OAI.EilenbergGanea.wordValue_congr_alphabet line 673
theorem OAI.EilenbergGanea.wordRelators_transport_trivial line 680

theorem OAI.EilenbergGanea.align_generators line 690

Source documentation

Generator change starting with an actual boundary-basis presentation, not with an assumed aligned one.

theorem align_generators (v : S → Γ) (hv : Function.Surjective (wordValue v))
    (a : A → Γ) (ha : Function.Surjective (wordValue a))
    (r : R → FreeGroup A) (hr : ∀ i, wordValue a (r i) = 1)
    (hp : (wordValue a).ker = Subgroup.normalClosure (Set.range r))
    (B : BasedChains Γ R ≃ₗ[ℤ] cycles a)
    (hB : ∀ c, (B c : BasedChains Γ A) = relatorChainMap a r c) :
    ∃ (r' : R ⊕ S → FreeGroup (S ⊕ A))
      (B' : BasedChains Γ (R ⊕ S) ≃ₗ[ℤ] cycles (Sum.elim v (fun _ : A => 1))),
      (∀ i, wordValue (Sum.elim v (fun _ : A => 1)) (r' i) = 1) ∧
      (wordValue (Sum.elim v (fun _ : A => 1))).ker =
        Subgroup.normalClosure (Set.range r') ∧
      ∀ c, (B' c : BasedChains Γ (S ⊕ A)) =
…

Mentions: OAI.EilenbergGanea.wordValue, OAI.EilenbergGanea.BasedChains, OAI.EilenbergGanea.cycles, OAI.EilenbergGanea.relatorChainMap

theorem OAI.EilenbergGanea.relatorChainMap_sum line 757
theorem OAI.EilenbergGanea.sumChains_pathChain_left line 768
theorem OAI.EilenbergGanea.sumChains_relatorMap_left line 784
theorem OAI.EilenbergGanea.sumChains_relatorMap_right line 795
theorem OAI.EilenbergGanea.range_sumElim line 806

theorem OAI.EilenbergGanea.stabilized_alignment line 819

Source documentation

The stabilized three-shear conclusion in exact cycle coordinates. This includes injectivity for the entire new boundary list, even for infinite sets.

theorem stabilized_alignment (v : S → Γ) (hv : Function.Surjective (wordValue v))
    (r : R → FreeGroup S) (z : I → FreeGroup S)
    (hr : ∀ i, wordValue v (r i) = 1) (_hz : ∀ i, wordValue v (z i) = 1)
    (hp : (wordValue v).ker = Subgroup.normalClosure (Set.range r))
    (E : BasedChains Γ R ≃ₗ[ℤ] cycles v) (B : BasedChains Γ I ≃ₗ[ℤ] cycles v)
    (hE : ∀ c, (E c : BasedChains Γ S) = relatorChainMap v r c)
    (hB : ∀ c, (B c : BasedChains Γ S) = relatorChainMap v z c) :
    ∃ (r' : R → FreeGroup (S ⊕ I)) (u' : I → FreeGroup (S ⊕ I)),
      (∀ i, wordValue (Sum.elim v (fun _ : I => 1)) (r' i) = 1) ∧
      (∀ i, wordValue (Sum.elim v (fun _ : I => 1)) (u' i) = 1) ∧
      (wordValue (Sum.elim v (fun _ : I => 1))).ker =
        Subgroup.normalClosure (Set.range (Sum.elim r' u')) ∧
…

Mentions: OAI.EilenbergGanea.wordValue, OAI.EilenbergGanea.BasedChains, OAI.EilenbergGanea.cycles, OAI.EilenbergGanea.relatorChainMap

def OAI.EilenbergGanea.chainIndexEquiv line 890
theorem OAI.EilenbergGanea.chainIndexEquiv_single line 894
theorem OAI.EilenbergGanea.relatorChainMap_reindex line 898
theorem OAI.EilenbergGanea.chainIndexEquiv_pathChain line 907
theorem OAI.EilenbergGanea.chainIndexEquiv_relatorMap line 919
def OAI.EilenbergGanea.alignmentIndexEquiv line 932
Source documentation
Permutation of the stabilized relator indices into distinguished and ordinary blocks, in exactly the order of source (ordinary-diagonal).
```
def alignmentIndexEquiv : I ⊕ (T ⊕ R) ≃ R ⊕ (I ⊕ T) where
…
```
theorem OAI.EilenbergGanea.projectExtraChains_eq_sum_snd line 952
theorem OAI.EilenbergGanea.chainIndexEquiv_sumAssoc line 961
theorem OAI.EilenbergGanea.projectExtraChains_assoc line 977
def OAI.EilenbergGanea.ordinaryBlockEquiv line 983
Source documentation
The ordinary diagonal block (1,-A), without finite-rank assumptions.
```
def ordinaryBlockEquiv (A : BasedChains Γ R ≃ₗ[ℤ] BasedChains Γ I) :
    BasedChains Γ (T ⊕ R) ≃ₗ[ℤ] BasedChains Γ (T ⊕ I) :=
…
```
Mentions: OAI.EilenbergGanea.BasedChains
theorem OAI.EilenbergGanea.ordinaryBlockEquiv_value line 989

theorem OAI.EilenbergGanea.finish_alignment line 1003

Source documentation

Reorder the two stabilization blocks into the distinguished and ordinary lists. The projected ordinary block is exactly (1,-A), not only injective.

theorem finish_alignment
    (v : S → Γ) (z : Z → FreeGroup S)
    (B : BasedChains Γ Z ≃ₗ[ℤ] cycles v)
    (hB : ∀ c, (B c : BasedChains Γ S) = relatorChainMap v z c)
    (A : BasedChains Γ R ≃ₗ[ℤ] BasedChains Γ (Z ⊕ T))
    (r : R → FreeGroup ((S ⊕ T) ⊕ (Z ⊕ T)))
    (u : Z ⊕ T → FreeGroup ((S ⊕ T) ⊕ (Z ⊕ T)))
    (hr : ∀ i, wordValue (Sum.elim (Sum.elim v (fun _ : T => 1)) (fun _ : Z ⊕ T => 1)) (r i) = 1)
    (hu : ∀ i, wordValue (Sum.elim (Sum.elim v (fun _ : T => 1)) (fun _ : Z ⊕ T => 1)) (u i) = 1)
    (hp : (wordValue (Sum.elim (Sum.elim v (fun _ : T => 1)) (fun _ : Z ⊕ T => 1))).ker =
      Subgroup.normalClosure (Set.range (Sum.elim r u)))
    (hinj : Function.Injective (relatorChainMap
…

Mentions: OAI.EilenbergGanea.BasedChains, OAI.EilenbergGanea.cycles, OAI.EilenbergGanea.relatorChainMap, OAI.EilenbergGanea.wordValue

theorem OAI.EilenbergGanea.boundary_basis_presentation_alignment line 1123

Source documentation

Full algebraic alignment. The initial and final presentations are genuine normal-closure presentations. No finiteness of the old generators or of either relator family is required.

theorem boundary_basis_presentation_alignment
    (v : S → Γ) (hv : Function.Surjective (wordValue v))
    (z : Z → FreeGroup S) (hz : ∀ i, wordValue v (z i) = 1)
    (B : BasedChains Γ Z ≃ₗ[ℤ] cycles v)
    (hB : ∀ c, (B c : BasedChains Γ S) = relatorChainMap v z c)
    (a : A → Γ) (ha : Function.Surjective (wordValue a))
    (r : R → FreeGroup A) (hr : ∀ i, wordValue a (r i) = 1)
    (hp : (wordValue a).ker = Subgroup.normalClosure (Set.range r))
    (E : BasedChains Γ R ≃ₗ[ℤ] cycles a)
    (hE : ∀ c, (E c : BasedChains Γ A) = relatorChainMap a r c) :
    ∃ (r' : Z ⊕ (A ⊕ (R ⊕ S)) → FreeGroup (S ⊕ (A ⊕ (Z ⊕ A))))
      (Q : BasedChains Γ (A ⊕ (R ⊕ S)) ≃ₗ[ℤ] BasedChains Γ (A ⊕ (Z ⊕ A))),
…

Mentions: OAI.EilenbergGanea.wordValue, OAI.EilenbergGanea.BasedChains, OAI.EilenbergGanea.cycles, OAI.EilenbergGanea.relatorChainMap

theorem OAI.EilenbergGanea.boundary_basis_small_transport line 1178

Source documentation

Full algebraic content of source Theorem presentation: the only additional input is a genuine arbitrary-alphabet presentation with boundary basis. The separate CW-to-presentation bridge must supply that input; it is not asserted here as a hypothesis of the main result.

theorem boundary_basis_small_transport
    (v : S → Γ) (hv : Function.Surjective (wordValue v))
    (z : Z → FreeGroup S) (hz : ∀ i, wordValue v (z i) = 1)
    (B : BasedChains Γ Z ≃ₗ[ℤ] cycles v)
    (hB : ∀ c, (B c : BasedChains Γ S) = relatorChainMap v z c)
    (a₀ : A → Γ) (ha₀ : Function.Surjective (wordValue a₀))
    (r₀ : R → FreeGroup A) (hr₀ : ∀ i, wordValue a₀ (r₀ i) = 1)
    (hp₀ : (wordValue a₀).ker = Subgroup.normalClosure (Set.range r₀))
    (E : BasedChains Γ R ≃ₗ[ℤ] cycles a₀)
    (hE : ∀ c, (E c : BasedChains Γ A) = relatorChainMap a₀ r₀ c) :
    ∃ η : ℝ, 0 < η ∧ ∀ a : Γ → S → SU2,
      (∀ g s, ‖(a g s : ℍ)-1‖ < η) →
…

Mentions: OAI.EilenbergGanea.wordValue, OAI.EilenbergGanea.BasedChains, OAI.EilenbergGanea.cycles, OAI.EilenbergGanea.relatorChainMap, OAI.EilenbergGanea.SU2