Homological

Results named in Tau Ceti's TauCeti.RepresentationTheory.Homological modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremCorestriction through Shapiro's lemma#

Precomposed with Shapiro's isomorphism Hⁿ(G, Coind_S^G Res_S A) ≅ Hⁿ(S, Res_S A), corestriction is the map induced by the trace Coind_S^G Res_S A ⟶ A, the counit of Rep.coindResAdjunction.

TauCeti.groupCohomology.coindIso_hom_comp_corestriction.{u} {k G : Type u} [CommRing k] [Group G]
  (S : Subgroup G) [S.FiniteIndex] (A : Rep.{u, u, u} k G) (n : ℕ) :
  CategoryTheory.CategoryStruct.comp (groupCohomology.coindIso (Rep.res S.subtype A) n).hom
      (TauCeti.groupCohomology.corestriction S A n) =
    groupCohomology.map (MonoidHom.id G) ((Rep.coindResAdjunction k S).counit.app A) n
Lean

Formalized in Tau Ceti as TauCeti.groupCohomology.coindIso_hom_comp_corestriction.

Other forms

Corestriction through Shapiro's lemma. Formalized in Tau Ceti as TauCeti.groupHomology.indIso_inv_comp_map_counit.

TauCeti.groupHomology.indIso_inv_comp_map_counit.{u} {k G : Type u} [CommRing k] [Group G]
  [DecidableEq G] (S : Subgroup G) (B : Rep.{u, u, u} k G) (n : ℕ) :
  CategoryTheory.CategoryStruct.comp (groupHomology.indIso S (Rep.res S.subtype B) n).inv
      (groupHomology.map (MonoidHom.id G) ((Rep.indResAdjunction k S.subtype).counit.app B) n) =
    groupHomology.map S.subtype (CategoryTheory.CategoryStruct.id (Rep.res S.subtype B)) n

Corestriction through Shapiro's lemma. Formalized in Tau Ceti as TauCeti.groupHomology.indIso_inv_comp_map_counit_assoc.

TauCeti.groupHomology.indIso_inv_comp_map_counit_assoc.{u} {k G : Type u} [CommRing k] [Group G]
  [DecidableEq G] (S : Subgroup G) (B : Rep.{u, u, u} k G) (n : ℕ) {Z : ModuleCat k}
  (h : groupHomology B n ⟶ Z) :
  CategoryTheory.CategoryStruct.comp (groupHomology.indIso S (Rep.res S.subtype B) n).inv
      (CategoryTheory.CategoryStruct.comp
        (groupHomology.map (MonoidHom.id G) ((Rep.indResAdjunction k S.subtype).counit.app B) n)
        h) =
    CategoryTheory.CategoryStruct.comp
      (groupHomology.map S.subtype (CategoryTheory.CategoryStruct.id (Rep.res S.subtype B)) n) h
Sources
LeanTauCeti.groupCohomology.coindIso_hom_comp_corestriction · TauCeti.groupHomology.indIso_inv_comp_map_counit · TauCeti.groupHomology.indIso_inv_comp_map_counit_assoc
Used by 21
Used byHilbert reciprocity · Local reciprocity for the Weil group · TauCeti.ClassFieldTheory.tateTheorem · The global class formation · The global invariant · The global invariant is injective · The Kummer case of global existence (Milne VII, Lemma 9.3) · Hilbert sign prescription (O'Meara 71:19a) · Existence of the Tate module of a finite layer (NSW (5.6.5) and the proof of (7.4.1)) · Local reciprocity for A(L) · The cyclotomic normalization of the local Artin map of a finite extension of ℚ_p · Global existence (Milne VII, Theorem 9.5) · The cyclic Hasse norm theorem · The Hasse principle for Brauer classes, from idele-class H¹ · The Kronecker–Weber theorem · The Kummer case of the second fundamental inequality · The principal ideal theorem for a class formation · The finite level of the generator theorem (NSW, proof of (7.4.1)) · The connecting isomorphism H¹(C_m, T) ≃ H²(C_m, Λ) · The Sylow reduction of Tate's triviality criterion (Milne II 3.10, last paragraph) · The Tate–Nakayama theorem

DefinitionThe degree-one finite-quotient colimit theorem#

H¹(G, M) is the colimit of the finite-level first cohomology groups H¹(G ⧸ U, M^U), through the inflation maps.

TauCeti.ContCohomology.explicitFiniteQuotientColimit1.{u, v} (G : Type u) [Group G]
  [TopologicalSpace G] [IsTopologicalGroup G] (M : Type v) [AddCommGroup M] [DistribMulAction G M]
  [TopologicalSpace M] [IsTopologicalAddGroup M] [DiscreteTopology M] [CompactSpace G]
  [TotallyDisconnectedSpace G] [ContinuousSMul G M] :
  CategoryTheory.Limits.IsColimit (TauCeti.ContCohomology.explicitFiniteQuotientCocone1 G M)
Lean

Formalized in Tau Ceti as TauCeti.ContCohomology.explicitFiniteQuotientColimit1.

Sources
LeanTauCeti.ContCohomology.explicitFiniteQuotientColimit1

DefinitionThe degree-two finite-quotient colimit theorem#

H²(G, M) is the colimit of the finite-level second cohomology groups H²(G ⧸ U, M^U), through the inflation maps.

TauCeti.ContCohomology.explicitFiniteQuotientColimit2.{u, v} (G : Type u) [Group G]
  [TopologicalSpace G] [IsTopologicalGroup G] (M : Type v) [AddCommGroup M] [DistribMulAction G M]
  [TopologicalSpace M] [IsTopologicalAddGroup M] [DiscreteTopology M] [CompactSpace G]
  [TotallyDisconnectedSpace G] [ContinuousSMul G M] :
  CategoryTheory.Limits.IsColimit (TauCeti.ContCohomology.explicitFiniteQuotientCocone2 G M)
Lean

Formalized in Tau Ceti as TauCeti.ContCohomology.explicitFiniteQuotientColimit2.

Sources
LeanTauCeti.ContCohomology.explicitFiniteQuotientColimit2

DefinitionThe degree-zero finite-quotient colimit theorem#

H⁰(G, M) is the colimit of H⁰(G ⧸ U, M^U) over the open normal subgroups, through the inflation maps.

Every transition is an isomorphism, so the system is eventually constant and the whole-group level — where the comparison leg is the equivalence TauCeti.ContCohomology.explicitInfl0Equiv — already computes the colimit.

TauCeti.ContCohomology.explicitFiniteQuotientColimit0.{u, v} (G : Type u) [Group G]
  [TopologicalSpace G] [IsTopologicalGroup G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] :
  CategoryTheory.Limits.IsColimit (TauCeti.ContCohomology.explicitFiniteQuotientCocone0 G M)
Lean

Formalized in Tau Ceti as TauCeti.ContCohomology.explicitFiniteQuotientColimit0.

Sources
LeanTauCeti.ContCohomology.explicitFiniteQuotientColimit0

DefinitionThe finite-quotient colimit theorem in every degree#

For a compact group G and a discrete module M with continuous action, the inflation-and-inclusion cocone exhibits the canonical continuous cohomology Hⁿ(G, M) as the colimit, in TopModuleCat ℤ, of the cohomology groups Hⁿ(G ⧸ U, M^U) of the finite quotients over the open normal subgroups U of G.

TauCeti.ContCohomology.continuousFiniteQuotientColimit.{u} (G : Type u) [Group G]
  [TopologicalSpace G] [IsTopologicalGroup G] (M : Type u) [AddCommGroup M] [TopologicalSpace M]
  [DiscreteTopology M] [DistribMulAction G M] [CompactSpace G] [ContinuousSMul G M] (n : ℕ) :
  CategoryTheory.Limits.IsColimit (TauCeti.ContCohomology.continuousFiniteQuotientCocone G M n)
Lean

Formalized in Tau Ceti as TauCeti.ContCohomology.continuousFiniteQuotientColimit.

Sources
LeanTauCeti.ContCohomology.continuousFiniteQuotientColimit

TheoremThe Mackey double-coset formula in degree one (NSW (1.5.6))#

for an open subgroup U of finite index and any subgroup V, res^G_V ∘ cor^G_U = ∑_{VsU} cor^V_{V ⊓ sUs⁻¹} ∘ (s)_* ∘ res on H¹(U, M), for any choice r of representatives s = r D of the double cosets.

TauCeti.ContCohomology.explicitCor1_mackey.{u, v} (G : Type u) [Group G] (M : Type v)
  [AddCommGroup M] [DistribMulAction G M] (U V : Subgroup G) [U.FiniteIndex]
  (r : DoubleCoset.Quotient ↑V ↑U → G)
  (hr : ∀ (D : DoubleCoset.Quotient ↑V ↑U), DoubleCoset.mk V U (r D) = D) [TopologicalSpace G]
  [IsTopologicalGroup G] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousSMul G M]
  (hU : IsOpen ↑U) (x : TauCeti.ContCohomology.H1 (↥U) M) :
  (TauCeti.ContCohomology.explicitRes1 G M V) ((TauCeti.ContCohomology.explicitCor1 G M U hU) x) =
    ∑ D, (TauCeti.ContCohomology.explicitMackeyTerm1 G M U V hU (r D)) x
