OAI/Topology/EilenbergGanea/Dimension.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EilenbergGanea.SeedEncoding.cellEquiv_symm_apply line 13
2. abbrev OAI.EilenbergGanea.sourceVertexOrder line 16
3. theorem OAI.EilenbergGanea.sourceVertexOrder_lt line 23
4. theorem OAI.EilenbergGanea.source_valid_to_index line 26
5. theorem OAI.EilenbergGanea.index_valid_to_source line 35
6. def OAI.EilenbergGanea.sourceLinkContraction line 46

   Source documentation

   Relabeling uses the original seed graph and merely chooses an order on its vertices for the signed integral chain convention.

   noncomputable def sourceLinkContraction (K : SimplicialChains.Contraction SeedChainCertificate.graph) :
       SimplicialChains.Contraction seedGraph :=
   …

   Mentions: OAI.SimplicialChains.Contraction, OAI.EilenbergGanea.SeedChainCertificate.graph

7. theorem OAI.EilenbergGanea.source_valid_length_le line 58
8. theorem OAI.EilenbergGanea.source_cd_eq_two_of_contraction line 63
9. theorem OAI.EilenbergGanea.source_no_boundary_basis_of_contraction line 74

   Source documentation

   The exact remaining geometric interface is not limited to finite or countable presentations. This endpoint excludes any ordinary presentation whose actual integral equivariant cellular boundaries freely span cycles.

   theorem source_no_boundary_basis_of_contraction
       (K : SimplicialChains.Contraction SeedChainCertificate.graph)
       {A R : Type*} (a₀ : A → SourceGroup)
       (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 SourceGroup R ≃ₗ[ℤ] cycles a₀)
       (hE : ∀ c, (E c : BasedChains SourceGroup A) = relatorChainMap a₀ r₀ c) : False := by
   …

   Mentions: OAI.SimplicialChains.Contraction, OAI.EilenbergGanea.SeedChainCertificate.graph, OAI.EilenbergGanea.SourceGroup, OAI.EilenbergGanea.wordValue, OAI.EilenbergGanea.BasedChains, OAI.EilenbergGanea.cycles, OAI.EilenbergGanea.relatorChainMap

10. theorem OAI.EilenbergGanea.source_cohomologicalDimension line 94

    Source documentation

    Literal integral cohomological dimension of the source's fixed group.

    theorem source_cohomologicalDimension : cohomologicalDimension SourceGroup = 2 :=
    …

    Mentions: OAI.EilenbergGanea.SourceGroup

11. theorem OAI.EilenbergGanea.source_no_boundary_basis line 99

    Source documentation

    No arbitrary-alphabet genuine presentation has its relators as an integral basis of Cayley cycles.

    theorem source_no_boundary_basis
        {A R : Type*} (a₀ : A → SourceGroup)
        (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 SourceGroup R ≃ₗ[ℤ] cycles a₀)
        (hE : ∀ c, (E c : BasedChains SourceGroup A) = relatorChainMap a₀ r₀ c) : False :=
    …

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