Free actions of finite groups on rings

Let a finite group G act on a commutative R-algebra A by R-algebra automorphisms, and suppose that R is the ring of invariants (Algebra.IsInvariant R A G), for instance R = Aᴳ. The action of G on Spec A is free when no g ≠ 1 fixes a geometric point. The fixed locus of g is the closed subscheme cut out by the elements g • a - a, so freeness says that for every g ≠ 1 these elements generate the unit ideal of A.

This file proves the theorem of Chase, Harrison and Rosenberg that a free action makes A a Galois extension of R with group G: the map

A ⊗[R] A → (G → A), a ⊗ b ↦ (a * g • b)_g

(TauCeti.MulSemiringAction.tensorToPi) is an isomorphism, A is a finite R-module, and A is formally unramified over R. If moreover R → A is injective, as for R = Aᴳ, then A is a projective, faithfully flat and étale R-algebra. Geometrically, Spec A → Spec Aᴳ is then a finite étale surjection, and Spec A ×_{Spec Aᴳ} Spec A is the disjoint union of |G| copies of Spec A, the copy indexed by g mapping by the identity to the first factor and by the automorphism induced by g to the second. This is the input that makes the affine invariant quotient by a free action of a finite group a finite locally free quotient.

Surjectivity of tensorToPi is equivalent to freeness, for any R (TauCeti.MulSemiringAction.tensorToPi_surjective_iff). Freeness gives, for each g ≠ 1, an element of A ⊗[R] A whose components at 1 and at g are 1 and 0, and the product of these elements over all g ≠ 1 maps to the indicator function of 1. Writing that product as ∑ i, xᵢ ⊗ yᵢ, so that ∑ i, xᵢ * g • yᵢ is 1 for g = 1 and 0 otherwise, every b : A is b = ∑ i, (∑ g, g • (yᵢ * b)) * xᵢ, where each ∑ g, g • (yᵢ * b) is invariant and so comes from R. This identity shows that A is a finite R-module and that tensorToPi is injective. When R → A is injective the coefficients ∑ g, g • (yᵢ * b) have unique, hence R-linear, preimages in R, so the identity is a finite dual basis of A over R and A is projective.

The map tensorToPi and its elementary identities also apply to monoid actions on commutative semirings. The freeness criterion, bijectivity, module finiteness and projectivity allow a commutative semiring as the base, while the algebra carrying the action is a commutative ring. The invariant tensor identity mul_tmul_eq_tmul_mul also allows a noncommutative semiring target.

Main definitions

• TauCeti.MulSemiringAction.tensorToPi R A G: the A-algebra map A ⊗[R] A →ₐ[A] (G → A), a ⊗ b ↦ (a * g • b)_g.

Main results

• TauCeti.MulSemiringAction.tensorToPi_baseChange: tensorToPi commutes with base change, for G acting on A' ⊗[R] A through the right factor.
• TauCeti.MulSemiringAction.bijective_tensorToPi_baseChange_iff: for a finite monoid and a faithfully flat R → A', tensorToPi for A' ⊗[R] A is bijective exactly when it is for A.
• TauCeti.MulSemiringAction.tensorToPi_surjective_iff: tensorToPi is surjective exactly when the action is free.
• TauCeti.MulSemiringAction.tensorToPi_bijective: for a free action with invariant ring R, tensorToPi is bijective.
• TauCeti.MulSemiringAction.moduleFinite, TauCeti.MulSemiringAction.projective, TauCeti.MulSemiringAction.faithfullyFlat: for a free action with invariant ring R, A is a finite R-module, and if R → A is injective it is projective and faithfully flat.
• TauCeti.MulSemiringAction.formallyUnramified, TauCeti.MulSemiringAction.etale: A is formally unramified over R, and étale if R → A is injective.
• TauCeti.MulSemiringAction.sum_smul_sum_smul_smul: the dual basis identity n = ∑ i, xᵢ • ∑ g, g • (yᵢ • n) for a module with semilinear action.
• TauCeti.MulSemiringAction.exists_sum_smul_eq_one: for a free action on a commutative ring, some element has trace ∑ g, g • c = 1.
• RingHom.sum_mul_sum_smul: pairing a dual basis of tensorToPi with traces, after a map equivariant along π : G' → G, sums the translates by the kernel of π.
• TauCeti.MulSemiringAction.span_range_smul_sub_eq_top_iff: on a finite-type algebra over a field, freeness of g means that g fixes no point valued in an algebraically closed field.

