Documentation

Q2Presentation.Induction.Section7RawTowerBridge

The ambient quotient-image bridge for the corrected Section 7 raw tower #

The concrete module file defines

The remaining bridge required by Sec7RawTowerPacket is the first-isomorphism-theorem identification between the image of K in the ambient quotient Y / kernelFrattini K and the intrinsic quotient K / frattini K.

source
def Q2Presentation.Induction.mulEquivMultiplicativeAdditive (G : Type u_1) [Group G] :
G ≃* Multiplicative (Additive G)

The canonical type-synonym multiplicative equivalence G ≃* Multiplicative (Additive G).

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Q2Presentation.Induction.sec7KmodRToImageHom {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) :
    towerMgrp K →* ↥(Subgroup.map (QuotientGroup.mk' (kernelFrattini K)) K.Ksub)

    The quotient map K / Φ(K) -> image(K -> Y / Φ(K)).

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem Q2Presentation.Induction.sec7KmodRToImageHom_mk {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (k : ↥K.Ksub) :
      (sec7KmodRToImageHom chief K) ((QuotientGroup.mk' (frattini ↥K.Ksub)) k) = ⟨(QuotientGroup.mk' (kernelFrattini K)) ↑k, ⋯⟩
      source
      theorem Q2Presentation.Induction.sec7KmodRToImageHom_surjective {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) :
      Function.Surjective ⇑(sec7KmodRToImageHom chief K)

      The map K/Φ(K) -> image(K -> Y/Φ(K)) is surjective by definition of image.

      source
      theorem Q2Presentation.Induction.sec7KmodRToImageHom_injective {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) :
      Function.Injective ⇑(sec7KmodRToImageHom chief K)

      The map K/Φ(K) -> image(K -> Y/Φ(K)) is injective because the ambient kernel on K is exactly the embedded intrinsic Frattini subgroup.

      source
      def Q2Presentation.Induction.sec7KmodRImageEquiv {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) :
      ↥(Subgroup.map (QuotientGroup.mk' (kernelFrattini K)) K.Ksub) ≃* towerMgrp K

      The intrinsic quotient K/Φ(K) is canonically the image of K in the ambient quotient Y/Φ(K).

      Equations
      Instances For
        source
        def Q2Presentation.Induction.sec7KmodRBridge {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) :
        ↥(Subgroup.map (QuotientGroup.mk' (kernelFrattini K)) K.Ksub) ≃* Multiplicative (sec7RawModuleData chief K).M

        The bridge in the exact type required by Sec7RawTowerPacket.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For