Reduction of p-adic group-algebra modules

Reduction of coefficients gives a surjective ring homomorphism ℤ_p[G] → 𝔽_p[G]. Its kernel is the ideal generated by p; hence it identifies the quotient ℤ_p[G] / (p) with 𝔽_p[G]. Transporting scalars across this equivalence gives the quotient M / pM of any ℤ_p[G]-module its canonical 𝔽_p[G]-module structure.

This is the coefficient-reduction bridge needed to compare projective integral lattices with modular representations in Swan's rational detection theorem. The quotient map is packaged as a semilinear map, and its scalar action and kernel are recorded explicitly. Projectivity of the reduction is the special case of RingHom.projective_quotient_smul_top for coefficient reduction.

Reduction is functorial for isomorphisms, and it commutes with restriction along a monoid homomorphism f : G →* H: the reduction of a ℤ_p[H]-module over G is its reduction over H, with 𝔽_p[G] acting through f. Restriction to a cyclic subgroup is how Swan's theorem reaches its prime-to-p case.

Main results

• TauCeti.padicMonoidAlgebraQuotientEquiv: ℤ_p[G] / (p) ≃+* 𝔽_p[G].
• TauCeti.padicReductionModule: the canonical 𝔽_p[G]-module structure on M / pM.
• TauCeti.padicReductionMk: the quotient map, semilinear along coefficient reduction.
• TauCeti.padicReduction_module_finite: reduction preserves finite generation.
• TauCeti.padicReduction_module_projective: reduction preserves projectivity.
• TauCeti.padicReduction_compatibleSMul_padicInt, TauCeti.padicReduction_compatibleSMul_zmod: on modules where ℤ_p[G] acts through 𝔽_p[G], the two notions of linearity agree.
• TauCeti.padicReductionCongr: reduction of a ℤ_p[G]-linear equivalence.
• TauCeti.padicReductionLinearEquivOfBijective: a bijective semilinear map out of the reduction is an 𝔽_p[G]-linear equivalence.
• TauCeti.padicReductionRestrictLinearEquiv: reduction commutes with restriction along a monoid homomorphism G →* H.
• TauCeti.compPadicReductionMk: a semilinear map out of the reduction, precomposed with the quotient map and read as semilinear along ℤ_p → 𝔽_p.

References

• J.-P. Serre, Linear Representations of Finite Groups, Part III, §§14–16.
• R. G. Swan, Induced representations and projective modules, Ann. of Math. 71 (1960).

theorem TauCeti.ker_padicMonoidAlgebraReduction (p : ℕ) [Fact (Nat.Prime p)] (G : Type u) [Monoid G] : RingHom.ker (MonoidAlgebra.mapRingHom G PadicInt.toZMod) = Ideal.span {↑p}

The kernel of coefficientwise reduction ℤ_p[G] → 𝔽_p[G] is the ideal generated by p.

theorem TauCeti.padicMonoidAlgebraReduction_surjective (p : ℕ) [Fact (Nat.Prime p)] (G : Type u) [Monoid G] : Function.Surjective ⇑(MonoidAlgebra.mapRingHom G PadicInt.toZMod)

Coefficientwise reduction ℤ_p[G] → 𝔽_p[G] is surjective.

noncomputable def TauCeti.padicMonoidAlgebraQuotientEquiv (p : ℕ) [Fact (Nat.Prime p)] (G : Type u) [Monoid G] : MonoidAlgebra ℤ_[p] G ⧸ RingHom.ker (MonoidAlgebra.mapRingHom G PadicInt.toZMod) ≃+* MonoidAlgebra (ZMod p) G

The group algebra modulo p is the group algebra over 𝔽_p.

@[simp]

theorem TauCeti.padicMonoidAlgebraQuotientEquiv_mk (p : ℕ) [Fact (Nat.Prime p)] (G : Type u) [Monoid G] (x : MonoidAlgebra ℤ_[p] G) : (padicMonoidAlgebraQuotientEquiv p G) ((Ideal.Quotient.mk (RingHom.ker (MonoidAlgebra.mapRingHom G PadicInt.toZMod))) x) = (MonoidAlgebra.mapRingHom G PadicInt.toZMod) x

