OAI/Topology/EilenbergGanea/Main.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EilenbergGanea.source_no_classifyingSpace_two line 16

   Source documentation

   Exclusion is for arbitrary ordinary2-dimensional classifying CW spaces, not merely finite presentations or cell complexes with finitely many orbits.

   theorem source_no_classifyingSpace_two : ¬ HasClassifyingSpace.{u} SourceGroup 2 := by
   …

   Mentions: OAI.EilenbergGanea.SourceGroup

2. theorem OAI.EilenbergGanea.source_main line 30

   Source documentation

   Source Theorem1.1 for the exact103-cell flag triangulation and its actual Artin height kernel. The last conjunct is polymorphic in the universe of the hypothetical ordinary CW model, with unrestricted numbers of cells.

   Distinct definitions of this name: ComparatorChallenges/EilenbergGanea.lean:113 (same statement text; different proof or body). Qualify references as OAI.EilenbergGanea.source_main@path.

   theorem source_main :
       Group.FG SourceGroup ∧ Group.ResiduallyFinite SourceGroup ∧
       cohomologicalDimension SourceGroup = 2 ∧
       HasClassifyingSpace.{0} SourceGroup 3 ∧
       ¬ HasClassifyingSpace.{u} SourceGroup 2 :=
   …

   Mentions: OAI.EilenbergGanea.SourceGroup