OAI/GroupTheory/Kervaire/Reductions.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Kervaire.coefficient_injective_iff line 10

   Source documentation

   The main theorem is exactly the trivial-intersection claim below.

   theorem coefficient_injective_iff {A : Type u} [Group A] (w : WordGroup A) :
       Function.Injective (coefficientMap w) ↔
         ∀ a : A, Monoid.Coprod.inl a ∈ relatorClosure w → a = 1 := by
   …

   Mentions: OAI.Kervaire.WordGroup, OAI.Kervaire.coefficientMap, OAI.Kervaire.relatorClosure

2. def OAI.Kervaire.exponentMod line 26
3. theorem OAI.Kervaire.exponentMod_relator line 30
4. def OAI.Kervaire.cyclicQuotientMap line 36

   Source documentation

   The quotient always surjects onto the expected cyclic exponent quotient.

   def cyclicQuotientMap {A : Type u} [Group A] (w : WordGroup A) :
       RelatorQuotient w →* Multiplicative (ZMod (exponentSum w).natAbs) :=
   …

   Mentions: OAI.Kervaire.WordGroup, OAI.Kervaire.RelatorQuotient, OAI.Kervaire.exponentSum

5. theorem OAI.Kervaire.cyclicQuotientMap_generator line 45
6. theorem OAI.Kervaire.quotient_nontrivial_of_not_unimodular line 51