@[simp]

theorem TauCeti.padicMonoidAlgebraQuotientEquiv_symm_apply (p : ℕ) [Fact (Nat.Prime p)] (G : Type u) [Monoid G] (x : MonoidAlgebra ℤ_[p] G) : (padicMonoidAlgebraQuotientEquiv p G).symm ((MonoidAlgebra.mapRingHom G PadicInt.toZMod) x) = (Ideal.Quotient.mk (RingHom.ker (MonoidAlgebra.mapRingHom G PadicInt.toZMod))) x

The inverse of padicMonoidAlgebraQuotientEquiv sends the reduction of x to the class of x modulo p.

@[instance_reducible]

noncomputable def TauCeti.padicReductionModule (p : ℕ) [Fact (Nat.Prime p)] (G : Type u) [Monoid G] (M : Type v) [AddCommGroup M] [Module (MonoidAlgebra ℤ_[p] G) M] : Module (MonoidAlgebra (ZMod p) G) (M ⧸ Ideal.span {↑p} • ⊤)

The canonical 𝔽_p[G]-module structure on the reduction of a ℤ_p[G]-module. The action is transported from the natural ℤ_p[G]/(p)-action using padicMonoidAlgebraQuotientEquiv.

@[simp]

theorem TauCeti.padicReduction_smul (p : ℕ) [Fact (Nat.Prime p)] (G : Type u) [Monoid G] (M : Type v) [AddCommGroup M] [Module (MonoidAlgebra ℤ_[p] G) M] (a : MonoidAlgebra ℤ_[p] G) (q : M ⧸ Ideal.span {↑p} • ⊤) : (MonoidAlgebra.mapRingHom G PadicInt.toZMod) a • q = a • q

Scalar multiplication on the reduction is induced by coefficientwise reduction.

noncomputable def TauCeti.padicReductionMk (p : ℕ) [Fact (Nat.Prime p)] (G : Type u) [Monoid G] (M : Type v) [AddCommGroup M] [Module (MonoidAlgebra ℤ_[p] G) M] : M →ₛₗ[MonoidAlgebra.mapRingHom G PadicInt.toZMod] M ⧸ Ideal.span {↑p} • ⊤

The quotient map to the modular reduction, semilinear along coefficient reduction.

@[simp]

theorem TauCeti.padicReductionMk_apply (p : ℕ) [Fact (Nat.Prime p)] (G : Type u) [Monoid G] (M : Type v) [AddCommGroup M] [Module (MonoidAlgebra ℤ_[p] G) M] (x : M) : (padicReductionMk p G M) x = Submodule.Quotient.mk x

theorem TauCeti.padicReductionMk_surjective (p : ℕ) [Fact (Nat.Prime p)] (G : Type u) [Monoid G] (M : Type v) [AddCommGroup M] [Module (MonoidAlgebra ℤ_[p] G) M] : Function.Surjective ⇑(padicReductionMk p G M)

The modular reduction map is surjective.

theorem TauCeti.padicReductionMk_eq_zero_iff (p : ℕ) [Fact (Nat.Prime p)] (G : Type u) [Monoid G] (M : Type v) [AddCommGroup M] [Module (MonoidAlgebra ℤ_[p] G) M] (x : M) : (padicReductionMk p G M) x = 0 ↔ x ∈ Ideal.span {↑p} • ⊤

The modular reduction map vanishes exactly on p • M, the submodule generated by the ideal (p).

theorem TauCeti.padicReduction_module_finite (p : ℕ) [Fact (Nat.Prime p)] (G : Type u) [Monoid G] (M : Type v) [AddCommGroup M] [Module (MonoidAlgebra ℤ_[p] G) M] [Module.Finite (MonoidAlgebra ℤ_[p] G) M] : Module.Finite (MonoidAlgebra (ZMod p) G) (M ⧸ Ideal.span {↑p} • ⊤)

