The twisted coefficients I(χ)/pⁱ of a p-adic character

Let G be a topological group and χ : G →ₜ* ℤ_pˣ a continuous character. For each i, the finite discrete module I(χ)/pⁱ is ℤ/pⁱ with G acting by g • x = χ(g) x, the action being through the truncation charScalar χ i g of χ g modulo pⁱ. The reductions I(χ)/pⁱ → I(χ)/pʲ for j ≤ i are equivariant and surjective, and form a compatible system. Dually, multiplication by pʲ is an equivariant injection I(χ)/pⁱ → I(χ)/pⁱ⁺ʲ, and the two fit into the short exact sequences

0 → I(χ)/pⁱ → I(χ)/pⁱ⁺ʲ → I(χ)/pʲ → 0

of discrete G-modules, whose long exact cohomology sequences relate the cohomology of the levels. These are the coefficient modules of Labute's prescription property of a character and of the twisted duality M^∨(χ) = Hom(M, I(χ)/pⁱ).

The coefficient module is placed in the universe of G, as a structure wrapping ZMod (p ^ i), because the universal property of a free pro-p group lifts maps into groups of the universe of its generators. I(χ)/p is ZModTwist χ 1, the module at i = 1, with carrier ZMod (p ^ 1).

Main definitions

• TauCeti.charScalar: the scalar χ g mod pⁱ by which g acts, as a monoid homomorphism G →* ZMod (p ^ i).
• TauCeti.ZModTwist: the twisted module I(χ)/pⁱ, a finite discrete G-module with continuous action; TauCeti.ZModTwist.equiv identifies it additively with ZMod (p ^ i).
• TauCeti.ZModTwist.reduce: the equivariant reduction I(χ)/pⁱ → I(χ)/pʲ for j ≤ i, with TauCeti.ZModTwist.reduce_self and TauCeti.ZModTwist.reduce_reduce its identity and composition laws.
• TauCeti.ZModTwist.mulPow: the equivariant multiplication by pʲ, I(χ)/pⁱ → I(χ)/pⁿ for i + j = n, with TauCeti.ZModTwist.mulPow_zero and TauCeti.ZModTwist.mulPow_mulPow its identity and composition laws.
• TauCeti.ZModTwist.shortExact: the short exact sequence 0 → I(χ)/pⁱ → I(χ)/pⁿ → I(χ)/pʲ → 0 of discrete G-modules, for i + j = n.

Main results

• TauCeti.ZModTwist.isProP_multiplicative: I(χ)/pⁱ is pro-p.
• TauCeti.ZModTwist.moduleBaer: I(χ)/pⁱ satisfies Baer's criterion over ℤ/pⁱ, so that Hom(-, I(χ)/pⁱ) is exact on the modules killed by pⁱ and the twisted dual M^∨(χ) of a short exact sequence of such modules is again short exact (TauCeti.ContCohomology.DiscreteShortExact.dual).
• TauCeti.IsProP.charScalar_one_eq_one, TauCeti.IsProP.smul_zModTwist_one_eq_self: a pro-p group acts trivially on the bottom level I(χ)/p, because a continuous character of a pro-p group takes principal-unit values.
• TauCeti.ZModTwist.reduce_surjective: the reductions are surjective.
• TauCeti.ZModTwist.mulPow_injective: the multiplications are injective.
• TauCeti.ZModTwist.reduce_mulPow_eq_mulPow_reduce: the reductions commute with the multiplications, and TauCeti.ZModTwist.explicitCoeff1_reduce_explicitCoeff1_mulPow is the induced commutation on H¹.
• TauCeti.ZModTwist.mulPow_reduce: multiplying by pʲ after reducing from level i + j to level i is multiplication by pʲ, and TauCeti.ZModTwist.explicitCoeff2_mulPow_explicitCoeff2_reduce is the induced identity on H².
• TauCeti.ZModTwist.pow_nsmul_eq_zero, TauCeti.ZModTwist.isPPrimaryTorsion: pⁱ kills I(χ)/pⁱ, which is therefore p-primary torsion; TauCeti.ZModTwist.exists_mulPow_eq_of_nsmul_eq_zero: the pⁱ-torsion of I(χ)/pⁱ⁺ʲ is the image of I(χ)/pⁱ under multiplication by pʲ.
• TauCeti.ZModTwist.smul_internalHom_eq_self: the conjugation action on the homomorphisms I(χ)/pⁱ → I(χ)/pⁿ between two twists is trivial, so all of them are invariant (TauCeti.ZModTwist.H0_internalHom_eq_top), and TauCeti.ZModTwist.surjective_explicitCoeff0_precomp_mulPow: every invariant homomorphism I(χ)/pⁱ → I(χ)/pⁿ extends along the multiplication by pʲ to an invariant endomorphism of I(χ)/pⁿ.

