Documentation

Q2Presentation.Induction.TargetKmodRInnerConjugationClosed

Closing target K/R inner conjugation from the realized quotient bridge #

This sidecar tests the Pro-suggested refinement: inner conjugation by an element of K on the realized quotient K/R should be trivial because K/R is identified with the abelian multiplicative group of the additive module M.

source
def Q2Presentation.Induction.TargetKmodRInnerConjugationClosed.kClass {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (k : p.fst.Y) (hk : k ∈ D.Ksub) :
↥(Subgroup.map (QuotientGroup.mk' D.Rsub) D.Ksub)

The class of k : K in the realized quotient K/R.

Equations
Instances For
    source
    theorem Q2Presentation.Induction.TargetKmodRInnerConjugationClosed.quotientConjugateKmodRPoint_eq_kClass_conj {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (k : p.fst.Y) (hk : k ∈ D.Ksub) (q : ↥(Subgroup.map (QuotientGroup.mk' D.Rsub) D.Ksub)) :
    TargetDecorationCanonicalInvarianceProofs.quotientConjugateKmodRPoint B D k q = (kClass B D k hk)⁻¹ * q * kClass B D k hk

    Ambient quotient conjugation by k : K is subgroup inner conjugation by its class in K/R.

    source
    theorem Q2Presentation.Induction.TargetKmodRInnerConjugationClosed.quotientConjugateKmodRPoint_eq_self_of_mem_K {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (k : p.fst.Y) (hk : k ∈ D.Ksub) (q : ↥(Subgroup.map (QuotientGroup.mk' D.Rsub) D.Ksub)) :
    TargetDecorationCanonicalInvarianceProofs.quotientConjugateKmodRPoint B D k q = q

    Since K/R is multiplicatively equivalent to the abelian group Multiplicative B.M, inner conjugation by elements of K is trivial on K/R.

    source
    def Q2Presentation.Induction.TargetKmodRInnerConjugationClosed.innerConjugationData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :
    TargetKmodRSameTowerSemanticClosers.CentralCoverTargetKmodRInnerConjugationData B D

    The current semantic inner-conjugation packet, theorem-level from the realized K/R ~= M bridge.

    Equations
    • ⋯ = ⋯
    Instances For
      source
      theorem Q2Presentation.Induction.centralCover_targetKmodRInnerConjugationData_from_KmodR_bridge {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :
      Nonempty (TargetKmodRSameTowerSemanticClosers.CentralCoverTargetKmodRInnerConjugationData B D)

      Route-ready closure of the target K/R inner-conjugation packet from the realized bridge K/R ~= M.

      source
      theorem Q2Presentation.Induction.centralCover_targetKmodRQuotientActionData_from_sameTowerSemanticClosers_noInnerResidual {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :
      Nonempty (TargetKmodRActionProofs.CentralCoverTargetKmodRQuotientActionData B D)

      Same-tower quotient-action packet with the inner-conjugation residual closed from K/R ~= M.