Documentation

Q2Presentation.Induction.TargetDecorationActualDescentProofs

Actual target-decoration descent proof refinements #

This sidecar strictly narrows the current Section 8 packet centralCover_targetDecorationActualDescentData.

Manuscript anchor: lem:decorationblock. The Frattini-layer descent condition R <= ker(thetaY) is theorem-level from the existing concrete provenance R = Phi(K): any homomorphism from a group to the multiplicative group of an F_2-module kills the Frattini subgroup. The only remaining residual is the compatibility between the abstract C-action B.actM and the canonical descended map on K/R.

source
def Q2Presentation.Induction.TargetDecorationActualDescentProofs.multiplicativeLinearCharacter {E : Type} [AddCommGroup E] [Module (ZMod 2) E] (psi : E →ₗ[ZMod 2] ZMod 2) :
Multiplicative E →* Multiplicative (ZMod 2)

A linear functional on an F_2-module, read as a multiplicative character.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Q2Presentation.Induction.TargetDecorationActualDescentProofs.character_to_zmod2_kernel_isCoatom {G : Type} [Group G] (chi : G →* Multiplicative (ZMod 2)) (hchi : chi ≠ 1) :
    IsCoatom chi.ker

    A nontrivial character to Multiplicative (ZMod 2) has maximal kernel.

    source
    theorem Q2Presentation.Induction.TargetDecorationActualDescentProofs.frattini_le_ker_to_multiplicative_vector {G E : Type} [Group G] [AddCommGroup E] [Module (ZMod 2) E] (f : G →* Multiplicative E) :
    frattini G ≤ f.ker

    Any homomorphism to an elementary multiplicative vector group kills the Frattini subgroup.

    source
    theorem Q2Presentation.Induction.TargetDecorationActualDescentProofs.Rsub_le_thetaY_ker {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :
    D.Rsub ≤ p.fst.thetaY.ker

    The Frattini layer of the actual target tower is killed by the decoration.

    The single residual left by this sidecar #

    source
    structure Q2Presentation.Induction.TargetDecorationActualDescentProofs.CentralCoverTargetDecorationCanonicalInvarianceData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :
    Prop

    Remaining compatibility: the canonical descended decoration map is invariant for the abstract C-action on the realized block K/R ~= M.

    Instances For
      source
      def Q2Presentation.Induction.TargetDecorationActualDescentProofs.actualDescentData_of_canonicalInvariance {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (H : CentralCoverTargetDecorationCanonicalInvarianceData B D) :
      TargetDecorationBlockMapActualProofs.CentralCoverTargetDecorationActualDescentData B D
      Equations
      • ⋯ = ⋯
      Instances For
        source
        axiom Q2Presentation.Induction.centralCover_targetDecorationCanonicalInvarianceData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :
        Nonempty (TargetDecorationActualDescentProofs.CentralCoverTargetDecorationCanonicalInvarianceData B D)

        Strictly smaller residual replacing centralCover_targetDecorationActualDescentData.

        The descent condition R <= ker(thetaY) is now proved in TargetDecorationActualDescentProofs.Rsub_le_thetaY_ker; this residual asks only for invariance of that canonical descended map under the abstract C-action.

        source
        theorem Q2Presentation.Induction.centralCover_targetDecorationActualDescentData_from_canonicalInvariance {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :
        Nonempty (TargetDecorationBlockMapActualProofs.CentralCoverTargetDecorationActualDescentData B D)

        Route-ready replacement for the current actual-descent residual.

        source
        theorem Q2Presentation.Induction.centralCover_targetDecorationBlockMapData_from_canonicalInvariance {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :
        Nonempty (TargetDecorationKernelProofs.CentralCoverTargetDecorationBlockMapData B D)

        Block-map packet reassembled from the single canonical-invariance residual.

        source
        theorem Q2Presentation.Induction.centralCover_targetDecorationKernelData_from_canonicalInvariance {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :
        Nonempty (CentralCoverTargetDecorationKernelData B D)

        Decoration-kernel packet reassembled from the single canonical-invariance residual.

        source
        theorem Q2Presentation.Induction.centralCover_targetCanonicalFramedQuotientData_from_canonicalInvariance {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :
        Nonempty (CentralCoverTargetCanonicalFramedQuotientData B D)

        Canonical framed quotient packet reassembled from the single canonical-invariance residual.