Documentation

TauCeti.NumberTheory.ClassFieldTheory.Formation.Tate.Corestriction

Corestriction of finite-layer Tate cohomology #

For a restriction of finite normal layers K/E inside K/F, this file defines corestriction

Ĥʳ(Gal(K/E), A^V) ⟶ Ĥʳ(Gal(K/F), A^V)

in every integer degree. The construction uses the canonical identification of the smaller Galois group with the image of its inclusion into the larger one. In positive degrees it is the ordinary cohomological corestriction from TauCeti.NumberTheory.ClassFieldTheory.Formation.Corestriction; in degrees zero and minus one it is induced by the relative norm and inclusion of norm kernels; and in degrees at most minus two it is the covariant map on group homology.

The comparison lemmas below identify each branch with the corresponding established map. They allow consumers to use Tate corestriction without unfolding its integer-degree case split. On representatives, degree zero is the ground-level norm N_{U/U'} : A^{U'} → A^U and degree minus one is the inclusion of norm kernels; in degrees at most minus two corestriction is the covariant map on group homology along the inclusion of Galois groups. These descriptions no longer mention the image subgroup through which the construction passes, and they give functoriality along a tower F ⊆ E ⊆ E' ⊆ K of ground fields in every degree.

Main definitions #

Main results #

References #