Reduction of a finite group-algebra module is finite over the reduced group algebra.

theorem TauCeti.padicReduction_module_projective (p : ℕ) [Fact (Nat.Prime p)] (G : Type u) [Monoid G] (M : Type v) [AddCommGroup M] [Module (MonoidAlgebra ℤ_[p] G) M] [Module.Projective (MonoidAlgebra ℤ_[p] G) M] : Module.Projective (MonoidAlgebra (ZMod p) G) (M ⧸ Ideal.span {↑p} • ⊤)

Reduction modulo p preserves projectivity. A projective ℤ_p[G]-module reduces to a projective 𝔽_p[G]-module.

theorem TauCeti.padicReduction_compatibleSMul_padicInt (p : ℕ) [Fact (Nat.Prime p)] (G : Type u) [Monoid G] {P : Type u_1} {Q : Type u_2} [AddCommMonoid P] [SMul (MonoidAlgebra ℤ_[p] G) P] [Module (MonoidAlgebra (ZMod p) G) P] [AddCommMonoid Q] [SMul (MonoidAlgebra ℤ_[p] G) Q] [Module (MonoidAlgebra (ZMod p) G) Q] (hP : ∀ (a : MonoidAlgebra ℤ_[p] G) (x : P), (MonoidAlgebra.mapRingHom G PadicInt.toZMod) a • x = a • x) (hQ : ∀ (a : MonoidAlgebra ℤ_[p] G) (y : Q), (MonoidAlgebra.mapRingHom G PadicInt.toZMod) a • y = a • y) : LinearMap.CompatibleSMul P Q (MonoidAlgebra ℤ_[p] G) (MonoidAlgebra (ZMod p) G)

A 𝔽_p[G]-linear map preserves ℤ_p[G]-scalar multiplication when the integral actions on its domain and codomain factor through coefficient reduction.

theorem TauCeti.padicReduction_compatibleSMul_zmod (p : ℕ) [Fact (Nat.Prime p)] (G : Type u) [Monoid G] {P : Type u_1} {Q : Type u_2} [AddCommMonoid P] [Module (MonoidAlgebra ℤ_[p] G) P] [SMul (MonoidAlgebra (ZMod p) G) P] [AddCommMonoid Q] [Module (MonoidAlgebra ℤ_[p] G) Q] [SMul (MonoidAlgebra (ZMod p) G) Q] (hP : ∀ (a : MonoidAlgebra ℤ_[p] G) (x : P), (MonoidAlgebra.mapRingHom G PadicInt.toZMod) a • x = a • x) (hQ : ∀ (a : MonoidAlgebra ℤ_[p] G) (y : Q), (MonoidAlgebra.mapRingHom G PadicInt.toZMod) a • y = a • y) : LinearMap.CompatibleSMul P Q (MonoidAlgebra (ZMod p) G) (MonoidAlgebra ℤ_[p] G)

A ℤ_p[G]-linear map preserves 𝔽_p[G]-scalar multiplication when the integral actions on its domain and codomain factor through coefficient reduction.

noncomputable def TauCeti.padicReductionCongr (p : ℕ) [Fact (Nat.Prime p)] (G : Type u) [Monoid G] {M : Type v} [AddCommGroup M] [Module (MonoidAlgebra ℤ_[p] G) M] {N : Type u_1} [AddCommGroup N] [Module (MonoidAlgebra ℤ_[p] G) N] (e : M ≃ₗ[MonoidAlgebra ℤ_[p] G] N) : (M ⧸ Ideal.span {↑p} • ⊤) ≃ₗ[MonoidAlgebra (ZMod p) G] N ⧸ Ideal.span {↑p} • ⊤

Reduction modulo p of an isomorphism. A ℤ_p[G]-linear equivalence M ≃ N induces an 𝔽_p[G]-linear equivalence M / pM ≃ N / pN.

@[simp]