Informally uses
Lean

Formalized in Tau Ceti as TauCeti.ContCohomology.explicitCor1_mackey.

Other forms

The Mackey double-coset formula in degree two (NSW (1.5.6)). Formalized in Tau Ceti as TauCeti.ContCohomology.explicitCor2_mackey.

TauCeti.ContCohomology.explicitCor2_mackey.{u, v} (G : Type u) [Group G] (M : Type v)
  [AddCommGroup M] [DistribMulAction G M] (U V : Subgroup G) [U.FiniteIndex]
  (r : DoubleCoset.Quotient ↑V ↑U → G)
  (hr : ∀ (D : DoubleCoset.Quotient ↑V ↑U), DoubleCoset.mk V U (r D) = D) [TopologicalSpace G]
  [IsTopologicalGroup G] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousSMul G M]
  (hU : IsOpen ↑U) (x : TauCeti.ContCohomology.H2 (↥U) M) :
  (TauCeti.ContCohomology.explicitRes2 G M V) ((TauCeti.ContCohomology.explicitCor2 G M U hU) x) =
    ∑ D, (TauCeti.ContCohomology.explicitMackeyTerm2 G M U V hU (r D)) x

The Mackey double-coset formula in degree zero (NSW (1.5.6)). Formalized in Tau Ceti as TauCeti.ContCohomology.explicitCor0_mackey.

TauCeti.ContCohomology.explicitCor0_mackey.{u, v} (G : Type u) [Group G] (M : Type v)
  [AddCommGroup M] [DistribMulAction G M] (U V : Subgroup G) [U.FiniteIndex]
  (r : DoubleCoset.Quotient ↑V ↑U → G)
  (hr : ∀ (D : DoubleCoset.Quotient ↑V ↑U), DoubleCoset.mk V U (r D) = D)
  (m : ↥(TauCeti.ContCohomology.H0 (↥U) M)) :
  (TauCeti.ContCohomology.explicitRes0 G M V) ((TauCeti.ContCohomology.explicitCor0 G M U) m) =
    ∑ D, (TauCeti.ContCohomology.explicitMackeyTerm0 G M U V (r D)) m

The Mackey double-coset formula in every degree (NSW (1.5.6)). Formalized in Tau Ceti as TauCeti.ContinuousCohomology.corestriction_mackey.

TauCeti.ContinuousCohomology.corestriction_mackey.{u} {G : Type u} [Group G] [TopologicalSpace G]
  [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (U V : Subgroup G)
  (M : Type u) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M]
  [ContinuousSMul G M] (hU : IsOpen ↑U) (hV : IsClosed ↑V) [U.FiniteIndex]
  (r : DoubleCoset.Quotient ↑V ↑U → G)
  (hr : ∀ (D : DoubleCoset.Quotient ↑V ↑U), DoubleCoset.mk V U (r D) = D) (n : ℕ) :
  CategoryTheory.CategoryStruct.comp (TauCeti.ContinuousCohomology.corestriction U M hU n)
      (TauCeti.ContinuousCohomology.res V (TauCeti.ofDiscreteModule ℤ G M) n) =
    ∑ D, TauCeti.ContinuousCohomology.mackeyTerm U V M hU hV (r D) n
Sources
LeanTauCeti.ContCohomology.explicitCor1_mackey · TauCeti.ContCohomology.explicitCor2_mackey · TauCeti.ContCohomology.explicitCor0_mackey · TauCeti.ContinuousCohomology.corestriction_mackey
Uses 1 · Used by 1
Statement usesShapiro's lemma in degree one
Used byThe Mackey formula for the degree-one corestriction cochain

TheoremThe Mackey formula for the degree-one corestriction cochain#

At the adapted transversal Subgroup.mackeyTransversal, the restriction to V of the corestriction of a 1-cochain f on U is, on the nose, the sum over the double cosets V \ G / U of the corestrictions, from the Mackey subgroups to V at the canonical transversal, of the conjugates y ↦ s • f (s⁻¹ y s) of f.

TauCeti.ContCohomology.cochainsCor1_mackeyTransversal.{u, v} (G : Type u) [Group G] (M : Type v)
  [AddCommGroup M] [DistribMulAction G M] (U V : Subgroup G) [U.FiniteIndex]
  (r : DoubleCoset.Quotient ↑V ↑U → G)
  (hr : ∀ (D : DoubleCoset.Quotient ↑V ↑U), DoubleCoset.mk V U (r D) = D) (f : ↥U → M) (k : ↥V) :
  (TauCeti.ContCohomology.cochainsCor1 G M U (U.mackeyTransversal V r hr) ⋯) f ↑k =
    ∑ D,
      (TauCeti.ContCohomology.cochainsCor1 (↥V) M ((TauCeti.mackeySubgroup (r D) U V).subgroupOf V)
          Quotient.out ⋯)
        ((TauCeti.ContCohomology.cochainsMap1 (TauCeti.mackeyToH (r D) U V)
            (DistribSMul.toAddMonoidHom M (r D)))
          f)
        k
Lean

Formalized in Tau Ceti as TauCeti.ContCohomology.cochainsCor1_mackeyTransversal.

Other forms

The Mackey formula along a continuous homomorphism (NSW (1.5.6)). Formalized in Tau Ceti as TauCeti.ContCohomology.explicitMap2_explicitCor2_eq_sum.

