Continuous cohomology of profinite groups

The declarations the status of Tau Ceti's roadmap names, and the other results named in the modules where only this status names declarations, or in folders below the areas where only it names 2 or more, as Tau Ceti has them at commit ace60277.

TheoremHilbert 90 for the absolute Galois group, stated for Mathlib's canonical continuous cohomology#

H¹(G_K, (Kˢ)ˣ) = 0 (NSW (6.2.1)). This is the form in which the vanishing feeds the canonical all-degree theory, where it makes the Kummer map Kˣ → H¹(G_K, μₙ) surjective for n positive and invertible in K.

TauCeti.hilbert90.{u_1} (K : Type u_1) [Field K] :
  CategoryTheory.Limits.IsZero
    (continuousCohomology 1
      (TauCeti.ofDiscreteModule ℤ (TauCeti.AbsoluteGaloisGroup K) (TauCeti.UnitsCoeff K)))

Lean

Formalized in Tau Ceti as TauCeti.hilbert90.

Sources

• Tau Ceti documentation: TauCeti.hilbert90
• Source of TauCeti.hilbert90 in TauCeti/FieldTheory/GaloisCohomology/Hilbert90.lean
• Tau Ceti roadmap status: Continuous cohomology of profinite groups

LeanTauCeti.hilbert90

DefinitionThe Kummer isomorphism#

The Kummer isomorphism Kˣ ⧸ (Kˣ)ⁿ ≃* H¹(G_K, μₙ) (NSW (6.2.1) and the display following it), for n invertible in K. It is TauCeti.kummerClassMap, which is injective since the kernel of the Kummer map is (Kˣ)ⁿ and surjective by Hilbert 90.

TauCeti.kummerIso.{u_1} (K : Type u_1) [Field K] (n : ℕ) (hn : IsUnit ↑n) :
  TauCeti.powerClassQuotient Kˣ n ≃*
    Multiplicative
      (TauCeti.ContCohomology.H1 (TauCeti.AbsoluteGaloisGroup K) (TauCeti.KummerCoeff K n))

Lean

Formalized in Tau Ceti as TauCeti.kummerIso.

Sources

• Tau Ceti documentation: TauCeti.kummerIso
• Source of TauCeti.kummerIso in TauCeti/FieldTheory/GaloisCohomology/Kummer.lean
• Tau Ceti roadmap status: Continuous cohomology of profinite groups

LeanTauCeti.kummerIso

Used by 25

Used byThe equivariant Kummer isomorphism on Kummer classes (TauCeti.dualTensorHom_kummerH1FiniteRepresentationEquiv) · Hilbert reciprocity · Local reciprocity for the Weil group · Quadratic reciprocity is Hilbert reciprocity for two odd primes · Demushkin's theorem · 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) · 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) · Hilbert's product formula · The Evens norm of a Kummer class over a local field, as an element of H²(G_K, 𝔽₂) · The relative Stiefel–Whitney formula in degree two, on the trace forms themselves (Kahn, Théorème 2 in degree two) · The relative Stiefel–Whitney formula over a local field · 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 equivariant Kummer isomorphism on Kummer classes (TauCeti.ClassFieldTheory.dualTensorHom_kummerH1ConjRepresentationEquiv) · The Euler characteristic formula and G₀ · The finite level of the generator theorem (NSW, proof of (7.4.1)) · The Gram formula for the Kummer cup over ℚ₂

TheoremThe strict cohomological dimension through integral coefficients (NSW (3.3.4)), as vanishing predicates#

For a profinite group G and a prime p, StrictCohomologicalDimensionLE p G n holds if and only if CohomologicalDimensionLE p G n holds and the p-primary component of Hⁿ⁺¹(U, ℤ) vanishes for every open subgroup U, the integers carrying the trivial action.

