OAI/GroupTheory/Presentation/KernelCycles.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.EilenbergGanea.KernelCycles.Kernel line 18
2. abbrev OAI.EilenbergGanea.KernelCycles.AbKernel line 19
3. def OAI.EilenbergGanea.KernelCycles.kernelChainHom line 21
4. def OAI.EilenbergGanea.KernelCycles.abKernelToCycles line 32
5. theorem OAI.EilenbergGanea.KernelCycles.abKernelToCycles_of line 35
6. def OAI.EilenbergGanea.KernelCycles.bridge line 40
7. theorem OAI.EilenbergGanea.KernelCycles.bridge_one line 46
8. theorem OAI.EilenbergGanea.KernelCycles.bridge_mul line 50
9. theorem OAI.EilenbergGanea.KernelCycles.bridge_inv line 56
10. def OAI.EilenbergGanea.KernelCycles.bridgeAb line 63
11. theorem OAI.EilenbergGanea.KernelCycles.bridgeAb_one line 65
12. theorem OAI.EilenbergGanea.KernelCycles.bridgeAb_mul line 66
13. theorem OAI.EilenbergGanea.KernelCycles.bridgeAb_inv line 72
14. def OAI.EilenbergGanea.KernelCycles.chainsToKernel line 78
15. theorem OAI.EilenbergGanea.KernelCycles.chainsToKernel_single line 81
16. theorem OAI.EilenbergGanea.KernelCycles.chainsToKernel_pathChain line 85
17. theorem OAI.EilenbergGanea.KernelCycles.bridgeAb_kernel line 93
18. theorem OAI.EilenbergGanea.KernelCycles.chains_kernel_inverse line 104
19. def OAI.EilenbergGanea.KernelCycles.anchors line 115
20. theorem OAI.EilenbergGanea.KernelCycles.bridge_chain line 117
21. theorem OAI.EilenbergGanea.KernelCycles.kernel_chains_identity line 124
22. def OAI.EilenbergGanea.KernelCycles.abKernelCycleEquiv line 143

    Source documentation

    The exact integral abelianized-kernel/Cayley-cycle comparison, with its literal Fox/path-chain coefficients. No graph realization is assumed.

    def abKernelCycleEquiv : AbKernel a ≃ₗ[ℤ] cycles a :=
    …

    Mentions: OAI.EilenbergGanea.KernelCycles.AbKernel, OAI.EilenbergGanea.cycles

23. theorem OAI.EilenbergGanea.PresentationAlgebra.boundary_basis_of_free line 161

    Source documentation

    A kernel basis with genuine conjugate coefficients becomes the literal Cayley relator-chain basis after choosing a free generating alphabet.

    theorem boundary_basis_of_free [IsFreeGroup H]
        (hp : φ.ker = Subgroup.normalClosure (Set.range r))
        (B : BasedChains G R ≃ₗ[ℤ] Additive (Abelianization φ.ker))
        (hB : ∀ g j, ∃ k : H, φ k = g ∧ B (Finsupp.single (g,j) 1) =
          Additive.ofMul (Abelianization.of (⟨k*r j*k⁻¹,by
            change φ (k*r j*k⁻¹) = 1
            rw [map_mul,map_mul,map_inv,hr,mul_one,mul_inv_cancel]⟩ : φ.ker))) :
        ∃ (A : Type u) (a : A → G), Function.Surjective (wordValue a) ∧
          ∃ (s : R → FreeGroup A), (∀ j, wordValue a (s j) = 1) ∧
            (wordValue a).ker = Subgroup.normalClosure (Set.range s) ∧
            ∃ E : BasedChains G R ≃ₗ[ℤ] cycles a,
              ∀ c, (E c : BasedChains G A) = relatorChainMap a s c := by
    …

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

24. theorem OAI.EilenbergGanea.PresentationAlgebra.boundary_basis_of_free_target line 238

    Source documentation

    The same literal kernel-basis criterion is invariant under a specified isomorphism of the quotient group. No new presentation is assumed.

    theorem boundary_basis_of_free_target [IsFreeGroup H]
        (hp : φ.ker = Subgroup.normalClosure (Set.range r))
        (B : BasedChains G R ≃ₗ[ℤ] Additive (Abelianization φ.ker))
        (hB : ∀ g j, ∃ k : H, φ k = g ∧ B (Finsupp.single (g,j) 1) =
          Additive.ofMul (Abelianization.of (⟨k*r j*k⁻¹,by
            change φ (k*r j*k⁻¹) = 1
            rw [map_mul,map_mul,map_inv,hr,mul_one,mul_inv_cancel]⟩ : φ.ker)))
        {K : Type*} [Group K] (χ : G ≃* K) :
        ∃ (A : Type u) (a : A → K), Function.Surjective (wordValue a) ∧
          ∃ (s : R → FreeGroup A), (∀ j, wordValue a (s j) = 1) ∧
            (wordValue a).ker = Subgroup.normalClosure (Set.range s) ∧
            ∃ E : BasedChains K R ≃ₗ[ℤ] cycles a,
    …

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