PresentationComparison.lean`

61 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.EilenbergGanea.pathProduct_map line 17
def OAI.EilenbergGanea.pathSpelling line 28
Source documentation
The literal edge word traversed by a generator word. Free reduction of this word is harmless for all nonabelian edge labelings.
```
def pathSpelling (v : S → Γ) (w : FreeGroup S) (g : Γ) : FreeGroup (Γ × S) :=
…
```
theorem OAI.EilenbergGanea.pathSpelling_eval line 31

theorem OAI.EilenbergGanea.pathSpelling_abelianization line 40

Source documentation

Abelianizing the literal edge word gives exactly the integral edge chain.

theorem pathSpelling_abelianization (v : S → Γ) (w : FreeGroup S) (g : Γ) :
    FreeGroup.lift (fun i : Γ × S => Multiplicative.ofAdd (Finsupp.single i (1 : ℤ)))
      (pathSpelling v w g) = Multiplicative.ofAdd (pathChain v w g) := by
…

Mentions: OAI.EilenbergGanea.pathSpelling, OAI.EilenbergGanea.pathChain

theorem OAI.EilenbergGanea.pathChain_pairing line 47
Source documentation
Naturality in the target additive free module; used when projecting to extra generators and when tensoring with a finite quotient.
```
theorem pathChain_pairing {M : Type*} [AddCommGroup M]
    (v : S → Γ) (b : Γ × S → M) (w : FreeGroup S) (g : Γ) :
    Finsupp.linearCombination ℤ b (pathChain v w g) =
      (pathProduct v (fun p s => Multiplicative.ofAdd (b (p,s))) w g).toAdd := by
…
```
Mentions: OAI.EilenbergGanea.pathChain, OAI.EilenbergGanea.pathProduct
def OAI.EilenbergGanea.inverseNormalFactor line 66
theorem OAI.EilenbergGanea.normalFactor_inverse line 69
theorem OAI.EilenbergGanea.exists_normalExpression line 76
Source documentation
Every element of a normal closure admits one finite product of conjugates, including for arbitrary (possibly uncountable) index types.
```
theorem exists_normalExpression (r : R → FreeGroup S) {w : FreeGroup S}
    (hw : w ∈ Subgroup.normalClosure (Set.range r)) :
    ∃ l : List (NormalFactor S R), w = (l.map (normalFactorWord r)).prod := by
…
```
Mentions: OAI.EilenbergGanea.NormalFactor, OAI.EilenbergGanea.normalFactorWord
theorem OAI.EilenbergGanea.su2_mul_distance line 108

theorem OAI.EilenbergGanea.finite_word_control line 118

Source documentation

A finite control set for a word, uniform over all base vertices and all labelings. Both the set and the coefficient are chosen before any quotient.

theorem finite_word_control (v : S → Γ) (w : FreeGroup S) :
    ∃ (P : Finset S) (n : ℕ), ∀ (ε : ℝ), 0 ≤ ε → ∀ (a : Γ → S → SU2),
      (∀ g, ∀ s ∈ P, ‖(a g s : ℍ) - 1‖ ≤ ε) →
      ∀ g, ‖((pathProduct v a w g : SU2) : ℍ) - 1‖ ≤ n * ε := by
…

Mentions: OAI.EilenbergGanea.SU2, OAI.EilenbergGanea.pathProduct

theorem OAI.EilenbergGanea.finite_word_control_universal line 148

Source documentation

A finite control set for a word, uniform over all base vertices and all labelings. Both the set and the coefficient are chosen before any quotient.

theorem finite_word_control_universal (w : FreeGroup S) :
    ∃ (P : Finset S) (n : ℕ), ∀ {D : Type u} [Group D] (v : S → D) (ε : ℝ), 0 ≤ ε → ∀ (a : D → S → SU2),
      (∀ g, ∀ s ∈ P, ‖(a g s : ℍ) - 1‖ ≤ ε) →
      ∀ g, ‖((pathProduct v a w g : SU2) : ℍ) - 1‖ ≤ n * ε := by
…

Mentions: OAI.EilenbergGanea.SU2, OAI.EilenbergGanea.pathProduct

theorem OAI.EilenbergGanea.wordValue_quotient line 184
def OAI.EilenbergGanea.evaluatedNormalFactor line 192
theorem OAI.EilenbergGanea.evaluatedNormalFactor_value line 196
theorem OAI.EilenbergGanea.pathProduct_normalProduct line 206
theorem OAI.EilenbergGanea.quotient_evaluated_counts line 220
Source documentation
Exact translated signed counts are preserved upon passage to every quotient. No flatness, finiteness, or injectivity of the quotient is used.
```
theorem quotient_evaluated_counts (v : S → Γ) (q : Γ →* D)
    (a : D → S → SU2) (l : List (NormalFactor S R)) (ρ : R)
    (hc : (l.map (fun f => normalFactorCount v f 1)).sum = Finsupp.single (1,ρ) 1)
    (g : D) :
    relatorSignedCounts (l.map (fun f => evaluatedNormalFactor (fun s => q (v s)) a f g)) =
      Finsupp.single (g,ρ) 1 := by
