Documentation

Q2Presentation.Induction.TerminalBridgeChi

source
@[reducible, inline]
abbrev Q2Presentation.Induction.TerminalBridge.H2grp (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) :
Type

The common quotient H₂ = Y/(Ñ ⊔ L_Y).

Equations
Instances For
    source
    instance Q2Presentation.Induction.TerminalBridge.instFiniteH2grp (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) :
    Finite (H2grp Yt N)
    source
    theorem Q2Presentation.Induction.TerminalBridge.H2grp_isTwoGroup (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] (hidx : ∃ (k : ℕ), N.index = 2 ^ k) :
    IsPGroup 2 (H2grp Yt N)

    H₂ is a 2-group when Ñ has 2-power index.

    source
    def Q2Presentation.Induction.TerminalBridge.hbar (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] :
    Yt.H →* H2grp Yt N

    The descent h̄ : H →* H₂ along π_Y (ker π_Y = L_Y ≤ Ñ ⊔ L_Y).

    Equations
    Instances For
      source
      @[simp]
      theorem Q2Presentation.Induction.TerminalBridge.hbar_piY (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] (y : Yt.Y) :
      (hbar Yt N) (Yt.piY y) = (QuotientGroup.mk' (N ⊔ Yt.LY)) y
      source
      def Q2Presentation.Induction.TerminalBridge.cMap (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] (F : BoundaryFrame Yt) :
      Ttame ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (H2grp Yt N))

      The profinite-level comparison map c := α ≫ h̄ : 𝕋_tame ⟶ H₂.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem Q2Presentation.Induction.TerminalBridge.cMap_apply (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] (F : BoundaryFrame Yt) (x : ↑Ttame.toProfinite.toTop) :
        (ProfiniteGrp.Hom.hom (cMap Yt N F)) x = (hbar Yt N) ((ProfiniteGrp.Hom.hom F.alpha) x)
        source
        theorem Q2Presentation.Induction.TerminalBridge.cMap_tameTau (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] (hidx : ∃ (k : ℕ), N.index = 2 ^ k) (F : BoundaryFrame Yt) :
        (ProfiniteGrp.Hom.hom (cMap Yt N F)) tameTau = 1

        τ dies: the comparison map kills the tame generator τ.

        The character χ #

        source
        def Q2Presentation.Induction.TerminalBridge.chiExp (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] (hidx : ∃ (k : ℕ), N.index = 2 ^ k) (F : BoundaryFrame Yt) :
        ℕ

        The 2-power annihilator exponent of g := c(σ).

        Equations
        Instances For
          source
          theorem Q2Presentation.Induction.TerminalBridge.chiExp_spec (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] (hidx : ∃ (k : ℕ), N.index = 2 ^ k) (F : BoundaryFrame Yt) :
          (ProfiniteGrp.Hom.hom (cMap Yt N F)) tameSigma ^ 2 ^ chiExp Yt N hidx F = 1
          source
          def Q2Presentation.Induction.TerminalBridge.chiFin (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] (hidx : ∃ (k : ℕ), N.index = 2 ^ k) (F : BoundaryFrame Yt) :
          Multiplicative (ZMod (2 ^ chiExp Yt N hidx F)) →* H2grp Yt N

          The finite cyclic hom C2Pow a →* H₂, generator ↦ g = c(σ), via val.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            theorem Q2Presentation.Induction.TerminalBridge.chiFin_gen (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] (hidx : ∃ (k : ℕ), N.index = 2 ^ k) (F : BoundaryFrame Yt) :
            (chiFin Yt N hidx F) (Multiplicative.ofAdd 1) = (ProfiniteGrp.Hom.hom (cMap Yt N F)) tameSigma
            source
            theorem Q2Presentation.Induction.TerminalBridge.chiFin_zero (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] (hidx : ∃ (k : ℕ), N.index = 2 ^ k) (F : BoundaryFrame Yt) :
            (chiFin Yt N hidx F) (Multiplicative.ofAdd 0) = 1
            source
            def Q2Presentation.Induction.TerminalBridge.chi (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] (hidx : ∃ (k : ℕ), N.index = 2 ^ k) (F : BoundaryFrame Yt) :
            ProfiniteZ2 ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (H2grp Yt N))

            The character χ : ℤ₂ ⟶ H₂.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem Q2Presentation.Induction.TerminalBridge.nu_t_comp_chi (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] (hidx : ∃ (k : ℕ), N.index = 2 ^ k) (F : BoundaryFrame Yt) :
              CategoryTheory.CategoryStruct.comp nu_t (chi Yt N hidx F) = cMap Yt N F

              χ factors the comparison map through ν_t (density on {σ, τ}).

              source
              theorem Q2Presentation.Induction.TerminalBridge.package_comparison (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] (hidx : ∃ (k : ℕ), N.index = 2 ^ k) (F : BoundaryFrame Yt) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) :
              CategoryTheory.CategoryStruct.comp B.tameMap (cMap Yt N F) = CategoryTheory.CategoryStruct.comp B.pro2Map (CategoryTheory.CategoryStruct.comp nu_2 (chi Yt N hidx F))

              The marking discharge: for ANY boundary package the pinned tame comparison equals the pro-2 route through χ — pure package algebra.