TauCeti.ContCohomology.explicitMap2_explicitCor2_eq_sum.{u, v, w, z} {G : Type u} {H : Type v}
  [Group G] [Group H] [TopologicalSpace G] [TopologicalSpace H] {M : Type w} {N : Type z}
  [AddCommGroup M] [AddCommGroup N] [DistribMulAction G M] [DistribMulAction H N] (φ : H →ₜ* G)
  (f : M →+ N) (hequiv : ∀ (h : H) (m : M), f (φ h • m) = h • f m) (U : Subgroup G)
  [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousSMul G M] [TopologicalSpace N]
  [IsTopologicalAddGroup N] [ContinuousSMul H N] [IsTopologicalGroup G] [ContinuousMul H]
  (hf : Continuous ⇑f) [U.FiniteIndex] (hU : IsOpen ↑U)
  (r : DoubleCoset.Quotient ↑(↑φ).range ↑U → G)
  (hr : ∀ (D : DoubleCoset.Quotient ↑(↑φ).range ↑U), DoubleCoset.mk (↑φ).range U (r D) = D)
  (ψ : DoubleCoset.Quotient ↑(↑φ).range ↑U → H →ₜ* G)
  (hψ : ∀ (D : DoubleCoset.Quotient ↑(↑φ).range ↑U) (h : H), (ψ D) h = (r D)⁻¹ * φ h * r D)
  (x : TauCeti.ContCohomology.H2 (↥U) M) :
  (TauCeti.ContCohomology.explicitMap2 G M H N φ f hf hequiv)
      ((TauCeti.ContCohomology.explicitCor2 G M U hU) x) =
    ∑ D,
      (TauCeti.ContCohomology.explicitCor2 H N (Subgroup.comap (↑(ψ D)) U) ⋯)
        ((TauCeti.ContCohomology.explicitMap2 (↥U) M (↥(Subgroup.comap (↑(ψ D)) U)) N
            ((ψ D).subgroupComap U) (f.comp (DistribSMul.toAddMonoidHom M (r D))) ⋯ ⋯)
          x)

The Mackey formula for the degree-two corestriction cochain. Formalized in Tau Ceti as TauCeti.ContCohomology.cochainsCor2_mackeyTransversal.

TauCeti.ContCohomology.cochainsCor2_mackeyTransversal.{u, v} (G : Type u) [Group G] (M : Type v)
  [AddCommGroup M] [DistribMulAction G M] (U V : Subgroup G) [U.FiniteIndex]
  (r : DoubleCoset.Quotient ↑V ↑U → G)
  (hr : ∀ (D : DoubleCoset.Quotient ↑V ↑U), DoubleCoset.mk V U (r D) = D) (f : ↥U × ↥U → M)
  (k l : ↥V) :
  (TauCeti.ContCohomology.cochainsCor2 G M U (U.mackeyTransversal V r hr) ⋯) f (↑k, ↑l) =
    ∑ D,
      (TauCeti.ContCohomology.cochainsCor2 (↥V) M ((TauCeti.mackeySubgroup (r D) U V).subgroupOf V)
          Quotient.out ⋯)
        ((TauCeti.ContCohomology.cochainsMap2 (TauCeti.mackeyToH (r D) U V)
            (DistribSMul.toAddMonoidHom M (r D)))
          f)
        (k, l)
Sources
LeanTauCeti.ContCohomology.cochainsCor1_mackeyTransversal · TauCeti.ContCohomology.explicitMap2_explicitCor2_eq_sum · TauCeti.ContCohomology.cochainsCor2_mackeyTransversal
Uses 1 · Used by 4
Proof usesThe Mackey double-coset formula in degree one (NSW (1.5.6))
Used byThe global class formation · The global invariant · The global invariant is injective · The Kronecker–Weber theorem

TheoremNakayama–Rim, Sylow form#

Nakayama–Rim, Sylow form (Serre, Local Fields, IX §§3–5; Rim, Ann. of Math. 69 (1959)). Let k be a commutative ring, G a finite group, and A a representation of G on a projective k-module. Suppose that for each prime p dividing |G| some Sylow p-subgroup P satisfies: p is a unit in k, or pk is a maximal ideal, multiplication by p is injective on A, and H_Tate⁰(P, A) = H_Tate⁻¹(P, A) = 0. Then A is projective over k[G].

Rep.projective_of_isZero_res_sylow.{u} {k G : Type u} [CommRing k] [Group G] [Finite G]
  (A : Rep.{u, u, u} k G) [Module.Projective k ↑A]
  (h :
    ∀ (p : ℕ),
      Nat.Prime p →
        p ∣ Nat.card G →
          ∃ P x,
            IsUnit ↑p ∨
              (Ideal.span {↑p}).IsMaximal ∧
                (∀ (v : ↑A), ↑p • v = 0 → v = 0) ∧
                  CategoryTheory.Limits.IsZero (tateCohomology (Rep.res (↑P).subtype A) 0) ∧
                    CategoryTheory.Limits.IsZero (tateCohomology (Rep.res (↑P).subtype A) (-1))) :
  Module.Projective (MonoidAlgebra k G) A.ρ.asModule
Lean

Formalized in Tau Ceti as Rep.projective_of_isZero_res_sylow.

Other forms

Nakayama–Rim, lattice form. Formalized in Tau Ceti as Rep.projective_of_isZero_res.

Rep.projective_of_isZero_res.{u} {k G : Type u} [CommRing k] [Group G] [Finite G] [IsDomain k]
  [CharZero k] (hk : ∀ (p : ℕ), Nat.Prime p → IsUnit ↑p ∨ (Ideal.span {↑p}).IsMaximal)
  (A : Rep.{u, u, u} k G) [Module.Projective k ↑A]
  (hA :
    ∀ (S : Subgroup G) [inst : Fintype ↥S] (n : ℤ),
      CategoryTheory.Limits.IsZero (tateCohomology (Rep.res S.subtype A) n)) :
  Module.Projective (MonoidAlgebra k G) A.ρ.asModule

Nakayama–Rim: cohomological triviality gives projective dimension at most one. Formalized in Tau Ceti as Rep.projective_ker_of_isZero_res.

Rep.projective_ker_of_isZero_res.{u, u_1} {k G : Type u} [CommRing k] [Group G] [Finite G]
  [IsDomain k] [IsPrincipalIdealRing k] [CharZero k]
  (hk : ∀ (p : ℕ), Nat.Prime p → IsUnit ↑p ∨ (Ideal.span {↑p}).IsMaximal) (A : Rep.{u, u, u} k G)
  (hA :
    ∀ (S : Subgroup G) [inst : Fintype ↥S] (n : ℤ),
      CategoryTheory.Limits.IsZero (tateCohomology (Rep.res S.subtype A) n))
  {P : Type u_1} [AddCommGroup P] [_root_.Module (MonoidAlgebra k G) P]
  [Module.Projective (MonoidAlgebra k G) P] (f : P →ₗ[MonoidAlgebra k G] A.ρ.asModule)
  (hf : Function.Surjective ⇑f) : Module.Projective (MonoidAlgebra k G) ↥f.ker
Sources
LeanRep.projective_of_isZero_res_sylow · Rep.projective_of_isZero_res · Rep.projective_ker_of_isZero_res
Uses 1 · Used by 2
Proof usesSchanuel's lemma in automorphism form
Used byExistence of the Tate module of a finite layer (NSW (5.6.5) and the proof of (7.4.1)) · The Tate–Nakayama theorem

