OAI/GroupTheory/PolycyclicRecognition/Finiteness/NormalExtensionColumnHomology.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The other homology direction of the normal-extension bicomplex

Taking ambient-resolution homology gives the quotient group's actual bar complex with coefficients in derived normal coinvariants. This identifies the second homology page without treating it or its convergence as an input.

  1. def OAI.PolycyclicRecognition.rightCoinvariantsNatTrans line 20
  2. abbrev OAI.PolycyclicRecognition.columnHomologyComplex line 25
  3. def OAI.PolycyclicRecognition.normalExtensionColumnHomologyBarIso line 33
  4. def OAI.PolycyclicRecognition.normalExtensionColumnSecondHomologyIso line 53
  5. def OAI.PolycyclicRecognition.normalExtensionSecondPageIso line 65

    Source documentation

    The canonical second page uses the derived quotient action on normal subgroup homology, independent of the chosen ambient resolution.

    def normalExtensionSecondPageIso
    (P : ProjectiveResolution (trivialIntegral G)) (i j : ℕ) :
    (columnHomologyComplex (normalExtensionBicomplex N P) i).homology j ≅
      groupHomology (normalDerivedHomology N i) j := by
…

    Mentions: OAI.PolycyclicRecognition.trivialIntegral, OAI.PolycyclicRecognition.columnHomologyComplex, OAI.PolycyclicRecognition.normalExtensionBicomplex, OAI.PolycyclicRecognition.normalDerivedHomology