References

• J. P. Labute, Classification of Demushkin groups, Canad. J. Math. 19 (1967), 106–132, §2.

The scalar of the action

noncomputable def TauCeti.charScalar {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) (i : ℕ) : G →* ZMod (p ^ i)

The scalar by which g acts on I(χ)/pⁱ: the truncation of χ g modulo pⁱ, as a monoid homomorphism into the multiplicative monoid of ZMod (p ^ i).

Equations

• TauCeti.charScalar χ i = (↑(PadicInt.toZModPow i)).comp ((Units.coeHom ℤ_[p]).comp χ.toMonoidHom)

@[simp]

theorem TauCeti.charScalar_apply {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) (i : ℕ) (g : G) : (charScalar χ i) g = (PadicInt.toZModPow i) ↑(χ g)

The scalar of the action of g is the truncation of χ g modulo pⁱ.

theorem TauCeti.continuous_charScalar {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) (i : ℕ) : Continuous ⇑(charScalar χ i)

The scalar of the action depends continuously on the group element, because χ and the truncation modulo pⁱ are continuous.

theorem TauCeti.isUnit_charScalar {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) (i : ℕ) (g : G) : IsUnit ((charScalar χ i) g)

The scalar of the action is a unit, being the reduction of a p-adic unit.

theorem TauCeti.castHom_charScalar {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) {i j : ℕ} (h : j ≤ i) (g : G) : (ZMod.castHom ⋯ (ZMod (p ^ j))) ((charScalar χ i) g) = (charScalar χ j) g

The scalars at different levels are compatible under reduction: the scalar at level i reduces modulo pʲ to the scalar at level j ≤ i.

The twisted module

structure TauCeti.ZModTwist {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) (i : ℕ) : Type u

The twisted module I(χ)/pⁱ: the additive group ZMod (p ^ i), placed in the universe of G, on which g acts by multiplication by the scalar charScalar χ i g. The character is a parameter of the type so that the action can be an instance.

• val : ZMod (p ^ i)

  The underlying residue class modulo pⁱ.

theorem TauCeti.ZModTwist.ext_iff {p : ℕ} {inst✝ : Fact (Nat.Prime p)} {G : Type u} {inst✝¹ : Group G} {inst✝² : TopologicalSpace G} {χ : G →ₜ* ℤ_[p]ˣ} {i : ℕ} {x y : ZModTwist χ i} : x = y ↔ x.val = y.val

theorem TauCeti.ZModTwist.ext {p : ℕ} {inst✝ : Fact (Nat.Prime p)} {G : Type u} {inst✝¹ : Group G} {inst✝² : TopologicalSpace G} {χ : G →ₜ* ℤ_[p]ˣ} {i : ℕ} {x y : ZModTwist χ i} (val : x.val = y.val) : x = y

@[instance_reducible]

instance TauCeti.ZModTwist.instAddCommGroup {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) (i : ℕ) : AddCommGroup (ZModTwist χ i)

Equations

