OAI/GroupTheory/PolycyclicRecognition/Finiteness/AbelianNormalExteriorFiniteness.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The exterior square of an abelian normal subgroup

The quotient acts by actual conjugation. The cross product is equivariant and, when multiplication by two is injective on the exterior square, embeds this module in second homology. No character-tameness conclusion is asserted.

  1. theorem OAI.PolycyclicRecognition.IntegralRepresentationFinite.of_mono line 19
  2. def OAI.PolycyclicRecognition.abelianKernelConjugationAction line 36
  3. def OAI.PolycyclicRecognition.abelianKernelQuotientConjugationAction line 53
  4. def OAI.PolycyclicRecognition.abelianNormalExteriorAction line 65
  5. def OAI.PolycyclicRecognition.abelianNormalExteriorProduct line 68
  6. theorem OAI.PolycyclicRecognition.abelianNormalExteriorProduct_mono line 79
  7. theorem OAI.PolycyclicRecognition.typeFPInfinity_abelianNormalExterior_finite line 86

    Source documentation

    A concrete necessary finiteness consequence of FP-infinity.

    theorem typeFPInfinity_abelianNormalExterior_finite [Group.FG G]
    [IsMulCommutative (G ⧸ N)] (h : TypeFPInfinity G)
    (h2 : Function.Injective (fun x : ⋀[ℤ]^2 (Additive N) => (2 : ℤ) • x)) :
    IntegralRepresentationFinite (G ⧸ N) (abelianNormalExteriorAction N) := by
…

    Mentions: OAI.PolycyclicRecognition.TypeFPInfinity, OAI.PolycyclicRecognition.IntegralRepresentationFinite, OAI.PolycyclicRecognition.abelianNormalExteriorAction