theorem TauCeti.padicReductionCongr_mk (p : ℕ) [Fact (Nat.Prime p)] (G : Type u) [Monoid G] {M : Type v} [AddCommGroup M] [Module (MonoidAlgebra ℤ_[p] G) M] {N : Type u_1} [AddCommGroup N] [Module (MonoidAlgebra ℤ_[p] G) N] (e : M ≃ₗ[MonoidAlgebra ℤ_[p] G] N) (x : M) : (padicReductionCongr p G e) (Submodule.Quotient.mk x) = Submodule.Quotient.mk (e x)

noncomputable def TauCeti.padicReductionLinearEquivOfBijective (p : ℕ) [Fact (Nat.Prime p)] (G : Type u) [Monoid G] {M : Type v} [AddCommGroup M] [Module (MonoidAlgebra ℤ_[p] G) M] {Y : Type u_2} [AddCommMonoid Y] [Module (MonoidAlgebra (ZMod p) G) Y] (f : M ⧸ Ideal.span {↑p} • ⊤ →ₛₗ[MonoidAlgebra.mapRingHom G PadicInt.toZMod] Y) (hf : Function.Bijective ⇑f) : (M ⧸ Ideal.span {↑p} • ⊤) ≃ₗ[MonoidAlgebra (ZMod p) G] Y

A bijective map out of the reduction M / pM, semilinear along coefficient reduction, is an 𝔽_p[G]-linear equivalence.

@[simp]

theorem TauCeti.padicReductionLinearEquivOfBijective_apply (p : ℕ) [Fact (Nat.Prime p)] (G : Type u) [Monoid G] {M : Type v} [AddCommGroup M] [Module (MonoidAlgebra ℤ_[p] G) M] {Y : Type u_2} [AddCommMonoid Y] [Module (MonoidAlgebra (ZMod p) G) Y] (f : M ⧸ Ideal.span {↑p} • ⊤ →ₛₗ[MonoidAlgebra.mapRingHom G PadicInt.toZMod] Y) (hf : Function.Bijective ⇑f) (x : M ⧸ Ideal.span {↑p} • ⊤) : (padicReductionLinearEquivOfBijective p G f hf) x = f x

theorem TauCeti.padicReduction_smul_of_mapDomain (p : ℕ) [Fact (Nat.Prime p)] (G : Type u) [Monoid G] {H : Type u_2} [Monoid H] (f : G →* H) (X : Type u_3) [AddCommGroup X] [Module (MonoidAlgebra ℤ_[p] H) X] [SMul (MonoidAlgebra ℤ_[p] G) (MonoidAlgebra ℤ_[p] H)] [SMul (MonoidAlgebra ℤ_[p] G) X] [IsScalarTower (MonoidAlgebra ℤ_[p] G) (MonoidAlgebra ℤ_[p] H) X] [SMul (MonoidAlgebra (ZMod p) G) (X ⧸ Ideal.span {↑p} • ⊤)] (hscalar : ∀ (a : MonoidAlgebra ℤ_[p] G) (b : MonoidAlgebra ℤ_[p] H), a • b = (MonoidAlgebra.mapDomainRingHom ℤ_[p] f) a * b) (hk : ∀ (b : MonoidAlgebra (ZMod p) G) (q : X ⧸ Ideal.span {↑p} • ⊤), b • q = (MonoidAlgebra.mapDomainRingHom (ZMod p) f) b • q) (a : MonoidAlgebra ℤ_[p] G) (q : X ⧸ Ideal.span {↑p} • ⊤) : (MonoidAlgebra.mapRingHom G PadicInt.toZMod) a • q = a • q

Let ℤ_p[G] act on a ℤ_p[H]-module X along f : G →* H, and let 𝔽_p[G] act on the reduction X / pX through f. Then ℤ_p[G] acts on X / pX through coefficient reduction.