• TauCeti.ZModTwist.instAddCommGroup χ i = { toFun := TauCeti.ZModTwist.val, invFun := TauCeti.ZModTwist.mk, left_inv := ⋯, right_inv := ⋯ }.addCommGroup

def TauCeti.ZModTwist.equiv {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) (i : ℕ) : ZModTwist χ i ≃+ ZMod (p ^ i)

The identification of I(χ)/pⁱ with ZMod (p ^ i) as an additive group, forgetting the action.

Equations

• TauCeti.ZModTwist.equiv χ i = { toFun := TauCeti.ZModTwist.val, invFun := TauCeti.ZModTwist.mk, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

@[simp]

theorem TauCeti.ZModTwist.equiv_apply {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) (i : ℕ) (x : ZModTwist χ i) : (equiv χ i) x = x.val

@[simp]

theorem TauCeti.ZModTwist.equiv_symm_apply {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) (i : ℕ) (x : ZMod (p ^ i)) : (equiv χ i).symm x = { val := x }

@[simp]

theorem TauCeti.ZModTwist.val_zero {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) (i : ℕ) : val 0 = 0

@[simp]

theorem TauCeti.ZModTwist.val_add {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) (i : ℕ) (x y : ZModTwist χ i) : (x + y).val = x.val + y.val

@[simp]

theorem TauCeti.ZModTwist.val_neg {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) (i : ℕ) (x : ZModTwist χ i) : (-x).val = -x.val

@[simp]

theorem TauCeti.ZModTwist.val_sub {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) (i : ℕ) (x y : ZModTwist χ i) : (x - y).val = x.val - y.val

@[simp]

theorem TauCeti.ZModTwist.val_nsmul {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) (i k : ℕ) (x : ZModTwist χ i) : (k • x).val = k • x.val

@[simp]

theorem TauCeti.ZModTwist.pow_nsmul_eq_zero {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) (i : ℕ) (x : ZModTwist χ i) : p ^ i • x = 0

pⁱ kills I(χ)/pⁱ.

theorem TauCeti.ZModTwist.isPPrimaryTorsion {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) (i : ℕ) : IsPPrimaryTorsion p (ZModTwist χ i)

I(χ)/pⁱ is p-primary torsion.

@[instance_reducible]

instance TauCeti.ZModTwist.instTopologicalSpace {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) (i : ℕ) : TopologicalSpace (ZModTwist χ i)

Equations

• TauCeti.ZModTwist.instTopologicalSpace χ i = ⊥

instance TauCeti.ZModTwist.instDiscreteTopology {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) (i : ℕ) : DiscreteTopology (ZModTwist χ i)

instance TauCeti.ZModTwist.instFinite {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) (i : ℕ) : Finite (ZModTwist χ i)

@[instance_reducible]

instance TauCeti.ZModTwist.instModuleZModHPowNat {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) (i : ℕ) : Module (ZMod (p ^ i)) (ZModTwist χ i)

I(χ)/pⁱ is a ℤ/pⁱ-module, being killed by pⁱ (AddCommGroup.zmodModule); equiv is ℤ/pⁱ-linear for it, as every additive homomorphism of ℤ/pⁱ-modules is, and the scalar c acts on the residue class x.val by multiplication (val_zmod_smul).

Equations

• TauCeti.ZModTwist.instModuleZModHPowNat χ i = AddCommGroup.zmodModule ⋯

@[simp]

theorem TauCeti.ZModTwist.val_zmod_smul {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) (i : ℕ) (c : ZMod (p ^ i)) (x : ZModTwist χ i) : (c • x).val = c * x.val

theorem TauCeti.ZModTwist.moduleBaer {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) (i : ℕ) : Module.Baer (ZMod (p ^ i)) (ZModTwist χ i)

I(χ)/pⁱ is an injective ℤ/pⁱ-module, in the form of Baer's criterion: it is ℤ/pⁱ as a ℤ/pⁱ-module, which is self-injective (Module.Baer.of_addEquiv_zmod). Hence Hom(-, I(χ)/pⁱ) is exact on the modules killed by pⁱ, which is what makes the twisted dual M ↦ Hom(M, I(χ)/pⁱ) exact on short exact sequences of such modules (TauCeti.InternalHom.precomp_surjective_of_baer).

@[instance_reducible]

noncomputable instance TauCeti.ZModTwist.instSMul {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) (i : ℕ) : SMul G (ZModTwist χ i)

G acts on I(χ)/pⁱ through the scalar charScalar χ i.

Equations

• TauCeti.ZModTwist.instSMul χ i = { smul := fun (g : G) (x : TauCeti.ZModTwist χ i) => { val := (TauCeti.charScalar χ i) g * x.val } }

@[simp]

theorem TauCeti.ZModTwist.val_smul {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) (i : ℕ) (g : G) (x : ZModTwist χ i) : (g • x).val = (charScalar χ i) g * x.val

@[instance_reducible]

noncomputable instance TauCeti.ZModTwist.instDistribMulAction {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) (i : ℕ) : DistribMulAction G (ZModTwist χ i)

The action of G on I(χ)/pⁱ through the scalar charScalar χ i is distributive.

Equations

• TauCeti.ZModTwist.instDistribMulAction χ i = { toSMul := TauCeti.ZModTwist.instSMul χ i, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ }

instance TauCeti.ZModTwist.instContinuousSMul {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) (i : ℕ) : ContinuousSMul G (ZModTwist χ i)

The action of G on the discrete module I(χ)/pⁱ is continuous, because the scalar charScalar χ i is.

theorem TauCeti.ZModTwist.isProP_multiplicative {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) (i : ℕ) : IsProP p (Multiplicative (ZModTwist χ i))

I(χ)/pⁱ, with its discrete topology, is pro-p: it is the discrete cyclic group ℤ/pⁱ.

def TauCeti.ZModTwist.reduce {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) {i j : ℕ} (h : j ≤ i) : ZModTwist χ i →+[G] ZModTwist χ j

The reduction I(χ)/pⁱ → I(χ)/pʲ for j ≤ i, an equivariant additive homomorphism.

Equations

• TauCeti.ZModTwist.reduce χ h = { toFun := fun (x : TauCeti.ZModTwist χ i) => { val := (ZMod.castHom ⋯ (ZMod (p ^ j))) x.val }, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem TauCeti.ZModTwist.val_reduce {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) {i j : ℕ} (h : j ≤ i) (x : ZModTwist χ i) : ((reduce χ h) x).val = (ZMod.castHom ⋯ (ZMod (p ^ j))) x.val

@[simp]

theorem TauCeti.ZModTwist.reduce_self {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) {i : ℕ} (x : ZModTwist χ i) : (reduce χ ⋯) x = x

The reduction from a level to itself is the identity.

@[simp]

theorem TauCeti.ZModTwist.reduce_reduce {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) {i j k : ℕ} (h₁ : j ≤ i) (h₂ : k ≤ j) (x : ZModTwist χ i) : (reduce χ h₂) ((reduce χ h₁) x) = (reduce χ ⋯) x

Two successive reductions compose to the reduction between the outer levels.

theorem TauCeti.ZModTwist.reduce_surjective {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) {i j : ℕ} (h : j ≤ i) : Function.Surjective ⇑(reduce χ h)

The reduction I(χ)/pⁱ → I(χ)/pʲ is surjective: every residue class modulo pʲ lifts to a residue class modulo pⁱ.

The trivial module at level zero

instance TauCeti.ZModTwist.instSubsingletonOfNatNat {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) : Subsingleton (ZModTwist χ 0)

I(χ)/p⁰ = ℤ/1 is trivial.

Multiplication by pʲ

def TauCeti.ZModTwist.mulPow {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) {i j n : ℕ} (h : i + j = n) : ZModTwist χ i →+[G] ZModTwist χ n

Multiplication by pʲ, I(χ)/pⁱ →+[G] I(χ)/pⁿ for i + j = n. It is equivariant because the scalar of the action at level n reduces to the scalar at level i.

Equations

• TauCeti.ZModTwist.mulPow χ h = { toFun := fun (x : TauCeti.ZModTwist χ i) => { val := (ZMod.mulCastHom (p ^ j) ⋯) x.val }, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem TauCeti.ZModTwist.val_mulPow {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) {i j n : ℕ} (h : i + j = n) (x : ZModTwist χ i) : ((mulPow χ h) x).val = (ZMod.mulCastHom (p ^ j) ⋯) x.val

The residue class of pʲ x is pʲ times the residue class of x.

theorem TauCeti.ZModTwist.mulPow_injective {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) {i j n : ℕ} (h : i + j = n) : Function.Injective ⇑(mulPow χ h)

Multiplication by pʲ is injective on I(χ)/pⁱ.

@[simp]

theorem TauCeti.ZModTwist.mulPow_zero {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) {i : ℕ} : mulPow χ ⋯ = DistribMulActionHom.id G

Multiplication by p⁰ is the identity.

theorem TauCeti.ZModTwist.mulPow_mulPow {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) {i j n k m : ℕ} (h : i + j = n) (h' : n + k = m) (h'' : i + (j + k) = m) (x : ZModTwist χ i) : (mulPow χ h') ((mulPow χ h) x) = (mulPow χ h'') x

Two successive multiplications, by pʲ and then by pᵏ, compose to the multiplication by pʲ⁺ᵏ. The index equation of the composite is taken as a hypothesis, so that any proof of it may be used.

@[simp]

theorem TauCeti.ZModTwist.reduce_mulPow {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) {i j n : ℕ} (h : i + j = n) (x : ZModTwist χ i) : (reduce χ ⋯) ((mulPow χ h) x) = 0

The reduction modulo pʲ kills the image of the multiplication by pʲ.

@[simp]

theorem TauCeti.ZModTwist.mulPow_reduce {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) {i j n : ℕ} (h : i + j = n) (y : ZModTwist χ n) : (mulPow χ h) ((reduce χ ⋯) y) = p ^ j • y

Multiplying by pʲ after reducing from level n to level i, i + j = n, is multiplication by pʲ on I(χ)/pⁿ.

theorem TauCeti.ZModTwist.reduce_mulPow_eq_mulPow_reduce {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) {i j n i' n' : ℕ} (h : i + j = n) (h' : i' + j = n') (hi : i' ≤ i) (hn : n' ≤ n) (x : ZModTwist χ i) : (reduce χ hn) ((mulPow χ h) x) = (mulPow χ h') ((reduce χ hi) x)

The reductions commute with the multiplications: reducing pʲ x from level n to level n' is pʲ times the reduction of x from level i to level i', when i + j = n and i' + j = n'.

theorem TauCeti.ZModTwist.reduce_comp_reduce {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) {i j k : ℕ} (h₁ : j ≤ i) (h₂ : k ≤ j) : (reduce χ h₂).comp (reduce χ h₁) = reduce χ ⋯

Two successive reductions compose to the reduction between the outer levels, as equivariant homomorphisms.

theorem TauCeti.ZModTwist.reduce_comp_mulPow {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) {i j n i' n' : ℕ} (h : i + j = n) (h' : i' + j = n') (hi : i' ≤ i) (hn : n' ≤ n) : (reduce χ hn).comp (mulPow χ h) = (mulPow χ h').comp (reduce χ hi)

reduce_mulPow_eq_mulPow_reduce, as an equality of equivariant homomorphisms.

The short exact sequences 0 → I(χ)/pⁱ → I(χ)/pⁱ⁺ʲ → I(χ)/pʲ → 0

def TauCeti.ZModTwist.shortExact {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) {i j n : ℕ} (h : i + j = n) : ContCohomology.DiscreteShortExact G (ZModTwist χ i) (ZModTwist χ n) (ZModTwist χ j)

The short exact sequence 0 → I(χ)/pⁱ → I(χ)/pⁿ → I(χ)/pʲ → 0 of discrete G-modules, for i + j = n: multiplication by pʲ followed by reduction modulo pʲ.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.ZModTwist.shortExact_incl_apply {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) {i j n : ℕ} (h : i + j = n) (x : ZModTwist χ i) : (shortExact χ h).incl x = (mulPow χ h) x

The inclusion of shortExact multiplies by pʲ.

@[simp]

theorem TauCeti.ZModTwist.shortExact_proj_apply {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) {i j n : ℕ} (h : i + j = n) (y : ZModTwist χ n) : (shortExact χ h).proj y = (reduce χ ⋯) y

The projection of shortExact reduces modulo pʲ.

theorem TauCeti.ZModTwist.shortExact_inclDistribMulActionHom {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) {i j n : ℕ} (h : i + j = n) : (shortExact χ h).inclDistribMulActionHom = mulPow χ h

The inclusion of shortExact is the multiplication by pʲ.

theorem TauCeti.ZModTwist.shortExact_projDistribMulActionHom {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) {i j n : ℕ} (h : i + j = n) : (shortExact χ h).projDistribMulActionHom = reduce χ ⋯

The projection of shortExact is the reduction modulo pʲ.

theorem TauCeti.ZModTwist.exists_mulPow_eq_of_nsmul_eq_zero {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) {i j n : ℕ} (h : i + j = n) {y : ZModTwist χ n} (hy : p ^ i • y = 0) : ∃ (x : ZModTwist χ i), (mulPow χ h) x = y

The pⁱ-torsion of I(χ)/pⁿ is the image of I(χ)/pⁱ, for i + j = n: an element killed by pⁱ is a multiple of pʲ.

Homomorphisms between two twists

A group element g acts on every level I(χ)/pⁱ with i ≤ n as the natural number (χ g mod pⁿ).val, so an additive homomorphism between two twists commutes with the action: the conjugation action on Hom(I(χ)/pⁱ, I(χ)/pⁿ) is trivial, and every such homomorphism is invariant. With Baer's criterion for I(χ)/pⁿ, every invariant homomorphism I(χ)/pⁱ → I(χ)/pⁿ is then the restriction along the multiplication by pʲ of an invariant endomorphism of I(χ)/pⁿ.

theorem TauCeti.ZModTwist.smul_eq_nsmul_val_charScalar {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) {i n : ℕ} (h : i ≤ n) (g : G) (x : ZModTwist χ i) : g • x = ((charScalar χ n) g).val • x

At every level i ≤ n, g acts on I(χ)/pⁱ as the natural number (χ g mod pⁿ).val.

@[simp]

theorem TauCeti.ZModTwist.smul_internalHom_eq_self {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) {i n : ℕ} (g : G) (φ : InternalHom G (ZModTwist χ i) (ZModTwist χ n)) : g • φ = φ

The conjugation action on the homomorphisms between two twists is trivial: g acts on I(χ)/pⁱ and on I(χ)/pⁿ by one and the same natural number, with which every additive homomorphism commutes.

@[simp]

theorem TauCeti.ZModTwist.H0_internalHom_eq_top {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) {i n : ℕ} : ContCohomology.H0 G (InternalHom G (ZModTwist χ i) (ZModTwist χ n)) = ⊤

Every homomorphism between two twists is invariant.

theorem TauCeti.ZModTwist.surjective_explicitCoeff0_precomp_mulPow {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) {i j n : ℕ} (h : i + j = n) : Function.Surjective ⇑(ContCohomology.explicitCoeff0 G (InternalHom G (ZModTwist χ n) (ZModTwist χ n)) (InternalHom.precomp G (mulPow χ h)))

Every invariant homomorphism I(χ)/pⁱ → I(χ)/pⁿ is the restriction along the multiplication by pʲ of an invariant endomorphism of I(χ)/pⁿ, for i + j = n: an extension exists by Baer's criterion for I(χ)/pⁿ over ℤ/pⁿ, and it is invariant because every endomorphism of a twist is.

The induced maps on H¹

The reductions and multiplications induce maps on the explicit first continuous cohomology, and their composition laws pass to those maps. Both continuity proofs are the generic continuous_of_discreteTopology, which is what lets an equality of coefficient maps be transported across explicitCoeff1 by congrArg.

theorem TauCeti.ZModTwist.explicitCoeff1_reduce_explicitCoeff1_reduce {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) {i j k : ℕ} (h₁ : j ≤ i) (h₂ : k ≤ j) (x : ContCohomology.H1 G (ZModTwist χ i)) : (ContCohomology.explicitCoeff1 G (ZModTwist χ j) (reduce χ h₂) ⋯) ((ContCohomology.explicitCoeff1 G (ZModTwist χ i) (reduce χ h₁) ⋯) x) = (ContCohomology.explicitCoeff1 G (ZModTwist χ i) (reduce χ ⋯) ⋯) x

Two successive reductions on H¹ compose to the reduction between the outer levels.

theorem TauCeti.ZModTwist.explicitCoeff1_reduce_explicitCoeff1_mulPow {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) {i j n i' n' : ℕ} (h : i + j = n) (h' : i' + j = n') (hi : i' ≤ i) (hn : n' ≤ n) (x : ContCohomology.H1 G (ZModTwist χ i)) : (ContCohomology.explicitCoeff1 G (ZModTwist χ n) (reduce χ hn) ⋯) ((ContCohomology.explicitCoeff1 G (ZModTwist χ i) (mulPow χ h) ⋯) x) = (ContCohomology.explicitCoeff1 G (ZModTwist χ i') (mulPow χ h') ⋯) ((ContCohomology.explicitCoeff1 G (ZModTwist χ i) (reduce χ hi) ⋯) x)

On H¹, reducing after multiplying by pʲ is multiplying by pʲ after reducing.

The induced maps on H²

theorem TauCeti.ZModTwist.explicitCoeff2_reduce_explicitCoeff2_reduce {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) {i : ℕ} [ContinuousMul G] {j k : ℕ} (h₁ : j ≤ i) (h₂ : k ≤ j) (x : ContCohomology.H2 G (ZModTwist χ i)) : (ContCohomology.explicitCoeff2 G (ZModTwist χ j) (reduce χ h₂) ⋯) ((ContCohomology.explicitCoeff2 G (ZModTwist χ i) (reduce χ h₁) ⋯) x) = (ContCohomology.explicitCoeff2 G (ZModTwist χ i) (reduce χ ⋯) ⋯) x

Two successive reductions on H² compose to the reduction between the outer levels.

theorem TauCeti.ZModTwist.explicitCoeff2_mulPow_explicitCoeff2_reduce {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) {i j n : ℕ} [ContinuousMul G] (h : i + j = n) (x : ContCohomology.H2 G (ZModTwist χ n)) : (ContCohomology.explicitCoeff2 G (ZModTwist χ i) (mulPow χ h) ⋯) ((ContCohomology.explicitCoeff2 G (ZModTwist χ n) (reduce χ ⋯) ⋯) x) = p ^ j • x

On H², multiplying by pʲ after reducing from level n to level i, i + j = n, is multiplication by pʲ.

The bottom level I(χ)/p of a pro-p group

theorem TauCeti.IsProP.charScalar_one_eq_one {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) (hG : IsProP p G) (g : G) : (charScalar χ 1) g = 1

A pro-p group acts trivially on I(χ)/p: the scalar χ g mod p is 1, because a continuous character of a pro-p group takes values in the principal units 1 + pℤ_p.

@[simp]

theorem TauCeti.IsProP.smul_zModTwist_one_eq_self {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) (hG : IsProP p G) (g : G) (x : ZModTwist χ 1) : g • x = x

The action of a pro-p group on the bottom level I(χ)/p of the twisted coefficients is trivial.