…
```
Mentions: OAI.EilenbergGanea.SU2, OAI.EilenbergGanea.NormalFactor, OAI.EilenbergGanea.normalFactorCount, OAI.EilenbergGanea.relatorSignedCounts, OAI.EilenbergGanea.evaluatedNormalFactor

theorem OAI.EilenbergGanea.normalExpression_quadratic line 242

Source documentation

The actual relator expression, evaluated by arbitrary edge labels on a quotient graph, has the uniform quadratic error predicted by its exact chain counts.

theorem normalExpression_quadratic (v : S → Γ) (q : Γ →* D)
    (a : D → S → SU2) (r : R → FreeGroup S)
    (hr : ∀ i, wordValue v (r i) = 1) (z : FreeGroup S)
    (l : List (NormalFactor S R)) (he : z = (l.map (normalFactorWord r)).prod)
    (ρ : R) (hc : (l.map (fun f => normalFactorCount v f 1)).sum =
      Finsupp.single (1,ρ) 1)
    (h ε K : ℝ) (hh : 0 ≤ h) (hε : 0 ≤ ε) (hK : 0 ≤ K)
    (hb : ∀ f ∈ l, ∀ g, ‖((pathProduct (fun s => q (v s)) a (r f.2.1) g : SU2) : ℍ) - 1‖ ≤ h)
    (ha : ∀ f ∈ l, ∀ g, ‖((pathProduct (fun s => q (v s)) a f.1 g : SU2) : ℍ) - 1‖ ≤ K * (ε+h))
    (g : D) :
    ‖((pathProduct (fun s => q (v s)) a z g : SU2) : ℍ) -
      ((pathProduct (fun s => q (v s)) a (r ρ) g : SU2) : ℍ)‖ ≤
…

Mentions: OAI.EilenbergGanea.SU2, OAI.EilenbergGanea.wordValue, OAI.EilenbergGanea.NormalFactor, OAI.EilenbergGanea.normalFactorWord, OAI.EilenbergGanea.normalFactorCount, OAI.EilenbergGanea.pathProduct

theorem OAI.EilenbergGanea.normalFactor_product_distance line 284
theorem OAI.EilenbergGanea.normalProduct_distance line 295
Source documentation
Unlike the quadratic estimate, this linear bound needs no information whatever about the conjugating words. It controls the finitely many auxiliary loop labels before any bound on the conjugators is obtained.
```
theorem normalProduct_distance (v : S → Γ) (a : Γ → S → SU2)
    (r : R → FreeGroup S) (hr : ∀ i, wordValue v (r i) = 1)
    (l : List (NormalFactor S R)) (h : ℝ)
    (hb : ∀ f ∈ l, ∀ g, ‖((pathProduct v a (r f.2.1) g : SU2) : ℍ) - 1‖ ≤ h)
    (g : Γ) :
    ‖((pathProduct v a (l.map (normalFactorWord r)).prod g : SU2) : ℍ) - 1‖ ≤ l.length * h := by