noncomputable def TauCeti.padicReductionRestrictLinearEquiv (p : ℕ) [Fact (Nat.Prime p)] (G : Type u) [Monoid G] {H : Type u_2} [Monoid H] (f : G →* H) (X : Type u_3) [AddCommGroup X] [Module (MonoidAlgebra ℤ_[p] H) X] [SMul (MonoidAlgebra ℤ_[p] G) (MonoidAlgebra ℤ_[p] H)] [Module (MonoidAlgebra ℤ_[p] G) X] [IsScalarTower (MonoidAlgebra ℤ_[p] G) (MonoidAlgebra ℤ_[p] H) X] [Module (MonoidAlgebra (ZMod p) G) (X ⧸ Ideal.span {↑p} • ⊤)] (hscalar : ∀ (a : MonoidAlgebra ℤ_[p] G) (b : MonoidAlgebra ℤ_[p] H), a • b = (MonoidAlgebra.mapDomainRingHom ℤ_[p] f) a * b) (hk : ∀ (b : MonoidAlgebra (ZMod p) G) (q : X ⧸ Ideal.span {↑p} • ⊤), b • q = (MonoidAlgebra.mapDomainRingHom (ZMod p) f) b • q) : (X ⧸ Ideal.span {↑p} • ⊤) ≃ₗ[MonoidAlgebra (ZMod p) G] X ⧸ Ideal.span {↑p} • ⊤

Reduction modulo p commutes with restriction along f : G →* H. For a ℤ_p[H]-module X, viewed as a ℤ_p[G]-module along f, the reduction of X over G is the reduction of X over H, with 𝔽_p[G] acting through f.

@[simp]

theorem TauCeti.padicReductionRestrictLinearEquiv_mk (p : ℕ) [Fact (Nat.Prime p)] (G : Type u) [Monoid G] {H : Type u_2} [Monoid H] (f : G →* H) (X : Type u_3) [AddCommGroup X] [Module (MonoidAlgebra ℤ_[p] H) X] [SMul (MonoidAlgebra ℤ_[p] G) (MonoidAlgebra ℤ_[p] H)] [Module (MonoidAlgebra ℤ_[p] G) X] [IsScalarTower (MonoidAlgebra ℤ_[p] G) (MonoidAlgebra ℤ_[p] H) X] [Module (MonoidAlgebra (ZMod p) G) (X ⧸ Ideal.span {↑p} • ⊤)] (hscalar : ∀ (a : MonoidAlgebra ℤ_[p] G) (b : MonoidAlgebra ℤ_[p] H), a • b = (MonoidAlgebra.mapDomainRingHom ℤ_[p] f) a * b) (hk : ∀ (b : MonoidAlgebra (ZMod p) G) (q : X ⧸ Ideal.span {↑p} • ⊤), b • q = (MonoidAlgebra.mapDomainRingHom (ZMod p) f) b • q) (x : X) : (padicReductionRestrictLinearEquiv p G f X hscalar hk) (Submodule.Quotient.mk x) = Submodule.Quotient.mk x

noncomputable def TauCeti.compPadicReductionMk (p : ℕ) [Fact (Nat.Prime p)] (G : Type u) [Monoid G] {M : Type v} [AddCommGroup M] [Module (MonoidAlgebra ℤ_[p] G) M] [Module ℤ_[p] M] [IsScalarTower ℤ_[p] (MonoidAlgebra ℤ_[p] G) M] {Y : Type u_2} [AddCommMonoid Y] [Module (ZMod p) Y] [Module (MonoidAlgebra (ZMod p) G) Y] [IsScalarTower (ZMod p) (MonoidAlgebra (ZMod p) G) Y] (f : M ⧸ Ideal.span {↑p} • ⊤ →ₛₗ[MonoidAlgebra.mapRingHom G PadicInt.toZMod] Y) : M →ₛₗ[PadicInt.toZMod] Y

A map f out of the reduction M / pM, semilinear along coefficient reduction ℤ_p[G] → 𝔽_p[G], composed with the quotient map M → M / pM. Forgetting the group, the composite is semilinear along ℤ_p → 𝔽_p.