References

• S. U. Chase, D. K. Harrison and A. Rosenberg, Galois theory and Galois cohomology of commutative rings, Mem. Amer. Math. Soc. 52 (1965), 15–33, Theorem 1.3.
• M. Demazure and A. Grothendieck, Schémas en groupes (SGA 3), Exposé V, §4.

noncomputable def TauCeti.MulSemiringAction.tensorToPi (R : Type u_1) (A : Type u_2) (G : Type u_3) [CommSemiring R] [CommSemiring A] [Algebra R A] [Monoid G] [MulSemiringAction G A] [SMulCommClass G R A] : TensorProduct R A A →ₐ[A] G → A

The A-algebra map A ⊗[R] A → (G → A) sending a ⊗ b to g ↦ a * g • b. It is defined for monoid actions on commutative semirings. When A and R are rings and G is a finite group, on spectra it is the morphism from the disjoint union of |G| copies of Spec A to Spec A ×_{Spec R} Spec A whose g-th component is the identity on the first factor and the automorphism of Spec A induced by g on the second.

@[simp]

theorem TauCeti.MulSemiringAction.tensorToPi_tmul {R : Type u_1} {A : Type u_2} {G : Type u_3} [CommSemiring R] [CommSemiring A] [Algebra R A] [Monoid G] [MulSemiringAction G A] [SMulCommClass G R A] (a b : A) (g : G) : (tensorToPi R A G) (a ⊗ₜ[R] b) g = a * g • b