…
```
Mentions: OAI.EilenbergGanea.SU2, OAI.EilenbergGanea.wordValue, OAI.EilenbergGanea.NormalFactor, OAI.EilenbergGanea.pathProduct, OAI.EilenbergGanea.normalFactorWord
theorem OAI.EilenbergGanea.pathProduct_map_alphabet line 321
theorem OAI.EilenbergGanea.finite_word_family_control line 332

theorem OAI.EilenbergGanea.finite_normal_comparison line 363

Source documentation

All constants and all ordinary relators needed by the quadratic estimate are chosen before the group quotient and before the edge labels. The normal expressions are literal finite words, while the ambient alphabets may have any cardinality.

theorem finite_normal_comparison
    (v : S ⊕ T → Γ) (r : Z ⊕ R → FreeGroup (S ⊕ T))
    (hr : ∀ i, wordValue v (r i) = 1) (z : Z → FreeGroup S)
    (lz : Z → List (NormalFactor (S ⊕ T) (Z ⊕ R)))
    (lt : T → List (NormalFactor (S ⊕ T) (Z ⊕ R)))
    (hz : ∀ i, FreeGroup.map Sum.inl (z i) = ((lz i).map (normalFactorWord r)).prod)
    (ht : ∀ t, FreeGroup.of (Sum.inr t) = ((lt t).map (normalFactorWord r)).prod)
    (hc : ∀ i, ((lz i).map (fun f => normalFactorCount v f 1)).sum =
      Finsupp.single (1,Sum.inl i) 1) :
    ∃ (A : Finset R) (C : ℝ), 1 ≤ C ∧
      ∀ {F : Type u} [Group F] (q : Γ →* F) (a : F → S ⊕ T → SU2)
        (ε h : ℝ), 0 ≤ ε → 0 ≤ h →
…

Mentions: OAI.EilenbergGanea.wordValue, OAI.EilenbergGanea.NormalFactor, OAI.EilenbergGanea.normalFactorWord, OAI.EilenbergGanea.normalFactorCount, OAI.EilenbergGanea.SU2

abbrev OAI.EilenbergGanea.BasedChains line 466
def OAI.EilenbergGanea.translateChains line 468
def OAI.EilenbergGanea.quotientChains line 471
theorem OAI.EilenbergGanea.translateChains_single line 474
theorem OAI.EilenbergGanea.quotientChains_single line 478
theorem OAI.EilenbergGanea.translateChains_mul line 482
theorem OAI.EilenbergGanea.translateChains_one line 491
theorem OAI.EilenbergGanea.quotientChains_translate line 498
def OAI.EilenbergGanea.ChainsEquivariant line 508
Source documentation
The elementary equivariance expressing a left integral group-ring map.
```
def ChainsEquivariant (A : BasedChains Γ R →ₗ[ℤ] BasedChains Γ S) : Prop :=
…
```
Mentions: OAI.EilenbergGanea.BasedChains
def OAI.EilenbergGanea.quotientMatrix line 513
Source documentation
Base change of a translation-equivariant matrix, directly on its finitely supported columns. Its definition needs neither finite index sets nor flatness.
```
def quotientMatrix (q : Γ →* F) (A : BasedChains Γ R →ₗ[ℤ] BasedChains Γ S) :
    BasedChains F R →ₗ[ℤ] BasedChains F S :=
…
```
Mentions: OAI.EilenbergGanea.BasedChains
theorem OAI.EilenbergGanea.quotientMatrix_single line 518
theorem OAI.EilenbergGanea.quotientMatrix_equivariant line 524
theorem OAI.EilenbergGanea.quotientMatrix_natural line 535
theorem OAI.EilenbergGanea.quotientMatrix_comp line 548
theorem OAI.EilenbergGanea.quotientMatrix_id line 557
theorem OAI.EilenbergGanea.ChainsEquivariant.symm line 563
def OAI.EilenbergGanea.quotientChainEquiv line 572
Source documentation
Tensoring an isomorphism is an isomorphism. This finite-column proof makes no assertion that the quotient group ring is a flat module.
```
def quotientChainEquiv (q : Γ →* F) (A : BasedChains Γ R ≃ₗ[ℤ] BasedChains Γ S)
    (hA : ChainsEquivariant A.toLinearMap) : BasedChains F R ≃ₗ[ℤ] BasedChains F S where