@[simp]

theorem TauCeti.compPadicReductionMk_apply (p : ℕ) [Fact (Nat.Prime p)] (G : Type u) [Monoid G] {M : Type v} [AddCommGroup M] [Module (MonoidAlgebra ℤ_[p] G) M] [Module ℤ_[p] M] [IsScalarTower ℤ_[p] (MonoidAlgebra ℤ_[p] G) M] {Y : Type u_2} [AddCommMonoid Y] [Module (ZMod p) Y] [Module (MonoidAlgebra (ZMod p) G) Y] [IsScalarTower (ZMod p) (MonoidAlgebra (ZMod p) G) Y] (f : M ⧸ Ideal.span {↑p} • ⊤ →ₛₗ[MonoidAlgebra.mapRingHom G PadicInt.toZMod] Y) (x : M) : (compPadicReductionMk p G f) x = f ((padicReductionMk p G M) x)

theorem TauCeti.compPadicReductionMk_surjective (p : ℕ) [Fact (Nat.Prime p)] (G : Type u) [Monoid G] {M : Type v} [AddCommGroup M] [Module (MonoidAlgebra ℤ_[p] G) M] [Module ℤ_[p] M] [IsScalarTower ℤ_[p] (MonoidAlgebra ℤ_[p] G) M] {Y : Type u_2} [AddCommMonoid Y] [Module (ZMod p) Y] [Module (MonoidAlgebra (ZMod p) G) Y] [IsScalarTower (ZMod p) (MonoidAlgebra (ZMod p) G) Y] (f : M ⧸ Ideal.span {↑p} • ⊤ →ₛₗ[MonoidAlgebra.mapRingHom G PadicInt.toZMod] Y) (hf : Function.Surjective ⇑f) : Function.Surjective ⇑(compPadicReductionMk p G f)

For surjective f, the composite compPadicReductionMk is surjective.

theorem TauCeti.compPadicReductionMk_eq_zero_iff (p : ℕ) [Fact (Nat.Prime p)] (G : Type u) [Monoid G] {M : Type v} [AddCommGroup M] [Module (MonoidAlgebra ℤ_[p] G) M] [Module ℤ_[p] M] [IsScalarTower ℤ_[p] (MonoidAlgebra ℤ_[p] G) M] {Y : Type u_2} [AddCommMonoid Y] [Module (ZMod p) Y] [Module (MonoidAlgebra (ZMod p) G) Y] [IsScalarTower (ZMod p) (MonoidAlgebra (ZMod p) G) Y] (f : M ⧸ Ideal.span {↑p} • ⊤ →ₛₗ[MonoidAlgebra.mapRingHom G PadicInt.toZMod] Y) (hf : Function.Injective ⇑f) (x : M) : (compPadicReductionMk p G f) x = 0 ↔ x ∈ ↑p • ⊤

For injective f, the composite compPadicReductionMk vanishes exactly on pM.

theorem TauCeti.compPadicReductionMk_ofModule' (p : ℕ) [Fact (Nat.Prime p)] (G : Type u) [Monoid G] {M : Type v} [AddCommGroup M] [Module (MonoidAlgebra ℤ_[p] G) M] [Module ℤ_[p] M] [IsScalarTower ℤ_[p] (MonoidAlgebra ℤ_[p] G) M] {Y : Type u_2} [AddCommMonoid Y] [Module (ZMod p) Y] [Module (MonoidAlgebra (ZMod p) G) Y] [IsScalarTower (ZMod p) (MonoidAlgebra (ZMod p) G) Y] (f : M ⧸ Ideal.span {↑p} • ⊤ →ₛₗ[MonoidAlgebra.mapRingHom G PadicInt.toZMod] Y) (g : G) (x : M) : (compPadicReductionMk p G f) (((Representation.ofModule' M) g) x) = ((Representation.ofModule' Y) g) ((compPadicReductionMk p G f) x)

The composite compPadicReductionMk is equivariant for the group actions.