theorem TauCeti.MulSemiringAction.tensorToPi_apply_one {R : Type u_1} {A : Type u_2} {G : Type u_3} [CommSemiring R] [CommSemiring A] [Algebra R A] [Monoid G] [MulSemiringAction G A] [SMulCommClass G R A] (z : TensorProduct R A A) : (tensorToPi R A G) z 1 = (Algebra.TensorProduct.lmul' R) z

The component of tensorToPi at the identity is multiplication A ⊗[R] A → A.

theorem TauCeti.MulSemiringAction.tensorToPi_map_toAlgHom {R : Type u_1} {A : Type u_2} {G : Type u_3} [CommSemiring R] [CommSemiring A] [Algebra R A] [Monoid G] [MulSemiringAction G A] [SMulCommClass G R A] (k : G) (z : TensorProduct R A A) (g : G) : (tensorToPi R A G) ((Algebra.TensorProduct.map (AlgHom.id R A) (MulSemiringAction.toAlgHom R A k)) z) g = (tensorToPi R A G) z (g * k)

Twisting the right factor by k shifts the components of tensorToPi by k.

theorem TauCeti.MulSemiringAction.tensorToPi_baseChange {R : Type u_1} {A : Type u_2} {G : Type u_3} [CommSemiring R] [CommSemiring A] [Algebra R A] [Monoid G] [MulSemiringAction G A] [SMulCommClass G R A] (A' : Type u_4) [CommSemiring A'] [Algebra R A'] (z : TensorProduct R A' (TensorProduct R A A)) : (tensorToPi A' (TensorProduct R A' A) G) ((Algebra.TensorProduct.baseChangeTensorAlgEquiv R A' A A) z) = (Algebra.TensorProduct.piRightHom R A' A' fun (x : G) => A) ((Algebra.TensorProduct.map (AlgHom.id A' A') (AlgHom.restrictScalars R (tensorToPi R A G))) z)

tensorToPi commutes with base change along R → A', with G acting on A' ⊗[R] A through the right factor: read through A' ⊗[R] (A ⊗[R] A) ≃ (A' ⊗[R] A) ⊗[A'] (A' ⊗[R] A), the map tensorToPi for A' ⊗[R] A is id ⊗ tensorToPi R A G followed by A' ⊗[R] (G → A) → (G → A' ⊗[R] A).

theorem TauCeti.MulSemiringAction.bijective_tensorToPi_baseChange_iff {R : Type u_1} {A : Type u_2} {G : Type u_3} [CommRing R] [CommRing A] [Algebra R A] [Monoid G] [Finite G] [MulSemiringAction G A] [SMulCommClass G R A] (A' : Type u_4) [CommRing A'] [Algebra R A'] [Module.FaithfullyFlat R A'] : Function.Bijective ⇑(tensorToPi A' (TensorProduct R A' A) G) ↔ Function.Bijective ⇑(tensorToPi R A G)

Bijectivity of tensorToPi descends along a faithfully flat extension of the base: for R → A' faithfully flat, the map for A' ⊗[R] A is bijective exactly when the map for A is.

theorem TauCeti.MulSemiringAction.mul_tmul_eq_tmul_mul {R : Type u_1} {A : Type u_2} {G : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Group G] [MulSemiringAction G A] [Algebra.IsInvariant R A G] {c : A} (hc : ∀ (g : G), g • c = c) (a b : A) : (a * c) ⊗ₜ[R] b = a ⊗ₜ[R] (c * b)

An invariant element of A passes through the tensor product over the invariant ring.

theorem TauCeti.MulSemiringAction.sum_smul_sum_smul_smul {A : Type u_1} {G : Type u_2} {N : Type u_3} [Semiring A] [Monoid G] [MulSemiringAction G A] [AddCommMonoid N] [Module A N] [DistribMulAction G N] [SMulDistribClass G A N] [Fintype G] [DecidableEq G] {S : Finset (A × A)} (hS : ∀ (g : G), ∑ p ∈ S, p.1 * g • p.2 = Pi.single 1 1 g) (n : N) : ∑ p ∈ S, p.1 • ∑ g : G, g • p.2 • n = n

The dual basis identity n = ∑ i, xᵢ • ∑ g, g • (yᵢ • n) for an A-module with semilinear action, where ∑ i, xᵢ * g • yᵢ is the indicator function of 1.

theorem TauCeti.MulSemiringAction.tensorToPi_surjective_iff {R : Type u_1} {A : Type u_2} {G : Type u_3} [CommSemiring R] [CommRing A] [Algebra R A] [Group G] [MulSemiringAction G A] [SMulCommClass G R A] [Finite G] : Function.Surjective ⇑(tensorToPi R A G) ↔ ∀ (g : G), g ≠ 1 → Ideal.span (Set.range fun (a : A) => g • a - a) = ⊤

Chase–Harrison–Rosenberg. For a finite group, tensorToPi is surjective exactly when the action is free: for every g ≠ 1, the elements g • a - a generate the unit ideal.

theorem TauCeti.MulSemiringAction.exists_finset_sum_mul_smul {R : Type u_1} {A : Type u_2} {G : Type u_3} [CommSemiring R] [CommRing A] [Algebra R A] [Group G] [MulSemiringAction G A] [SMulCommClass G R A] [DecidableEq G] {u : TensorProduct R A A} (hu : (tensorToPi R A G) u = Pi.single 1 1) : ∃ (S : Finset (A × A)), ∀ (g : G), ∑ p ∈ S, p.1 * g • p.2 = Pi.single 1 1 g

The finite family attached to a preimage of the indicator function of 1 under tensorToPi.

theorem TauCeti.MulSemiringAction.tensorToPi_bijective {R : Type u_1} {A : Type u_2} {G : Type u_3} [CommSemiring R] [CommRing A] [Algebra R A] [Group G] [MulSemiringAction G A] [SMulCommClass G R A] [Algebra.IsInvariant R A G] [Finite G] (hG : ∀ (g : G), g ≠ 1 → Ideal.span (Set.range fun (a : A) => g • a - a) = ⊤) : Function.Bijective ⇑(tensorToPi R A G)

Chase–Harrison–Rosenberg. For a free action of a finite group with invariant ring R, tensorToPi : A ⊗[R] A → (G → A) is bijective.

theorem TauCeti.MulSemiringAction.moduleFinite {R : Type u_1} {A : Type u_2} {G : Type u_3} [CommSemiring R] [CommRing A] [Algebra R A] [Group G] [MulSemiringAction G A] [Algebra.IsInvariant R A G] [Finite G] (hG : ∀ (g : G), g ≠ 1 → Ideal.span (Set.range fun (a : A) => g • a - a) = ⊤) : Module.Finite R A

For a free action of a finite group, A is a finite R-module whenever every fixed point of A lies in the image of R; no compatibility of the action with R is assumed.

theorem TauCeti.MulSemiringAction.projective {R : Type u_1} {A : Type u_2} {G : Type u_3} [CommSemiring R] [CommRing A] [Algebra R A] [Group G] [MulSemiringAction G A] [SMulCommClass G R A] [Algebra.IsInvariant R A G] [Finite G] [FaithfulSMul R A] (hG : ∀ (g : G), g ≠ 1 → Ideal.span (Set.range fun (a : A) => g • a - a) = ⊤) : Module.Projective R A

For a free action of a finite group with invariant ring R, if R → A is injective then A is a projective R-module.

theorem TauCeti.MulSemiringAction.faithfullyFlat {R : Type u_1} {A : Type u_2} {G : Type u_3} [CommRing R] [CommRing A] [Algebra R A] [Group G] [MulSemiringAction G A] [SMulCommClass G R A] [Algebra.IsInvariant R A G] [Finite G] [FaithfulSMul R A] (hG : ∀ (g : G), g ≠ 1 → Ideal.span (Set.range fun (a : A) => g • a - a) = ⊤) : Module.FaithfullyFlat R A

For a free action of a finite group with invariant ring R, if R → A is injective then A is a faithfully flat R-module.

theorem TauCeti.MulSemiringAction.formallyUnramified {R : Type u_1} {A : Type u_2} {G : Type u_3} [CommRing R] [CommRing A] [Algebra R A] [Group G] [MulSemiringAction G A] [SMulCommClass G R A] [Algebra.IsInvariant R A G] [Finite G] (hG : ∀ (g : G), g ≠ 1 → Ideal.span (Set.range fun (a : A) => g • a - a) = ⊤) : Algebra.FormallyUnramified R A

For a free action of a finite group with invariant ring R, A is formally unramified over R.

theorem TauCeti.MulSemiringAction.etale {R : Type u_1} {A : Type u_2} {G : Type u_3} [CommRing R] [CommRing A] [Algebra R A] [Group G] [MulSemiringAction G A] [SMulCommClass G R A] [Algebra.IsInvariant R A G] [Finite G] [FaithfulSMul R A] (hG : ∀ (g : G), g ≠ 1 → Ideal.span (Set.range fun (a : A) => g • a - a) = ⊤) : Algebra.Etale R A

For a free action of a finite group with invariant ring R, if R → A is injective then A is an étale R-algebra.

theorem TauCeti.MulSemiringAction.exists_sum_smul_eq_one {A : Type u_1} {G : Type u_2} [CommRing A] [Group G] [MulSemiringAction G A] [Fintype G] (hG : ∀ (g : G), g ≠ 1 → Ideal.span (Set.range fun (a : A) => g • a - a) = ⊤) : ∃ (c : A), ∑ g : G, g • c = 1

For a free action of a finite group on a commutative ring, some element has trace ∑ g, g • c equal to 1. Equivalently, the trace to the fixed subring is surjective.

theorem RingHom.sum_mul_sum_smul {A : Type u_1} {G : Type u_2} [CommRing A] [Group G] [MulSemiringAction G A] [DecidableEq G] {G' : Type u_3} {C : Type u_4} [Group G'] [Fintype G'] [CommRing C] [MulSemiringAction G' C] (f : A →+* C) (π : G' →* G) (hπ : ∀ (g : G') (a : A), g • f a = f (π g • a)) {S : Finset (A × A)} (hS : ∀ (g : G), ∑ p ∈ S, p.1 * g • p.2 = Pi.single 1 1 g) (c : C) : ∑ p ∈ S, f p.1 * ∑ g : G', g • (f p.2 * c) = ∑ g : G', if π g = 1 then g • c else 0

Let (xᵢ, yᵢ) be a finite family with ∑ i, xᵢ * g • yᵢ equal to 1 at g = 1 and 0 elsewhere, as for a preimage of the indicator function of 1 under tensorToPi. After a ring map f : A → C equivariant along π : G' → G, pairing the xᵢ with the traces of yᵢ * c gives the sum of the translates of c by the kernel of π.

theorem TauCeti.MulSemiringAction.span_range_smul_sub_eq_top_iff {A : Type u_1} {G : Type u_2} [CommRing A] [Monoid G] [MulSemiringAction G A] {k : Type u_3} {K : Type u_4} [Field k] [Field K] [IsAlgClosed K] [Algebra k K] [Algebra k A] [Algebra.FiniteType k A] [SMulCommClass G k A] (g : G) : Ideal.span (Set.range fun (a : A) => g • a - a) = ⊤ ↔ ∀ (x : A →ₐ[k] K), x.comp (MulSemiringAction.toAlgHom k A g) ≠ x

On a finite-type algebra over a field, the elements g • a - a generate the unit ideal exactly when g fixes no point valued in an algebraically closed extension field. Thus freeness in the sense of tensorToPi_surjective_iff can be tested on geometric points.