…
```
Mentions: OAI.EilenbergGanea.BasedChains, OAI.EilenbergGanea.ChainsEquivariant

theorem OAI.EilenbergGanea.nonsingular_minor_of_left_inverse line 598

Source documentation

A finite family with an integral left inverse has a nonzero square minor. Expansion of the alternating determinant avoids a flatness or rationalization assumption, and also covers the empty row family.

theorem nonsingular_minor_of_left_inverse {I J : Type*} [Fintype I] [DecidableEq I] [Fintype J]
    (v : J → I → ℤ) (b : I → J → ℤ)
    (hb : ∀ i, ∑ j, b i j • v j = Pi.single i 1) :
    ∃ e : I → J, Function.Injective e ∧ Matrix.det (fun i k => v (e i) k) ≠ 0 := by
…

theorem OAI.EilenbergGanea.finitely_supported_split_family_minor line 630

Source documentation

The same finite-minor statement for an arbitrary direct sum. All supports are retained, but only the finite union needed by the chosen rows is used.

theorem finitely_supported_split_family_minor {I S : Type*} [Fintype I] [DecidableEq I]
    (v : I → S →₀ ℤ) (B : (S →₀ ℤ) →ₗ[ℤ] (I → ℤ))
    (hB : ∀ i, B (v i) = Pi.single i 1) :
    ∃ e : I → S, Function.Injective e ∧ Matrix.det (fun i j => v i (e j)) ≠ 0 := by
…

theorem OAI.EilenbergGanea.basis_subfamily_minor line 663

Source documentation

Every finite subfamily of an arbitrary integral basis has a nonsingular finite coordinate minor, including when the ambient basis is uncountable.

theorem basis_subfamily_minor {I R S : Type*} [Fintype I] [DecidableEq I]
    (A : (R →₀ ℤ) ≃ₗ[ℤ] (S →₀ ℤ)) (j : I ↪ R) :
    ∃ e : I → S, Function.Injective e ∧
      Matrix.det (fun i k => A (Finsupp.single (j i) 1) (e k)) ≠ 0 := by
…

theorem OAI.EilenbergGanea.pathChain_translate line 681
theorem OAI.EilenbergGanea.pathChain_quotient line 689
def OAI.EilenbergGanea.projectExtraChains line 697
theorem OAI.EilenbergGanea.projectExtraChains_single_left line 703
theorem OAI.EilenbergGanea.projectExtraChains_single_right line 708
theorem OAI.EilenbergGanea.projectExtraChains_translate line 712
theorem OAI.EilenbergGanea.projectExtraChains_quotient line 720
def OAI.EilenbergGanea.extraRelatorMap line 728
theorem OAI.EilenbergGanea.extraRelatorMap_single line 732
theorem OAI.EilenbergGanea.extraRelatorMap_equivariant line 738
theorem OAI.EilenbergGanea.extraRelatorMap_quotientMatrix line 749

theorem OAI.EilenbergGanea.finite_extra_boundary_minor line 761

Source documentation

The exponent minor used on a finite quotient is a consequence of the ordinary projected boundary isomorphism itself; no independent rank hypothesis and no unproved flatness claim is inserted.

theorem finite_extra_boundary_minor {I : Type*} [Fintype I] [DecidableEq I]
    (v : S ⊕ T → Γ) (r : R → FreeGroup (S ⊕ T))
    (A : BasedChains Γ R ≃ₗ[ℤ] BasedChains Γ T)
    (hA : A.toLinearMap = extraRelatorMap v r) (q : Γ →* D) (j : I ↪ D × R) :
    ∃ e : I → D × T, Function.Injective e ∧
      Matrix.det (fun i k => projectExtraChains
        (pathChain (fun s => q (v s)) (r (j i).2) (j i).1) (e k)) ≠ 0 := by
…

Mentions: OAI.EilenbergGanea.BasedChains, OAI.EilenbergGanea.extraRelatorMap, OAI.EilenbergGanea.projectExtraChains, OAI.EilenbergGanea.pathChain

theorem OAI.EilenbergGanea.pathSpelling_exponent line 791
Source documentation
The exponent of a literal edge is exactly its cellular path coefficient.
```
theorem pathSpelling_exponent [DecidableEq F] [DecidableEq S]
    (v : S → F) (w : FreeGroup S) (g : F) (e : F × S) :
    wordExponents (pathSpelling v w g) e = pathChain v w g e := by
…
```
Mentions: OAI.EilenbergGanea.wordExponents, OAI.EilenbergGanea.pathSpelling, OAI.EilenbergGanea.pathChain
theorem OAI.EilenbergGanea.projectExtraChains_apply line 806
Source documentation
Projection to the extra alphabet really deletes only the prescribed edges.
```
theorem projectExtraChains_apply (c : BasedChains F (S ⊕ T)) (e : F × T) :
    projectExtraChains c e = c (e.1, Sum.inr e.2) := by