TauCeti.strictCohomologicalDimensionLE_iff_forall_openSubgroup.{u} {p : ℕ} {G : Type u} [Group G]
  [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {n : ℕ}
  (hp : Nat.Prime p) :
  TauCeti.StrictCohomologicalDimensionLE p G n ↔
    TauCeti.CohomologicalDimensionLE p G n ∧
      ∀ (U : OpenSubgroup G),
        AddCommGroup.primaryComponent
            (↑(continuousCohomology (n + 1)
                  (TopRep.of (ContRepresentation.trivial ℤ (↥↑U) (ULift.{u, 0} ℤ)))).toModuleCat)
            p =
          ⊥

Lean

Formalized in Tau Ceti as TauCeti.strictCohomologicalDimensionLE_iff_forall_openSubgroup.

Sources

• Tau Ceti documentation: TauCeti.strictCohomologicalDimensionLE_iff_forall_openSubgroup
• Source of TauCeti.strictCohomologicalDimensionLE_iff_forall_openSubgroup in TauCeti/RepresentationTheory/Homological/ContCohomology/CohomologicalDimension/IntegralCriterion.lean
• Tau Ceti roadmap status: Continuous cohomology of profinite groups

LeanTauCeti.strictCohomologicalDimensionLE_iff_forall_openSubgroup

Uses 1 · Used by 2

Proof usesShapiro's lemma in degree one

Used byExistence of the Tate module of a finite layer (NSW (5.6.5) and the proof of (7.4.1)) · The finite level of the generator theorem (NSW, proof of (7.4.1))

TheoremThe p-cohomological dimension of the profinite integers is one, for every prime p#

TauCeti.zHat.cohomologicalDimensionAt_eq_one.{u} (p : ℕ) [Fact (Nat.Prime p)] :
  TauCeti.cohomologicalDimensionAt p ↑TauCeti.zHat.toProfinite.toTop = 1

Lean

Formalized in Tau Ceti as TauCeti.zHat.cohomologicalDimensionAt_eq_one.

Sources

• Tau Ceti documentation: TauCeti.zHat.cohomologicalDimensionAt_eq_one
• Source of TauCeti.zHat.cohomologicalDimensionAt_eq_one in TauCeti/Topology/Algebra/Group/Profinite/ZHat/CohomologicalDimension.lean
• Tau Ceti roadmap status: Continuous cohomology of profinite groups

LeanTauCeti.zHat.cohomologicalDimensionAt_eq_one

Uses 2

Proof usesDimension shifting in every positive degree · The first isomorphism theorem for a surjective strict homomorphism of topological groups

DefinitionTauCeti.zHat.h2EquivRatCircle#

Second integral continuous cohomology of the profinite integers is the rational circle. The inverse sends a rational-circle value to the connecting class of the unique continuous character taking that value at the canonical generator.

TauCeti.zHat.h2EquivRatCircle.{u}
  [DistribMulAction (↑TauCeti.zHat.toProfinite.toTop) (ULift.{u, 0} ℤ)]
  [DistribMulAction (↑TauCeti.zHat.toProfinite.toTop) (ULift.{u, 0} ℚ)]
  [TopologicalSpace (ULift.{u, 0} ℚ)] [DiscreteTopology (ULift.{u, 0} ℚ)] (C : Type u)
  [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C]
  [DistribMulAction (↑TauCeti.zHat.toProfinite.toTop) C] (e : C ≃+ AddCircle 1)
  (hℤ : ∀ (g : ↑TauCeti.zHat.toProfinite.toTop) (x : ULift.{u, 0} ℤ), g • x = x)
  (hℚ : ∀ (g : ↑TauCeti.zHat.toProfinite.toTop) (x : ULift.{u, 0} ℚ), g • x = x)
  (hC : ∀ (g : ↑TauCeti.zHat.toProfinite.toTop) (x : C), g • x = x) :
  ↑(continuousCohomology 2
          (TauCeti.ofDiscreteModule ℤ (↑TauCeti.zHat.toProfinite.toTop)
            (ULift.{u, 0} ℤ))).toModuleCat ≃+
    AddCircle 1

Lean

Formalized in Tau Ceti as TauCeti.zHat.h2EquivRatCircle.

Sources

• Tau Ceti documentation: TauCeti.zHat.h2EquivRatCircle
• Source of TauCeti.zHat.h2EquivRatCircle in TauCeti/Topology/Algebra/Group/Profinite/ZHat/IntegralCohomology.lean
• Tau Ceti roadmap status: Continuous cohomology of profinite groups

LeanTauCeti.zHat.h2EquivRatCircle

TheoremThe index-two corestriction--cup sequence is exact in every degree#

The kernel of cupping with the subgroup character consists exactly of the corestrictions from U.

OpenSubgroup.exact_cor_cup_of_index_two.{u} {G : Type u} [Group G] [TopologicalSpace G]
  [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (U : OpenSubgroup G)
  (hU : (↑U).index = 2) (n : ℕ) :
  Function.Exact ⇑(CategoryTheory.ConcreteCategory.hom (TauCeti.trivialF2CorMap G ↑U ⋯ n)) fun x =>
    (((TauCeti.trivialF2TopPairing G).cup n 1) x) (U.indexTwoCharacterClass hU)

Lean

Formalized in Tau Ceti as OpenSubgroup.exact_cor_cup_of_index_two.

Sources

• Tau Ceti documentation: OpenSubgroup.exact_cor_cup_of_index_two
• Source of OpenSubgroup.exact_cor_cup_of_index_two in TauCeti/RepresentationTheory/Homological/ContCohomology/Corestriction/IndexTwo/CupExact.lean
• Tau Ceti roadmap status: Continuous cohomology of profinite groups

LeanOpenSubgroup.exact_cor_cup_of_index_two

Uses 1 · Used by 1

Statement usesShapiro's lemma in degree one

Used byTauCeti.cyclicTwoCohomPolynomialEquiv

DefinitionTauCeti.cyclicTwoCohomPolynomialEquiv#

The canonical graded mod-two cohomology algebra of an order-two discrete group is a polynomial algebra, with X sent to its nontrivial character in degree one.

TauCeti.cyclicTwoCohomPolynomialEquiv.{u} (G : Type u) [Group G] [TopologicalSpace G]
  [IsTopologicalGroup G] [DiscreteTopology G] (hG : Nat.card G = 2) :
  Polynomial (ZMod 2) ≃ₐ[ZMod 2] TauCeti.gradedCohomF2 G

Lean

Formalized in Tau Ceti as TauCeti.cyclicTwoCohomPolynomialEquiv.

Sources

• Tau Ceti documentation: TauCeti.cyclicTwoCohomPolynomialEquiv
• Source of TauCeti.cyclicTwoCohomPolynomialEquiv in TauCeti/RepresentationTheory/Homological/ContCohomology/Cup/TrivialF2/CyclicTwo.lean
• Tau Ceti roadmap status: Continuous cohomology of profinite groups

LeanTauCeti.cyclicTwoCohomPolynomialEquiv

Uses 2

Proof usesThe index-two corestriction--cup sequence is exact in every degree · Shapiro's lemma in degree one

TheoremTauCeti.ContCohomology.smoothTensorInducedDiagonalClass_eq_graphClass#

The tensor-induced class of the homogeneous degree-one cocycle of a continuous character is the index-two graph class. The transversal has representatives 1 and s, and the coefficient identification multiplies the two tensor factors. The equality includes only the transport of degrees from 2 to card (G ⧸ U) * 1.

The quotient Fintype is a caller parameter: the diagonal class and its graded contraction use that enumeration. The input z and its cocycle data are exactly the inputs of smoothTensorInducedDiagonalClass; hzα identifies their explicit homogeneous representative. The theorem compares the classes associated to this explicit homogeneous representative. The statement installs local compactness from the compact open subgroup because the existing graphClass requires it.

TauCeti.ContCohomology.smoothTensorInducedDiagonalClass_eq_graphClass.{u} {G : Type u} [Group G]
  [TopologicalSpace G] [IsTopologicalGroup G] (U : OpenSubgroup G) (hU : (↑U).index = 2) (s : G)
  (hs : s ∉ U) (α : ↥↑U →* Multiplicative (ZMod 2)) (hα : Continuous ⇑α) [Fintype (G ⧸ ↑U)]
  [CompactSpace ↥↑U] (z : (TauCeti.trivialF2 ↥↑U).gradedResolutionModule)
  (hz : z ∈ (TauCeti.trivialF2 ↥↑U).gradedResolutionPiece 1)
  (hinv : ∀ (x : ↥↑U), ((TauCeti.trivialF2 ↥↑U).gradedResolutionTopRep.ρ x) z = z)
  (hdz : (TauCeti.trivialF2 ↥↑U).gradedResolutionDifferential z = 0)
  (hzα :
    z =
      (DirectSum.lof ℤ ℕ (fun n => ↑((TauCeti.trivialF2 ↥↑U).resolutionX (n + 1))) 1)
        ↑(TauCeti.ContCohomology.inhomogeneousCochain1 (fun x => Multiplicative.toAdd (α x)) ⋯)) :
  have t := ⟨Set.range ((↑U).indexTwoTransversal s), ⋯⟩;
  let A := { obj := TauCeti.trivialF2 ↥↑U, property := ⋯ };
  (CategoryTheory.ConcreteCategory.hom
        (TauCeti.ContinuousCohomology.coeffMap
          (TauCeti.smoothTensorInducedTrivialF2Iso G ↑U ⋯ t).hom.hom (Fintype.card (G ⧸ ↑U) * 1)))
      (TauCeti.smoothTensorInducedDiagonalClass ↑U ⋯ t A ⋯ z hz hinv hdz) =
    (TopModuleCat.Hom.hom (CategoryTheory.eqToHom ⋯)) (TauCeti.ContCohomology.graphClass U hU α hα)

Lean

Formalized in Tau Ceti as TauCeti.ContCohomology.smoothTensorInducedDiagonalClass_eq_graphClass.

Sources

• Tau Ceti documentation: TauCeti.ContCohomology.smoothTensorInducedDiagonalClass_eq_graphClass
• Source of TauCeti.ContCohomology.smoothTensorInducedDiagonalClass_eq_graphClass in TauCeti/RepresentationTheory/Homological/ContCohomology/Evens/TensorInduction.lean
• Tau Ceti roadmap status: Continuous cohomology of profinite groups

LeanTauCeti.ContCohomology.smoothTensorInducedDiagonalClass_eq_graphClass

Uses 2

Statement usesThe Evens norm of a cocycle

Proof usesFrobenius reciprocity for coind₁, uniqueness

DefinitionDimension shifting in every positive degree#

Dimension shifting in every positive degree, Hⁱ⁺¹(G, M) ≅ Hⁱ(G, Coind_1^G M ⧸ M) for i ≥ 1 and a compact group G, as an isomorphism of Mathlib's canonical continuous cohomology. Its inverse is the connecting map of TauCeti.ContCohomology.coindShortExact G ⊥ M (dimensionShiftIso_inv), an isomorphism by isIso_coindShortExact_bot_delta. The analogous statement on the explicit low-degree model, for a profinite G and in the direction of the connecting map, is TauCeti.ContCohomology.explicitDimensionShift1 : H¹(G, Coind_1^G M ⧸ M) ≃+ H²(G, M).

TauCeti.ContCohomology.dimensionShiftIso.{u} (G : Type u) [Group G] [TopologicalSpace G]
  [IsTopologicalGroup G] [CompactSpace G] (M : Type u) [AddCommGroup M] [TopologicalSpace M]
  [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] (i : ℕ) (hi : 0 < i) :
  continuousCohomology (i + 1) (TauCeti.ofDiscreteModule ℤ G M) ≅
    continuousCohomology i
      (TauCeti.ofDiscreteModule ℤ G (TauCeti.ContCohomology.CoindQuotient G ⊥ M))

Lean

Formalized in Tau Ceti as TauCeti.ContCohomology.dimensionShiftIso.

Sources

• Tau Ceti documentation: TauCeti.ContCohomology.dimensionShiftIso
• Source of TauCeti.ContCohomology.dimensionShiftIso in TauCeti/RepresentationTheory/Homological/ContCohomology/DimensionShifting/Basic.lean
• Tau Ceti roadmap status: Continuous cohomology of profinite groups

LeanTauCeti.ContCohomology.dimensionShiftIso

Used by 7

Used byExistence of the Tate module of a finite layer (NSW (5.6.5) and the proof of (7.4.1)) · Shafarevich's theorem · The finite level of the generator theorem (NSW, proof of (7.4.1)) · The p-cohomological dimension of the profinite integers is one, for every prime p · Tate's criterion for the cohomological dimension of a pro-p group · Serre's theorem at arbitrary rank, as an equivalence · The pro-p Nielsen–Schreier theorem

DefinitionThe index-two degree-one Evens norm#

The index-two degree-one Evens norm Nᴱᵛ : H¹(U, 𝔽₂) → H²(G, 𝔽₂) for an open subgroup U of index two: the graph class of a continuous homomorphism representing the class, which homClass_surjective provides and graphClass_representative_independent makes irrelevant. On the class of α it is graphClass U hU α (evensNormIndexTwo_homClass). It is a function and not an additive map.

TauCeti.ContCohomology.evensNormIndexTwo.{u} {G : Type u} [Group G] [TopologicalSpace G]
  [IsTopologicalGroup G] [LocallyCompactSpace G] (U : OpenSubgroup G) (hU : (↑U).index = 2)
  (x : ↑(continuousCohomology 1 (TauCeti.trivialF2 ↥↑U)).toModuleCat) :
  ↑(continuousCohomology 2 (TauCeti.trivialF2 G)).toModuleCat

Lean

Formalized in Tau Ceti as TauCeti.ContCohomology.evensNormIndexTwo.

Sources

• Tau Ceti documentation: TauCeti.ContCohomology.evensNormIndexTwo
• Source of TauCeti.ContCohomology.evensNormIndexTwo in TauCeti/RepresentationTheory/Homological/ContCohomology/Evens/IndexTwoNorm.lean
• Tau Ceti roadmap status: Continuous cohomology of profinite groups

LeanTauCeti.ContCohomology.evensNormIndexTwo

Used by 4

Used bySerre's formula for the Evens norm of a Kummer class (Serre, Théorème 1′ at n = 2) · The Evens norm of a Kummer class over a local field, as an element of H²(G_K, 𝔽₂) · The relative Stiefel–Whitney formula in degree two, on the trace forms themselves (Kahn, Théorème 2 in degree two) · The relative Stiefel–Whitney formula over a local field

DefinitionThe Evens norm of a cocycle#

for a homogeneous cocycle z of degree n of the total coinduced resolution of A, fixed by U, the class in H^{l n}(G, Ind⊗ A) of its diagonal tensor z ⊗ ⋯ ⊗ z, one factor for each of the l cosets of U. Here A has characteristic two, so that the tensor-induced resolution is a complex, and the class is computed through TauCeti.smoothTensorInducedGradedResolutionContraction for some order on the cosets; by TauCeti.smoothTensorInducedDiagonalClass_eq it does not depend on that order.

TauCeti.smoothTensorInducedDiagonalClass.{u, v, w} {R : Type u} [CommRing R] [TopologicalSpace R]
  [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] [CompactSpace ↥U]
  (A : TauCeti.SmoothDiscreteTopRep R ↥U) [Fintype (G ⧸ U)] (hA : ∀ (a : ↑A.obj), a + a = 0) {n : ℕ}
  (z : A.obj.gradedResolutionModule) (hz : z ∈ A.obj.gradedResolutionPiece ↑n)
  (hinv : ∀ (u : ↥U), (A.obj.gradedResolutionTopRep.ρ u) z = z)
  (hdz : A.obj.gradedResolutionDifferential z = 0) :
  ↑(continuousCohomology (Fintype.card (G ⧸ U) * n)
        ((TauCeti.toSmoothDiscrete R G).obj
            (TauCeti.DiscreteRep.tensorInduced U hU s
              ((TauCeti.ofSmoothDiscrete R ↥U).obj A))).obj).toModuleCat

Lean

Formalized in Tau Ceti as TauCeti.smoothTensorInducedDiagonalClass.

Sources

• Tau Ceti documentation: TauCeti.smoothTensorInducedDiagonalClass
• Source of TauCeti.smoothTensorInducedDiagonalClass in TauCeti/RepresentationTheory/Tensor/Induction/Resolution.lean
• Tau Ceti roadmap status: Continuous cohomology of profinite groups

LeanTauCeti.smoothTensorInducedDiagonalClass

Used by 2

Used byTauCeti.ContCohomology.smoothTensorInducedDiagonalClass_eq_graphClass · TauCeti.smoothTensorInducedDiagonalClass_trivialF2_changeTransversal

TheoremTauCeti.smoothTensorInducedDiagonalClass_trivialF2_changeTransversal#

After identifying tensor-induced trivial 𝔽₂ coefficients with the ambient trivial coefficient object, the class of an invariant diagonal cocycle does not depend on the transversal.

TauCeti.smoothTensorInducedDiagonalClass_trivialF2_changeTransversal.{v} (G : Type v) [Group G]
  [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U)
  (s t : U.LeftTransversal) [U.FiniteIndex] [CompactSpace ↥U] [Fintype (G ⧸ U)] {n : ℕ}
  (z : (TauCeti.trivialF2 ↥U).gradedResolutionModule)
  (hz : z ∈ (TauCeti.trivialF2 ↥U).gradedResolutionPiece ↑n)
  (hinv : ∀ (u : ↥U), ((TauCeti.trivialF2 ↥U).gradedResolutionTopRep.ρ u) z = z)
  (hdz : (TauCeti.trivialF2 ↥U).gradedResolutionDifferential z = 0) :
  (CategoryTheory.ConcreteCategory.hom
        (TauCeti.ContinuousCohomology.coeffMap
          (TauCeti.smoothTensorInducedTrivialF2Iso G U hU t).hom.hom (Fintype.card (G ⧸ U) * n)))
      (TauCeti.smoothTensorInducedDiagonalClass U hU t
        { obj := TauCeti.trivialF2 ↥U, property := ⋯ } ⋯ z hz hinv hdz) =
    (CategoryTheory.ConcreteCategory.hom
        (TauCeti.ContinuousCohomology.coeffMap
          (TauCeti.smoothTensorInducedTrivialF2Iso G U hU s).hom.hom (Fintype.card (G ⧸ U) * n)))
      (TauCeti.smoothTensorInducedDiagonalClass U hU s
        { obj := TauCeti.trivialF2 ↥U, property := ⋯ } ⋯ z hz hinv hdz)

Lean

Formalized in Tau Ceti as TauCeti.smoothTensorInducedDiagonalClass_trivialF2_changeTransversal.

Sources

• Tau Ceti documentation: TauCeti.smoothTensorInducedDiagonalClass_trivialF2_changeTransversal
• Source of TauCeti.smoothTensorInducedDiagonalClass_trivialF2_changeTransversal in TauCeti/RepresentationTheory/Tensor/Induction/ChangeTransversal/Resolution.lean
• Tau Ceti roadmap status: Continuous cohomology of profinite groups

LeanTauCeti.smoothTensorInducedDiagonalClass_trivialF2_changeTransversal

Uses 2

Statement usesThe Evens norm of a cocycle

Proof usesFrobenius reciprocity for coind₁, uniqueness

DefinitionArtin's theorem for a finite group of automorphisms#

An injective homomorphism f : H →* Gal(L/K) from a finite group identifies H with the Galois group of L over the fixed field of the image of f (FixedPoints.toAlgAutMulEquiv). No finiteness of L/K is needed.

TauCeti.galEquivOfInjective {K L : Type} [Field K] [Field L] [Algebra K L] {H : Type} [Group H]
  [Finite H] {f : H →* Gal(L/K)} (hf : Function.Injective ⇑f) :
  H ≃* Gal(L/↥(IntermediateField.fixedField f.range))

Lean

Formalized in Tau Ceti as TauCeti.galEquivOfInjective.

Sources

• Tau Ceti documentation: TauCeti.galEquivOfInjective
• Source of TauCeti.galEquivOfInjective in TauCeti/FieldTheory/GaloisCohomology/Hilbert90.lean

LeanTauCeti.galEquivOfInjective

Used by 12

Used byHilbert reciprocity · Local reciprocity for the Weil group · The global class formation · The global invariant · The global invariant is injective · The local class formation · The local invariant · Existence of the Tate module of a finite layer (NSW (5.6.5) and the proof of (7.4.1)) · The cyclotomic normalization of the local Artin map of a finite extension of ℚ_p · Tate's duality on an open subgroup acting trivially on μₙ · The Kronecker–Weber theorem · The finite level of the generator theorem (NSW, proof of (7.4.1))

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.