source
noncomputable def TauCeti.ClassFieldTheory.LayerRestriction.tateCor {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (F : Formation G) (r : ℤ) :
small.TateH F r ⟶ big.TateH F r

Corestriction between the Tate cohomology groups of finite normal layers, in every integer degree. Positive degrees use ordinary cohomological corestriction, degrees zero and minus one use the low-degree norm descriptions, and lower degrees use group-homological corestriction.

Instances For
    source
    @[simp]
    theorem TauCeti.ClassFieldTheory.LayerRestriction.tateCor_zero {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (F : Formation G) :
    T.tateCor F 0 = CategoryTheory.CategoryStruct.comp (T.tateRangeIso F 0).hom (TateCohomology.H0Cor (big.rep F) T.galHom.range)

    In degree zero, layer Tate corestriction is the range comparison followed by the relative norm map on degree-zero Tate cohomology.

    source
    @[simp]
    theorem TauCeti.ClassFieldTheory.LayerRestriction.tateCor_ofNat_succ {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (F : Formation G) (n : ℕ) :
    T.tateCor F (↑n + 1) = CategoryTheory.CategoryStruct.comp (small.tateHIsoH F (n + 1)).hom (CategoryTheory.CategoryStruct.comp (T.cohomologyCor F (n + 1)) (big.tateHIsoH F (n + 1)).inv)

    In a positive degree, layer Tate corestriction is ordinary cohomological corestriction read through the canonical positive-degree comparisons.

    source
    theorem TauCeti.ClassFieldTheory.LayerRestriction.tateCor_comp_tateHIsoH_hom {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (F : Formation G) (n : ℕ) [NeZero n] :
    CategoryTheory.CategoryStruct.comp (T.tateCor F ↑n) (big.tateHIsoH F n).hom = CategoryTheory.CategoryStruct.comp (small.tateHIsoH F n).hom (T.cohomologyCor F n)

    Positive-degree Tate corestriction commutes with the canonical comparison to ordinary cohomology.

    source
    theorem TauCeti.ClassFieldTheory.LayerRestriction.tateCor_comp_tateHIsoH_hom_assoc {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (F : Formation G) (n : ℕ) [NeZero n] {Z : ModuleCat ℤ} (h : big.H F n ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (T.tateCor F ↑n) (CategoryTheory.CategoryStruct.comp (big.tateHIsoH F n).hom h) = CategoryTheory.CategoryStruct.comp (small.tateHIsoH F n).hom (CategoryTheory.CategoryStruct.comp (T.cohomologyCor F n) h)

    Positive-degree Tate corestriction commutes with the canonical comparison to ordinary cohomology.

    source
    @[simp]
    theorem TauCeti.ClassFieldTheory.LayerRestriction.tateCor_neg_one {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (F : Formation G) :
    T.tateCor F (-1) = CategoryTheory.CategoryStruct.comp (T.tateRangeIso F (-1)).hom (TateCohomology.HNegOneCor (big.rep F) T.galHom.range)

    In degree minus one, layer Tate corestriction is the range comparison followed by inclusion of the subgroup norm kernel into the ambient norm kernel.

    source
    @[simp]
    theorem TauCeti.ClassFieldTheory.LayerRestriction.tateCor_negSucc_succ {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (F : Formation G) (n : ℕ) :
    T.tateCor F (Int.negSucc (n + 1)) = CategoryTheory.CategoryStruct.comp (T.tateRangeIso F (Int.negSucc (n + 1))).hom (TateCohomology.negSuccCor (big.rep F) T.galHom.range.subtype (n + 1))

    In degree -(n+2), layer Tate corestriction is the range comparison followed by the covariant group-homology map in degree n+1.

    source
    theorem TauCeti.ClassFieldTheory.LayerRestriction.tateCor_negSucc_succ_comp_negSuccIso_hom {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (F : Formation G) (n : ℕ) :
    CategoryTheory.CategoryStruct.comp (T.tateCor F (Int.negSucc (n + 1))) (TateCohomology.negSuccIso (big.rep F) (n + 1)).hom = CategoryTheory.CategoryStruct.comp (TateCohomology.negSuccIso (small.rep F) (n + 1)).hom (groupHomology.map T.galHom (T.repIso F).hom (n + 1))

    In degrees at most minus two, layer Tate corestriction is the covariant map on group homology along the inclusion of Galois groups, with the canonical identification of coefficients, read through TauCeti.TateCohomology.negSuccIso.

    source
    theorem TauCeti.ClassFieldTheory.LayerRestriction.tateCor_negSucc_succ_comp_negSuccIso_hom_assoc {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (F : Formation G) (n : ℕ) {Z : ModuleCat ℤ} (h : groupHomology (big.rep F) (n + 1) ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (T.tateCor F (Int.negSucc (n + 1))) (CategoryTheory.CategoryStruct.comp (TateCohomology.negSuccIso (big.rep F) (n + 1)).hom h) = CategoryTheory.CategoryStruct.comp (TateCohomology.negSuccIso (small.rep F) (n + 1)).hom (CategoryTheory.CategoryStruct.comp (groupHomology.map T.galHom (T.repIso F).hom (n + 1)) h)

    In degrees at most minus two, layer Tate corestriction is the covariant map on group homology along the inclusion of Galois groups, with the canonical identification of coefficients, read through TauCeti.TateCohomology.negSuccIso.

    source
    noncomputable def TauCeti.ClassFieldTheory.LayerRestriction.kerNormInclusion {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (F : Formation G) :
    ↥(LinearMap.ker (small.rep F).ρ.norm) →ₗ[ℤ] ↥(LinearMap.ker (big.rep F).ρ.norm)

    The inclusion of norm kernels along a restriction: an element of the top level A^V whose norm for the layer K/E vanishes has vanishing norm for the layer K/F. It moves no element of the ambient module (kerNormInclusion_apply_coe); on representatives, degree -1 corestriction is this inclusion (tateCor_neg_one_HNegOneπ).

    Instances For
      source
      @[simp]
      theorem TauCeti.ClassFieldTheory.LayerRestriction.kerNormInclusion_apply_coe {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (F : Formation G) (x : ↥(LinearMap.ker (small.rep F).ρ.norm)) :
      ↑↑((T.kerNormInclusion F) x) = ↑↑x

      The inclusion of norm kernels moves no element of the ambient module.

      source
      theorem TauCeti.ClassFieldTheory.LayerRestriction.tateCor_neg_one_HNegOneπ {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (F : Formation G) (x : ↥(LinearMap.ker (small.rep F).ρ.norm)) :
      (CategoryTheory.ConcreteCategory.hom (T.tateCor F (-1))) ((CategoryTheory.ConcreteCategory.hom (TateCohomology.HNegOneπ (small.rep F))) x) = (CategoryTheory.ConcreteCategory.hom (TateCohomology.HNegOneπ (big.rep F))) ((T.kerNormInclusion F) x)

      In degree minus one, layer Tate corestriction is the inclusion of norm kernels on representatives.

      source
      theorem TauCeti.ClassFieldTheory.LayerRestriction.tateCor_zero_H0π {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (F : Formation G) (x : ↥(small.rep F).ρ.invariants) :
      (CategoryTheory.ConcreteCategory.hom (T.tateCor F 0)) ((CategoryTheory.ConcreteCategory.hom (TateCohomology.H0π (small.rep F))) x) = (CategoryTheory.ConcreteCategory.hom (TateCohomology.H0π (big.rep F))) ((big.groundLevelEquiv F).symm ((T.groundNorm F) ((small.groundLevelEquiv F) x)))

      In degree zero, layer Tate corestriction is the ground-level norm N_{U/U'} on representatives: the class of an element of the ground level A^{U'} of K/E goes to the class of its norm in the ground level A^U of K/F.

      source
      theorem TauCeti.ClassFieldTheory.LayerRestriction.tateHZeroEquivNormQuotient_tateCor_H0π {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (F : Formation G) (x : ↥(small.rep F).ρ.invariants) :
      (big.tateHZeroEquivNormQuotient F) ((CategoryTheory.ConcreteCategory.hom (T.tateCor F 0)) ((CategoryTheory.ConcreteCategory.hom (TateCohomology.H0π (small.rep F))) x)) = (big.normQuotientMk F) ((T.groundNorm F) ((small.groundLevelEquiv F) x))

      In degree zero, corestriction is the ground-level norm on norm quotients. Read through the identification of degree-zero Tate cohomology with the norm quotient, corestricting the class of an element of the ground level A^{U'} of K/E gives the class of its norm N_{U/U'} in the ground level A^U of K/F.

      source
      theorem TauCeti.ClassFieldTheory.LayerRestriction.tateCor_zeroTateClass {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (F : Formation G) (a : ↥(F.level small.ground)) :
      (CategoryTheory.ConcreteCategory.hom (T.tateCor F 0)) ((small.zeroTateClass F) a) = (big.zeroTateClass F) ((T.groundNorm F) a)

      In degree zero, corestriction is the ground-level norm on zero-dimensional classes. The zero-dimensional Tate class of an element of the ground level A^{U'} of K/E corestricts to the zero-dimensional Tate class of its norm N_{U/U'} in the ground level A^U of K/F.

      Towers #

      source
      theorem TauCeti.ClassFieldTheory.LayerRestriction.tateCor_trans {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {a b c : NormalLayer G} (T : LayerRestriction a b) (T' : LayerRestriction b c) (F : Formation G) (r : ℤ) :
      ⋯.tateCor F r = CategoryTheory.CategoryStruct.comp (T.tateCor F r) (T'.tateCor F r)

      Tate corestriction is functorial along a tower of restrictions, in every integer degree. Corestricting from K/E' to K/E and then to K/F is corestricting from K/E' to K/F.

      Trivial coefficients #

      source
      noncomputable def TauCeti.ClassFieldTheory.LayerRestriction.trivialTateCor {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (r : ℤ) :
      small.TrivialTateH r ⟶ big.TrivialTateH r

      Corestriction on the Tate cohomology of finite normal layers with trivial integral coefficients, in every integer degree. It uses cohomological corestriction in positive degrees, the low-degree norm maps in degrees zero and minus one, and homological corestriction below them.

      Instances For
        source
        @[simp]
        theorem TauCeti.ClassFieldTheory.LayerRestriction.trivialTateCor_zero {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) :
        T.trivialTateCor 0 = CategoryTheory.CategoryStruct.comp (T.trivialTateRangeIso 0).hom (TateCohomology.H0Cor (Rep.trivial ℤ big.Gal ℤ) T.galHom.range)

        In degree zero, trivial-coefficient Tate corestriction is the range comparison followed by the relative norm map.

        source
        theorem TauCeti.ClassFieldTheory.LayerRestriction.trivialTateCor_zero_H0π {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (x : ↥(Rep.trivial ℤ small.Gal ℤ).ρ.invariants) :
        (CategoryTheory.ConcreteCategory.hom (T.trivialTateCor 0)) ((CategoryTheory.ConcreteCategory.hom (TateCohomology.H0π (Rep.trivial ℤ small.Gal ℤ))) x) = (CategoryTheory.ConcreteCategory.hom (TateCohomology.H0π (Rep.trivial ℤ big.Gal ℤ))) ⟨↑T.relativeDegree * ↑x, ⋯⟩

        On an invariant integral representative, degree-zero corestriction multiplies by the relative degree.

        source
        @[simp]
        theorem TauCeti.ClassFieldTheory.LayerRestriction.trivialTateCor_ofNat_succ {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (n : ℕ) :
        T.trivialTateCor (↑n + 1) = CategoryTheory.CategoryStruct.comp (T.trivialTateRangeIso (↑n + 1)).hom (CategoryTheory.CategoryStruct.comp ((TateCohomology.isoGroupCohomology (n + 1)).hom.app (Rep.res T.galHom.range.subtype (Rep.trivial ℤ big.Gal ℤ))) (CategoryTheory.CategoryStruct.comp (groupCohomology.corestriction T.galHom.range (Rep.trivial ℤ big.Gal ℤ) (n + 1)) ((TateCohomology.isoGroupCohomology (n + 1)).inv.app (Rep.trivial ℤ big.Gal ℤ))))

        In a positive degree, trivial-coefficient Tate corestriction is ordinary cohomological corestriction after identifying the smaller Galois group with its image.

        source
        theorem TauCeti.ClassFieldTheory.LayerRestriction.trivialTateCor_comp_isoGroupCohomology_hom {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (n : ℕ) [NeZero n] :
        CategoryTheory.CategoryStruct.comp (T.trivialTateCor ↑n) ((TateCohomology.isoGroupCohomology n).hom.app (Rep.trivial ℤ big.Gal ℤ)) = CategoryTheory.CategoryStruct.comp (T.trivialTateRangeIso ↑n).hom (CategoryTheory.CategoryStruct.comp ((TateCohomology.isoGroupCohomology n).hom.app (Rep.res T.galHom.range.subtype (Rep.trivial ℤ big.Gal ℤ))) (groupCohomology.corestriction T.galHom.range (Rep.trivial ℤ big.Gal ℤ) n))

        Positive-degree trivial-coefficient Tate corestriction commutes with Mathlib's canonical comparison to ordinary cohomology.

        source
        theorem TauCeti.ClassFieldTheory.LayerRestriction.trivialTateCor_comp_isoGroupCohomology_hom_assoc {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (n : ℕ) [NeZero n] {Z : ModuleCat ℤ} (h : (groupCohomology.functor ℤ big.Gal n).obj (Rep.trivial ℤ big.Gal ℤ) ⟶ Z) :
        CategoryTheory.CategoryStruct.comp (T.trivialTateCor ↑n) (CategoryTheory.CategoryStruct.comp ((TateCohomology.isoGroupCohomology n).hom.app (Rep.trivial ℤ big.Gal ℤ)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (T.trivialTateRangeIso ↑n).hom (CategoryTheory.CategoryStruct.comp ((TateCohomology.isoGroupCohomology n).hom.app (Rep.res T.galHom.range.subtype (Rep.trivial ℤ big.Gal ℤ))) (groupCohomology.corestriction T.galHom.range (Rep.trivial ℤ big.Gal ℤ) n))) h

        Positive-degree trivial-coefficient Tate corestriction commutes with Mathlib's canonical comparison to ordinary cohomology.

        source
        @[simp]
        theorem TauCeti.ClassFieldTheory.LayerRestriction.trivialTateCor_neg_one {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) :
        T.trivialTateCor (-1) = CategoryTheory.CategoryStruct.comp (T.trivialTateRangeIso (-1)).hom (TateCohomology.HNegOneCor (Rep.trivial ℤ big.Gal ℤ) T.galHom.range)

        In degree minus one, trivial-coefficient Tate corestriction is the range comparison followed by inclusion of norm kernels.

        source
        @[simp]
        theorem TauCeti.ClassFieldTheory.LayerRestriction.trivialTateCor_negSucc_succ {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (n : ℕ) :
        T.trivialTateCor (Int.negSucc (n + 1)) = CategoryTheory.CategoryStruct.comp (T.trivialTateRangeIso (Int.negSucc (n + 1))).hom (TateCohomology.negSuccCor (Rep.trivial ℤ big.Gal ℤ) T.galHom.range.subtype (n + 1))

        In degree -(n+2), trivial-coefficient Tate corestriction is the range comparison followed by the covariant group-homology map in degree n+1.

        source
        @[simp]
        theorem TauCeti.ClassFieldTheory.LayerRestriction.trivialTateCor_neg_two {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) :
        T.trivialTateCor (-2) = CategoryTheory.CategoryStruct.comp (T.trivialTateRangeIso (-2)).hom (TateCohomology.HNegTwoCor (Rep.trivial ℤ big.Gal ℤ) T.galHom.range.subtype)

        In degree -2, trivial-coefficient Tate corestriction is the range comparison followed by the map on first homology induced by inclusion.