The connecting map across the Tate norm #
For a short exact sequence 0 → M₁ → M₂ → M₃ → 0, the Tate connecting map from degree -1
of M₃ to degree zero of M₁ has a concrete description: lift a norm-zero element of M₃ to
M₂, take its norm, and lift that norm to an invariant element of M₁. The class of this
invariant is the image under the connecting map. This description allows the change-of-group
maps on the norm kernel and the invariants to be compared across the boundary of the Tate complex.
References #
- K. S. Brown, Cohomology of Groups, Chapter VI, §5.
- E. Artin and J. Tate, Class Field Theory, Chapter IV, §6.
- Mathlib's
CategoryTheory.ShortComplex.ShortExact.δ_applyinMathlib.Algebra.Homology.ConcreteCategory:δ_neg_one_HNegOneπspecializes this formula through the norm-kernel and invariant cycle identifications.
theorem
TauCeti.TateCohomology.δ_neg_one_HNegOneπ
{R G : Type u}
[CommRing R]
[Group G]
[Fintype G]
{S : CategoryTheory.ShortComplex (Rep R G)}
(hS : S.ShortExact)
(z : ↥(LinearMap.ker S.X₃.ρ.norm))
(y : ↑S.X₂)
(hy : (Rep.Hom.hom S.g) y = ↑z)
(x : ↥S.X₁.ρ.invariants)
(hx : (Rep.Hom.hom S.f) ↑x = S.X₂.ρ.norm y)
:
(CategoryTheory.ConcreteCategory.hom (TateCohomology.δ hS (-1)))
((CategoryTheory.ConcreteCategory.hom (HNegOneπ S.X₃)) z) = (CategoryTheory.ConcreteCategory.hom (H0π S.X₁)) x
The connecting map from degree -1 to degree zero sends a norm-zero representative to the
class of the norm of a lift, read in the invariant submodule of the first coefficient module.
theorem
TauCeti.TateCohomology.exists_δ_neg_one_eq_H0π
{R G : Type u}
[CommRing R]
[Group G]
[Fintype G]
{S : CategoryTheory.ShortComplex (Rep R G)}
(hS : S.ShortExact)
(z : ↥(LinearMap.ker S.X₃.ρ.norm))
:
∃ (y : ↑S.X₂) (x : ↥S.X₁.ρ.invariants),
(Rep.Hom.hom S.g) y = ↑z ∧ (Rep.Hom.hom S.f) ↑x = S.X₂.ρ.norm y ∧ (CategoryTheory.ConcreteCategory.hom (TateCohomology.δ hS (-1)))
((CategoryTheory.ConcreteCategory.hom (HNegOneπ S.X₃)) z) = (CategoryTheory.ConcreteCategory.hom (H0π S.X₁)) x
Every class in degree -1 admits lifts realizing the norm formula for its connecting image.