TheoremRestriction through Shapiro's lemma#

For a G-representation B, the map induced by the unit B ⟶ Coind_S^G Res_S B of restriction–coinduction, followed by Shapiro's isomorphism, is restriction Hⁿ(G, B) ⟶ Hⁿ(S, Res_S B).

TauCeti.groupCohomology.map_unit_comp_coindIso_hom.{u} {k G : Type u} [CommRing k] [Group G]
  (S : Subgroup G) (B : Rep.{u, u, u} k G) (n : ℕ) :
  CategoryTheory.CategoryStruct.comp
      (groupCohomology.map (MonoidHom.id G) ((Rep.resCoindAdjunction k S.subtype).unit.app B) n)
      (groupCohomology.coindIso (Rep.res S.subtype B) n).hom =
    groupCohomology.map S.subtype (CategoryTheory.CategoryStruct.id (Rep.res S.subtype B)) n
Lean

Formalized in Tau Ceti as TauCeti.groupCohomology.map_unit_comp_coindIso_hom.

Sources
LeanTauCeti.groupCohomology.map_unit_comp_coindIso_hom
Used by 21
Used byHilbert reciprocity · Local reciprocity for the Weil group · TauCeti.ClassFieldTheory.tateTheorem · The global class formation · The global invariant · The global invariant is injective · The Kummer case of global existence (Milne VII, Lemma 9.3) · Hilbert sign prescription (O'Meara 71:19a) · Existence of the Tate module of a finite layer (NSW (5.6.5) and the proof of (7.4.1)) · Local reciprocity for A(L) · The cyclotomic normalization of the local Artin map of a finite extension of ℚ_p · Global existence (Milne VII, Theorem 9.5) · The cyclic Hasse norm theorem · The Hasse principle for Brauer classes, from idele-class H¹ · The Kronecker–Weber theorem · The Kummer case of the second fundamental inequality · The principal ideal theorem for a class formation · The finite level of the generator theorem (NSW, proof of (7.4.1)) · The connecting isomorphism H¹(C_m, T) ≃ H²(C_m, Λ) · The Sylow reduction of Tate's triviality criterion (Milne II 3.10, last paragraph) · The Tate–Nakayama theorem

TheoremShapiro's isomorphism on an adjunct#

For a G-representation B and a morphism f : Res_S B ⟶ A, the map induced by the adjunct B ⟶ Coind_S^G A of f, followed by Shapiro's isomorphism, is the change-of-group map Hⁿ(G, B) ⟶ Hⁿ(S, A) induced by f along S ≤ G.

TauCeti.groupCohomology.map_resCoindToHom_comp_coindIso_hom.{u} {k G : Type u} [CommRing k]
  [Group G] (S : Subgroup G) (A : Rep.{u, u, u} k ↥S) {B : Rep.{u, u, u} k G}
  (f : Rep.res S.subtype B ⟶ A) (n : ℕ) :
  CategoryTheory.CategoryStruct.comp
      (groupCohomology.map (MonoidHom.id G) (Rep.resCoindToHom S.subtype B A f) n)
      (groupCohomology.coindIso A n).hom =
    groupCohomology.map S.subtype f n
Lean

Formalized in Tau Ceti as TauCeti.groupCohomology.map_resCoindToHom_comp_coindIso_hom.

Sources
LeanTauCeti.groupCohomology.map_resCoindToHom_comp_coindIso_hom
Used by 1
Used byShapiro's lemma in degree one

DefinitionShapiro's lemma in degree one#

Shapiro's lemma in degree one, H¹(G, Coind_U^G A) ≅ H¹(U, A), for a profinite G and a closed subgroup U. The forward map is restriction to U followed by evaluation at 1, and it involves no choice; the continuous section of G → G ⧸ U is used only to prove it bijective.

TauCeti.ContCohomology.explicitShapiro1.{u, v} (G : Type u) [Group G] [TopologicalSpace G]
  [IsTopologicalGroup G] (U : Subgroup G) (A : Type v) [AddCommGroup A] [TopologicalSpace A]
  [DiscreteTopology A] [DistribMulAction (↥U) A] [CompactSpace G] [ContinuousSMul (↥U) A]
  [TotallyDisconnectedSpace G] (hU : IsClosed ↑U) :
  TauCeti.ContCohomology.H1 G (TauCeti.DiscreteCoind G U A) ≃+ TauCeti.ContCohomology.H1 (↥U) A
Lean

Formalized in Tau Ceti as TauCeti.ContCohomology.explicitShapiro1.

Other forms

Shapiro's lemma for Herbrand quotients. Formalized in Tau Ceti as TauCeti.TateCohomology.herbrandQuotient_coind.

TauCeti.TateCohomology.herbrandQuotient_coind.{u} {R G : Type u} [CommRing R] [Group G] [Fintype G]
  [IsCyclic G] (S : Subgroup G) [Fintype ↥S] (A : Rep.{u, u, u} R ↥S) :
  TauCeti.TateCohomology.herbrandQuotient (Rep.coind.{u, u, u, u} S.subtype A) =
    TauCeti.TateCohomology.herbrandQuotient A

Shapiro's lemma for inflated induced representations. Formalized in Tau Ceti as TauCeti.ContinuousCohomology.indInflationShapiroIso.

TauCeti.ContinuousCohomology.indInflationShapiroIso.{u, v} {R : Type v} [CommRing R]
  [TopologicalSpace R] [DiscreteTopology R] {G : Type (max u v)} [Group G] [TopologicalSpace G]
  [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {V : OpenNormalSubgroup G}
  {C : Subgroup (G ⧸ ↑V.toOpenSubgroup)} (B : Rep.{max u v, v, max u v} R ↥C) (n : ℕ) :
  continuousCohomology n
      (TopRep.res (QuotientGroup.mk' ↑V.toOpenSubgroup)
        (TauCeti.discreteTopRep R (G ⧸ ↑V.toOpenSubgroup) (Rep.ind C.subtype B))) ≅
    continuousCohomology n (TauCeti.ContinuousCohomology.comapInflation V C B).obj

Shapiro's lemma for Tate cohomology in positive degrees. Formalized in Tau Ceti as TauCeti.TateCohomology.coindIsoPos.

TauCeti.TateCohomology.coindIsoPos.{u} {R G : Type u} [CommRing R] [Group G] [Fintype G]
  (S : Subgroup G) [Fintype ↥S] (A : Rep.{u, u, u} R ↥S) (n : ℕ) [NeZero n] :
  tateCohomology (Rep.coind.{u, u, u, u} S.subtype A) ↑n ≅ tateCohomology A ↑n

Shapiro's lemma for Tate cohomology of a finite cyclic group. Formalized in Tau Ceti as TauCeti.TateCohomology.coindIso.

TauCeti.TateCohomology.coindIso.{u} {R G : Type u} [CommRing R] [Group G] [Fintype G]
  (S : Subgroup G) [Fintype ↥S] (A : Rep.{u, u, u} R ↥S) [IsCyclic G] (n : ℤ) :
  tateCohomology (Rep.coind.{u, u, u, u} S.subtype A) n ≅ tateCohomology A n

Shapiro's lemma in degree one on the canonical carrier. Formalized in Tau Ceti as TauCeti.ContinuousCohomology.bijective_shapiroMap_one.

TauCeti.ContinuousCohomology.bijective_shapiroMap_one.{u} {G : Type u} [Group G]
  [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (A : Type u) [AddCommGroup A]
  [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction (↥U) A] [CompactSpace G]
  [ContinuousSMul (↥U) A] [TotallyDisconnectedSpace G] (hU : IsClosed ↑U) :
  Function.Bijective
    ⇑(CategoryTheory.ConcreteCategory.hom (TauCeti.ContinuousCohomology.shapiroMap U A 1))

Shapiro's lemma in degree two. Formalized in Tau Ceti as TauCeti.ContCohomology.explicitShapiro2.

TauCeti.ContCohomology.explicitShapiro2.{u, v} (G : Type u) [Group G] [TopologicalSpace G]
  [IsTopologicalGroup G] (U : Subgroup G) (A : Type v) [AddCommGroup A] [DistribMulAction (↥U) A]
  [TopologicalSpace A] [DiscreteTopology A] [CompactSpace G] [ContinuousSMul (↥U) A]
  [TotallyDisconnectedSpace G] (hU : IsClosed ↑U) :
  TauCeti.ContCohomology.H2 G (TauCeti.DiscreteCoind G U A) ≃+ TauCeti.ContCohomology.H2 (↥U) A

Shapiro's lemma in degree two on the canonical carrier. Formalized in Tau Ceti as TauCeti.ContinuousCohomology.bijective_shapiroMap_two.

TauCeti.ContinuousCohomology.bijective_shapiroMap_two.{u} {G : Type u} [Group G]
  [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (A : Type u) [AddCommGroup A]
  [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction (↥U) A] [CompactSpace G]
  [ContinuousSMul (↥U) A] [TotallyDisconnectedSpace G] (hU : IsClosed ↑U) :
  Function.Bijective
    ⇑(CategoryTheory.ConcreteCategory.hom (TauCeti.ContinuousCohomology.shapiroMap U A 2))

Shapiro's lemma in degree zero, H⁰(G, Coind_U^G A) ≅ H⁰(U, A), by evaluation at 1. Formalized in Tau Ceti as TauCeti.ContCohomology.explicitShapiro0.

TauCeti.ContCohomology.explicitShapiro0.{u, v} (G : Type u) [Group G] [TopologicalSpace G]
  (U : Subgroup G) (A : Type v) [AddCommGroup A] [DistribMulAction (↥U) A]
  [SeparatelyContinuousMul G] :
  ↥(TauCeti.ContCohomology.H0 G (TauCeti.DiscreteCoind G U A)) ≃+
    ↥(TauCeti.ContCohomology.H0 (↥U) A)

Shapiro's lemma in degree zero on the canonical carrier. Formalized in Tau Ceti as TauCeti.ContinuousCohomology.bijective_shapiroMap_zero.

TauCeti.ContinuousCohomology.bijective_shapiroMap_zero.{u} {G : Type u} [Group G]
  [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (A : Type u) [AddCommGroup A]
  [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction (↥U) A] :
  Function.Bijective
    ⇑(CategoryTheory.ConcreteCategory.hom (TauCeti.ContinuousCohomology.shapiroMap U A 0))

Shapiro's lemma in degrees at most two on the canonical carrier, in one statement. Formalized in Tau Ceti as TauCeti.ContinuousCohomology.bijective_shapiroMap_of_le_two.

TauCeti.ContinuousCohomology.bijective_shapiroMap_of_le_two.{u} {G : Type u} [Group G]
  [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (A : Type u) [AddCommGroup A]
  [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction (↥U) A] [CompactSpace G]
  [ContinuousSMul (↥U) A] [TotallyDisconnectedSpace G] (hU : IsClosed ↑U) {n : ℕ} (hn : n ≤ 2) :
  Function.Bijective
    ⇑(CategoryTheory.ConcreteCategory.hom (TauCeti.ContinuousCohomology.shapiroMap U A n))

Shapiro's lemma in every degree. Formalized in Tau Ceti as TauCeti.ContinuousCohomology.bijective_shapiroMap.

TauCeti.ContinuousCohomology.bijective_shapiroMap.{u} {G : Type u} [Group G] [TopologicalSpace G]
  [IsTopologicalGroup G] [CompactSpace G] (U : Subgroup G) [TotallyDisconnectedSpace G]
  (hU : IsClosed ↑U) (A : Type u) [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A]
  [DistribMulAction (↥U) A] [ContinuousSMul (↥U) A] (n : ℕ) :
  Function.Bijective
    ⇑(CategoryTheory.ConcreteCategory.hom (TauCeti.ContinuousCohomology.shapiroMap U A n))

Shapiro's lemma in every degree, as an isomorphism of TopModuleCat ℤ. Formalized in Tau Ceti as TauCeti.ContinuousCohomology.isIso_shapiroMap.

TauCeti.ContinuousCohomology.isIso_shapiroMap.{u} {G : Type u} [Group G] [TopologicalSpace G]
  [IsTopologicalGroup G] [CompactSpace G] (U : Subgroup G) [TotallyDisconnectedSpace G]
  (hU : IsClosed ↑U) (A : Type u) [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A]
  [DistribMulAction (↥U) A] [ContinuousSMul (↥U) A] (n : ℕ) :
  CategoryTheory.IsIso (TauCeti.ContinuousCohomology.shapiroMap U A n)

Shapiro's lemma in every degree, on cochains. Formalized in Tau Ceti as TauCeti.ContinuousCohomology.quasiIso_shapiroCochainMap.

TauCeti.ContinuousCohomology.quasiIso_shapiroCochainMap.{u} {G : Type u} [Group G]
  [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (U : Subgroup G)
  [TotallyDisconnectedSpace G] (hU : IsClosed ↑U) (A : Type u) [AddCommGroup A] [TopologicalSpace A]
  [DiscreteTopology A] [DistribMulAction (↥U) A] [ContinuousSMul (↥U) A] :
  QuasiIso (TauCeti.ContinuousCohomology.shapiroCochainMap U A)

Shapiro's lemma on cochains for smooth discrete representations over any ring. Formalized in Tau Ceti as TauCeti.ContinuousCohomology.quasiIso_shapiroCochainMapTopRep.

TauCeti.ContinuousCohomology.quasiIso_shapiroCochainMapTopRep.{u, v} {R : Type v} [Ring R]
  [TopologicalSpace R] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] (U : Subgroup G) [TotallyDisconnectedSpace G] (hU : IsClosed ↑U)
  (A : TauCeti.SmoothDiscreteTopRep R ↥U) :
  QuasiIso (TauCeti.ContinuousCohomology.shapiroCochainMapTopRep U A)

Shapiro's lemma through an identification of the subgroup. Formalized in Tau Ceti as groupCohomology.map_id_eq_zero_iff_of_comp_eq_resCoindToHom.

groupCohomology.map_id_eq_zero_iff_of_comp_eq_resCoindToHom.{u} {k G : Type u} [CommRing k]
  [Group G] (S : Subgroup G) {Γ : Type u} [Group Γ] {X M : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k Γ} {f : ↥S →* Γ} (hf : Function.Bijective ⇑f) {r : Γ →* G}
  (hr : ∀ (s : ↥S), r (f s) = ↑s) (φ : Rep.res r X ⟶ B) (ψ : Rep.res S.subtype X ⟶ Rep.res f B)
  (hψ : (Rep.Hom.hom ψ).toLinearMap = (Rep.Hom.hom φ).toLinearMap) (u : X ⟶ M)
  (e : M ≅ Rep.coind.{u, u, u, u} S.subtype (Rep.res f B))
  (hu : CategoryTheory.CategoryStruct.comp u e.hom = Rep.resCoindToHom S.subtype X (Rep.res f B) ψ)
  (n : ℕ) (x : ↑(groupCohomology X n)) :
  (CategoryTheory.ConcreteCategory.hom (groupCohomology.map (MonoidHom.id G) u n)) x = 0 ↔
    (CategoryTheory.ConcreteCategory.hom (groupCohomology.map r φ n)) x = 0
Sources
LeanTauCeti.ContCohomology.explicitShapiro1 · TauCeti.TateCohomology.herbrandQuotient_coind · TauCeti.ContinuousCohomology.indInflationShapiroIso · TauCeti.TateCohomology.coindIsoPos · TauCeti.TateCohomology.coindIso · TauCeti.ContinuousCohomology.bijective_shapiroMap_one · TauCeti.ContCohomology.explicitShapiro2 · TauCeti.ContinuousCohomology.bijective_shapiroMap_two · TauCeti.ContCohomology.explicitShapiro0 · TauCeti.ContinuousCohomology.bijective_shapiroMap_zero · TauCeti.ContinuousCohomology.bijective_shapiroMap_of_le_two · TauCeti.ContinuousCohomology.bijective_shapiroMap · TauCeti.ContinuousCohomology.isIso_shapiroMap · TauCeti.ContinuousCohomology.quasiIso_shapiroCochainMap · TauCeti.ContinuousCohomology.quasiIso_shapiroCochainMapTopRep · groupCohomology.map_id_eq_zero_iff_of_comp_eq_resCoindToHom
Uses 1 · Used by 36
Proof usesShapiro's isomorphism on an adjunct
Used byThe global class formation · The global invariant · The global invariant is injective · The Kummer case of global existence (Milne VII, Lemma 9.3) · The local class formation · Hilbert sign prescription (O'Meara 71:19a) · Demushkin's theorem · Existence of the Tate module of a finite layer (NSW (5.6.5) and the proof of (7.4.1)) · Shafarevich's theorem · The generator rank of a local absolute Galois group (NSW (7.4.1)) · The marked presentation of G_{ℚ₂}(2) · The marked presentation of G_{ℚ₂(√-2)}(2) · The relative Stiefel–Whitney formula in degree two, on the trace forms themselves (Kahn, Théorème 2 in degree two) · Local Tate duality in degree one · Modular-Artin reduction of the local Euler characteristic formula · Perfect local Tate duality in mixed characteristic · Shapiro's lemma for the normalized order · Tate's duality on an open subgroup acting trivially on μₙ · Tate's local Euler characteristic formula · The cyclic Hasse norm theorem · The Euler characteristic formula and G₀ · The Hasse principle for Brauer classes, from idele-class H¹ · The Kronecker–Weber theorem · The Kummer case of the second fundamental inequality · The finite level of the generator theorem (NSW, proof of (7.4.1)) · TauCeti.cyclicTwoCohomPolynomialEquiv · The index-two corestriction--cup sequence is exact in every degree · The strict cohomological dimension through integral coefficients (NSW (3.3.4)), as vanishing predicates · The Mackey double-coset formula in degree one (NSW (1.5.6)) · Tate's criterion for the cohomological dimension of a pro-p group · The three-term Euler formula · The three-term Euler identity under cd_p G ≤ 2 · The two-term Euler formula · An open subgroup of an infinite Demushkin group is Demushkin (Serre's exposé, §9.2) · The isomorphism type of an open subgroup of a Demushkin group · The pro-p Nielsen–Schreier theorem

TheoremThe Sylow reduction of Tate's triviality criterion (Milne II 3.10, last paragraph)#

if, for every prime p dividing the order of G, Hⁿ⁺¹(P, A) = 0 for some Sylow p-subgroup P, then Hⁿ⁺¹(G, A) = 0.

TauCeti.groupCohomology.isZero_of_isZero_sylow.{u} {k G : Type u} [CommRing k] [Group G] [Finite G]
  (A : Rep.{u, u, u} k G) (n : ℕ)
  (h :
    ∀ (p : ℕ) [Fact (Nat.Prime p)],
      p ∣ Nat.card G →
        ∃ P, CategoryTheory.Limits.IsZero (groupCohomology (Rep.res (↑P).subtype A) (n + 1))) :
  CategoryTheory.Limits.IsZero (groupCohomology A (n + 1))
Lean

Formalized in Tau Ceti as TauCeti.groupCohomology.isZero_of_isZero_sylow.

Sources
LeanTauCeti.groupCohomology.isZero_of_isZero_sylow
Uses 2 · Used by 7
Proof usesCorestriction through Shapiro's lemma · Restriction through Shapiro's lemma
Used byThe global class formation · The global invariant · The global invariant is injective · The cyclic Hasse norm theorem · The Hasse principle for Brauer classes, from idele-class H¹ · The Kronecker–Weber theorem · Tate's cohomological triviality criterion (Milne II 3.10)

TheoremTate's cohomological triviality criterion (Milne II 3.10)#

Let G be a finite group and A a representation of G. If its Tate cohomology vanishes in degrees q and q + 1 for every subgroup S of G of prime-power order, then it vanishes in degree n for every subgroup S of G and every integer n.

TauCeti.TateCohomology.isZero_of_forall_isPGroup.{u} {k G : Type u} [CommRing k] [Group G]
  [Finite G] (A : Rep.{u, u, u} k G) {q : ℤ}
  (h₁ :
    ∀ (p : ℕ) [Fact (Nat.Prime p)] (S : Subgroup G) [inst : Fintype ↥S],
      IsPGroup p ↥S → CategoryTheory.Limits.IsZero (tateCohomology (Rep.res S.subtype A) q))
  (h₂ :
    ∀ (p : ℕ) [Fact (Nat.Prime p)] (S : Subgroup G) [inst : Fintype ↥S],
      IsPGroup p ↥S → CategoryTheory.Limits.IsZero (tateCohomology (Rep.res S.subtype A) (q + 1)))
  (S : Subgroup G) [Fintype ↥S] (n : ℤ) :
  CategoryTheory.Limits.IsZero (tateCohomology (Rep.res S.subtype A) n)
Lean

Formalized in Tau Ceti as TauCeti.TateCohomology.isZero_of_forall_isPGroup.

Other forms

Tate's cohomological triviality criterion for ordinary cohomology (Milne II 3.10). Formalized in Tau Ceti as TauCeti.groupCohomology.isZero_of_forall_isPGroup.

TauCeti.groupCohomology.isZero_of_forall_isPGroup.{u} {k G : Type u} [CommRing k] [Group G]
  [Finite G] (A : Rep.{u, u, u} k G) {q : ℕ}
  (h₁ :
    ∀ (p : ℕ) [Fact (Nat.Prime p)] (S : Subgroup G),
      IsPGroup p ↥S → CategoryTheory.Limits.IsZero (groupCohomology (Rep.res S.subtype A) (q + 1)))
  (h₂ :
    ∀ (p : ℕ) [Fact (Nat.Prime p)] (S : Subgroup G),
      IsPGroup p ↥S → CategoryTheory.Limits.IsZero (groupCohomology (Rep.res S.subtype A) (q + 2)))
  (S : Subgroup G) (n : ℕ) :
  CategoryTheory.Limits.IsZero (groupCohomology (Rep.res S.subtype A) (n + 1))
Sources
LeanTauCeti.TateCohomology.isZero_of_forall_isPGroup · TauCeti.groupCohomology.isZero_of_forall_isPGroup
Uses 1 · Used by 12
Proof usesThe Sylow reduction of Tate's triviality criterion (Milne II 3.10, last paragraph)
Used byThe global class formation · The global invariant · The global invariant is injective · The Kummer case of global existence (Milne VII, Lemma 9.3) · Hilbert sign prescription (O'Meara 71:19a) · Existence of the Tate module of a finite layer (NSW (5.6.5) and the proof of (7.4.1)) · The cyclic Hasse norm theorem · The Hasse principle for Brauer classes, from idele-class H¹ · The Kronecker–Weber theorem · The Kummer case of the second fundamental inequality · Tate's isomorphism criterion · The Tate–Nakayama theorem

TheoremTate's isomorphism criterion#

Let G be a finite group and f : A ⟶ B a morphism of representations of G. If, for every subgroup S of G of prime-power order, the map induced by f on the Tate cohomology of S is surjective in degree q - 1, bijective in degree q and injective in degree q + 1, then f induces a bijection Ĥⁿ(G, A) → Ĥⁿ(G, B) in every degree n.

TauCeti.TateCohomology.map_bijective_of_forall_isPGroup.{u} {k G : Type u} [CommRing k] [Group G]
  {A B : Rep.{u, u, u} k G} (f : A ⟶ B) [Fintype G] {q : ℤ}
  (hsurj :
    ∀ (p : ℕ) [Fact (Nat.Prime p)] (S : Subgroup G) [inst : Fintype ↥S],
      IsPGroup p ↥S →
        Function.Surjective
          ⇑(CategoryTheory.ConcreteCategory.hom
              ((tateCohomologyFunctor (q - 1)).map ((Rep.resFunctor S.subtype).map f))))
  (hbij :
    ∀ (p : ℕ) [Fact (Nat.Prime p)] (S : Subgroup G) [inst : Fintype ↥S],
      IsPGroup p ↥S →
        Function.Bijective
          ⇑(CategoryTheory.ConcreteCategory.hom
              ((tateCohomologyFunctor q).map ((Rep.resFunctor S.subtype).map f))))
  (hinj :
    ∀ (p : ℕ) [Fact (Nat.Prime p)] (S : Subgroup G) [inst : Fintype ↥S],
      IsPGroup p ↥S →
        Function.Injective
          ⇑(CategoryTheory.ConcreteCategory.hom
              ((tateCohomologyFunctor (q + 1)).map ((Rep.resFunctor S.subtype).map f))))
  (n : ℤ) :
  Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom ((tateCohomologyFunctor n).map f))
Lean

Formalized in Tau Ceti as TauCeti.TateCohomology.map_bijective_of_forall_isPGroup.

Other forms

Tate's isomorphism criterion, on every subgroup. Formalized in Tau Ceti as TauCeti.TateCohomology.map_res_bijective_of_forall_isPGroup.

TauCeti.TateCohomology.map_res_bijective_of_forall_isPGroup.{u} {k G : Type u} [CommRing k]
  [Group G] {A B : Rep.{u, u, u} k G} (f : A ⟶ B) [Finite G] {q : ℤ}
  (hsurj :
    ∀ (p : ℕ) [Fact (Nat.Prime p)] (S : Subgroup G) [inst : Fintype ↥S],
      IsPGroup p ↥S →
        Function.Surjective
          ⇑(CategoryTheory.ConcreteCategory.hom
              ((tateCohomologyFunctor (q - 1)).map ((Rep.resFunctor S.subtype).map f))))
  (hbij :
    ∀ (p : ℕ) [Fact (Nat.Prime p)] (S : Subgroup G) [inst : Fintype ↥S],
      IsPGroup p ↥S →
        Function.Bijective
          ⇑(CategoryTheory.ConcreteCategory.hom
              ((tateCohomologyFunctor q).map ((Rep.resFunctor S.subtype).map f))))
  (hinj :
    ∀ (p : ℕ) [Fact (Nat.Prime p)] (S : Subgroup G) [inst : Fintype ↥S],
      IsPGroup p ↥S →
        Function.Injective
          ⇑(CategoryTheory.ConcreteCategory.hom
              ((tateCohomologyFunctor (q + 1)).map ((Rep.resFunctor S.subtype).map f))))
  (S : Subgroup G) [Fintype ↥S] (n : ℤ) :
  Function.Bijective
    ⇑(CategoryTheory.ConcreteCategory.hom
        ((tateCohomologyFunctor n).map ((Rep.resFunctor S.subtype).map f)))
Sources
LeanTauCeti.TateCohomology.map_bijective_of_forall_isPGroup · TauCeti.TateCohomology.map_res_bijective_of_forall_isPGroup
Uses 1 · Used by 1
Proof usesTate's cohomological triviality criterion (Milne II 3.10)
Used byTate's theorem

TheoremTate's lattice lemma#

Let G be a finite cyclic group, K a nontrivial commutative ℚ-algebra (classically ℝ) and ρ a representation of G on a K-module V. If M and N are integral representations of G, free over ℤ with M of finite rank, and G-equivariant maps i : M → V and j : N → V exhibit V as the base change of M and of N to K, then M and N have the same Herbrand quotient. The rank of N is then finite as well, being that of V.

TauCeti.TateCohomology.herbrandQuotient_eq_of_isBaseChange.{u_1, u_2} {G : Type} [Group G]
  [Fintype G] [IsCyclic G] {K : Type u_1} {V : Type u_2} [CommRing K] [Nontrivial K] [Algebra ℚ K]
  [AddCommGroup V] [_root_.Module K V] (ρ : Representation K G V) {M N : Rep.{0, 0, 0} ℤ G}
  [Module.Free ℤ ↑M] [Module.Finite ℤ ↑M] [Module.Free ℤ ↑N] {i : ↑M →ₗ[ℤ] V} {j : ↑N →ₗ[ℤ] V}
  (hi : IsBaseChange K i) (hj : IsBaseChange K j)
  (hiG : ∀ (g : G) (x : ↑M), i ((M.ρ g) x) = (ρ g) (i x))
  (hjG : ∀ (g : G) (y : ↑N), j ((N.ρ g) y) = (ρ g) (j y)) :
  TauCeti.TateCohomology.herbrandQuotient M = TauCeti.TateCohomology.herbrandQuotient N
Lean

Formalized in Tau Ceti as TauCeti.TateCohomology.herbrandQuotient_eq_of_isBaseChange.

Sources
LeanTauCeti.TateCohomology.herbrandQuotient_eq_of_isBaseChange
Used by 9
Used byThe global class formation · The global invariant · The global invariant is injective · The Kummer case of global existence (Milne VII, Lemma 9.3) · Hilbert sign prescription (O'Meara 71:19a) · The cyclic Hasse norm theorem · The Hasse principle for Brauer classes, from idele-class H¹ · The Kronecker–Weber theorem · The Kummer case of the second fundamental inequality

TheoremTate's theorem#

Let G be a finite group, N a representation of G over ℤ and u ∈ H²(G, N). Suppose that

  • u generates H²(G, N), a group of order |G|;
  • for every subgroup S of G of prime-power order, H¹(S, N) = 0 and H²(S, N) has order |S|.

Then cup product with u is a bijection H^r(G, ℤ) → H^{r+2}(G, ℤ ⊗ N) in every integer degree r. The classical hypothesis that the restriction of u to each subgroup generates its H² is a consequence of these and is not assumed.

TauCeti.TateCohomology.cup_bijective_of_forall_isPGroup {G : Type} [Group G] [Fintype G]
  (N : Rep.{0, 0, 0} ℤ G) (u : ↑(tateCohomology N 2))
  (hgen : ∀ (y : ↑(tateCohomology N 2)), ∃ m, m • u = y)
  (hcardG : Nat.card ↑(tateCohomology N 2) = Nat.card G)
  (h1 :
    ∀ (p : ℕ) [Fact (Nat.Prime p)] (S : Subgroup G) [inst : Fintype ↥S],
      IsPGroup p ↥S → CategoryTheory.Limits.IsZero (tateCohomology (Rep.res S.subtype N) 1))
  (hcard :
    ∀ (p : ℕ) [Fact (Nat.Prime p)] (S : Subgroup G) [inst : Fintype ↥S],
      IsPGroup p ↥S → Nat.card ↑(tateCohomology (Rep.res S.subtype N) 2) = Nat.card ↥S)
  (r r' : ℤ) (h : r + 2 = r') :
  Function.Bijective fun x => ((TauCeti.TateCohomology.cup (Rep.trivial ℤ G ℤ) N r 2 r' h) x) u
Lean

Formalized in Tau Ceti as TauCeti.TateCohomology.cup_bijective_of_forall_isPGroup.

Other forms

Tate's theorem, with the degree-zero injection as hypothesis. Formalized in Tau Ceti as TauCeti.TateCohomology.cup_bijective_of_cupTrivialInt_injective.

TauCeti.TateCohomology.cup_bijective_of_cupTrivialInt_injective {G : Type} [Group G] [Fintype G]
  (N : Rep.{0, 0, 0} ℤ G) (u : ↑(tateCohomology N 2))
  (hinj₀ : Function.Injective ⇑(TauCeti.TateCohomology.cupTrivialInt N u))
  (h1 :
    ∀ (p : ℕ) [Fact (Nat.Prime p)] (S : Subgroup G) [inst : Fintype ↥S],
      IsPGroup p ↥S → CategoryTheory.Limits.IsZero (tateCohomology (Rep.res S.subtype N) 1))
  (hcard :
    ∀ (p : ℕ) [Fact (Nat.Prime p)] (S : Subgroup G) [inst : Fintype ↥S],
      IsPGroup p ↥S → Nat.card ↑(tateCohomology (Rep.res S.subtype N) 2) = Nat.card ↥S)
  (r r' : ℤ) (h : r + 2 = r') :
  Function.Bijective fun x => ((TauCeti.TateCohomology.cup (Rep.trivial ℤ G ℤ) N r 2 r' h) x) u
Sources
LeanTauCeti.TateCohomology.cup_bijective_of_forall_isPGroup · TauCeti.TateCohomology.cup_bijective_of_cupTrivialInt_injective
Uses 1 · Used by 14
Proof usesTate's isomorphism criterion
Used byHilbert reciprocity · Local reciprocity for the Weil group · TauCeti.ClassFieldTheory.tateTheorem · The global class formation · The global invariant · The global invariant is injective · The Kummer case of global existence (Milne VII, Lemma 9.3) · Existence of the Tate module of a finite layer (NSW (5.6.5) and the proof of (7.4.1)) · Local reciprocity for A(L) · The cyclotomic normalization of the local Artin map of a finite extension of ℚ_p · Global existence (Milne VII, Theorem 9.5) · The Kronecker–Weber theorem · The principal ideal theorem for a class formation · The finite level of the generator theorem (NSW, proof of (7.4.1))

TheoremThe Tate–Nakayama theorem#

The Tate–Nakayama theorem (Nakayama, Ann. of Math. 65 (1957); Serre, Local Fields, IX §8). Let G be a finite group, C a representation of G over ℤ and u ∈ H²(G, C). Suppose that for every subgroup S of G of prime-power order

  • H¹(S, C) = 0,
  • the restriction of u generates H²(S, C), and
  • H²(S, C) has |S| elements.

Then for every representation M with Tor₁^ℤ(M, C) = 0, in the form that M ⊗ X → M ⊗ Y is injective for every short exact sequence 0 → X → Y → C → 0 of abelian groups, cup product with u is a bijection H^r(G, M) → H^{r+2}(G, M ⊗ C) in every integer degree r.

TauCeti.TateCohomology.cup_bijective_of_forall_isPGroup_of_lTensor_injective {G : Type} [Group G]
  [Fintype G] (M C : Rep.{0, 0, 0} ℤ G) (u : ↑(groupCohomology C 2))
  (h1 :
    ∀ (p : ℕ) [Fact (Nat.Prime p)] (S : Subgroup G),
      IsPGroup p ↥S → CategoryTheory.Limits.IsZero (groupCohomology (Rep.res S.subtype C) 1))
  (hgen :
    ∀ (p : ℕ) [Fact (Nat.Prime p)] (S : Subgroup G),
      IsPGroup p ↥S →
        ∀ (x : ↑(groupCohomology (Rep.res S.subtype C) 2)),
          ∃ m,
            m •
                (CategoryTheory.ConcreteCategory.hom
                    (groupCohomology.map S.subtype
                      (CategoryTheory.CategoryStruct.id (Rep.res S.subtype C)) 2))
                  u =
              x)
  (hcard :
    ∀ (p : ℕ) [Fact (Nat.Prime p)] (S : Subgroup G),
      IsPGroup p ↥S → Nat.card ↑(groupCohomology (Rep.res S.subtype C) 2) = Nat.card ↥S)
  (hM :
    ∀ {X Y : Type} [inst : AddCommGroup X] [inst_1 : _root_.Module ℤ X] [inst_2 : AddCommGroup Y]
      [inst_3 : _root_.Module ℤ Y] (f : X →ₗ[ℤ] Y) (g : Y →ₗ[ℤ] ↑C),
      Function.Injective ⇑f →
        Function.Exact ⇑f ⇑g →
          Function.Surjective ⇑g → Function.Injective ⇑(LinearMap.lTensor (↑M) f))
  (r r' : ℤ) (h : r + 2 = r') :
  Function.Bijective fun x =>
    ((TauCeti.TateCohomology.cup M C r 2 r' h) x)
      ((CategoryTheory.ConcreteCategory.hom ((TateCohomology.isoGroupCohomology 2).app C).inv) u)
Lean

Formalized in Tau Ceti as TauCeti.TateCohomology.cup_bijective_of_forall_isPGroup_of_lTensor_injective.

Sources
LeanTauCeti.TateCohomology.cup_bijective_of_forall_isPGroup_of_lTensor_injective
Uses 4
Proof usesCorestriction through Shapiro's lemma · Nakayama–Rim, Sylow form · Restriction through Shapiro's lemma · Tate's cohomological triviality criterion (Milne II 3.10)

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.