…
```
Mentions: OAI.EilenbergGanea.BasedChains, OAI.EilenbergGanea.projectExtraChains
theorem OAI.EilenbergGanea.norm_eq_familySize line 818
Source documentation
Sup norm agrees with the zero-normalized supremum, including an empty index.
```
theorem norm_eq_familySize {I : Type*} [Fintype I] (f : I → ℍ) :
    ‖f‖ = familySize (fun i => ‖f i‖) := by
…
```
Mentions: OAI.EilenbergGanea.familySize
theorem OAI.EilenbergGanea.norm_comp_equiv line 827
Source documentation
Reindexing does not change the actual supremum norm of a finite word family.
```
theorem norm_comp_equiv {I J : Type*} [Fintype I] [Fintype J] (e : I ≃ J) (f : J → ℍ) :
    ‖fun i => f (e i)‖ = ‖f‖ := by
…
```

theorem OAI.EilenbergGanea.finite_quotient_comparison_solvable line 845

Source documentation

The full finite quotient step. All coefficients on the prescribed alphabet are retained exactly, not merely up to a small perturbation.

theorem finite_quotient_comparison_solvable
    (v : S ⊕ T → F) (r : Z ⊕ R → FreeGroup (S ⊕ T)) (z : Z → FreeGroup S)
    (A : Finset R) (B : Finset R) (hAB : A ⊆ B)
    (Q : BasedChains F R ≃ₗ[ℤ] BasedChains F T)
    (hQ : Q.toLinearMap = extraRelatorMap v (fun i => r (.inr i)))
    (C δ η : ℝ) (hC : 0 ≤ C) (hδ : 0 < δ) (hη : 0 < η) (hη1 : η < 1)
    (hc₁ : C*(δ+η) < 1/2) (hc₂ : C*η < δ/2)
    (hcomp : ∀ (b : F → S ⊕ T → SU2) (h : ℝ), 0 ≤ h →
      (∀ g s, ‖(b g (.inl s) : ℍ)-1‖ ≤ η) →
      (∀ i ∈ A, ∀ g, pathProduct (H := SU2) v b (r (.inr i)) g = 1) →
…

Mentions: OAI.EilenbergGanea.BasedChains, OAI.EilenbergGanea.extraRelatorMap, OAI.EilenbergGanea.SU2, OAI.EilenbergGanea.pathProduct

theorem OAI.EilenbergGanea.wordValue_map_alphabet line 959

theorem OAI.EilenbergGanea.aligned_presentation_small_transport line 970

Source documentation

The algebraic core of the manuscript's presentation comparison, for an actual aligned presentation. The passage from arbitrary ordinary CW classifying spaces to this presentation is a separate topological obligation.

theorem aligned_presentation_small_transport
    (v : S ⊕ T → Γ) (r : Z ⊕ R → FreeGroup (S ⊕ T)) (z : Z → FreeGroup S)
    (hvT : ∀ t, v (.inr t) = 1)
    (hr : ∀ i, wordValue v (r i) = 1)
    (hz : ∀ i, wordValue (fun s => v (.inl s)) (z i) = 1)
    (hp : (wordValue v).ker = Subgroup.normalClosure (Set.range r))
    (hinj : Function.Injective (relatorChainMap v r))
    (hchain : ∀ i, pathChain v (FreeGroup.map Sum.inl (z i)) 1 = pathChain v (r (.inl i)) 1)
    (Q : BasedChains Γ R ≃ₗ[ℤ] BasedChains Γ T)
    (hQ : Q.toLinearMap = extraRelatorMap v (fun i => r (.inr i))) :
    ∃ η : ℝ, 0 < η ∧ ∀ a : Γ → S → SU2,
      (∀ g s, ‖(a g s : ℍ)-1‖ < η) →
…

Mentions: OAI.EilenbergGanea.wordValue, OAI.EilenbergGanea.relatorChainMap, OAI.EilenbergGanea.pathChain, OAI.EilenbergGanea.BasedChains, OAI.EilenbergGanea.extraRelatorMap, OAI.EilenbergGanea.SU2