Invariant rings and localization

Let a group G act on a commutative ring A by ring automorphisms, and write Aᴳ for the invariant subring FixedPoints.subring A G. This file compares invariants with localization.

For a submonoid M of invariant elements, the action extends to the localization M⁻¹A (Localization (Algebra.algebraMapSubmonoid A M)), compatibly with A → M⁻¹A. When G is finite, taking invariants commutes with this localization: (M⁻¹A)ᴳ is the localization of Aᴳ at M. A fraction a / s fixed by every g satisfies t_g (g • a - a) = 0 for some t_g ∈ M, which can be replaced by the product t of the t_g because G is finite, and then a / s = t a / (s t) with t a invariant. Taking M to be the powers of an invariant r gives the localization A[1/r] of A at r. The argument only uses finitely many ring endomorphisms compatible with the localization map, and is stated in that form for an arbitrary localization S of A, whose fixed elements are described by an arbitrary ring R' mapping injectively to S (TauCeti.FixedPoints.isLocalization_of_mem_range_iff).

Also for finite G, the local homomorphism (Aᴳ)_P → A_Q induced by Aᴳ ⊆ A at a prime Q of A lying over a prime P of Aᴳ is injective. If an invariant a is killed by some t ∉ Q, prime avoidance applied to the annihilator of a, which is G-stable, and the finitely many primes g⁻¹ • Q gives such a t outside every g⁻¹ • Q; then the invariant ∏ g, g • t lies outside P and kills a.

These are the two local facts behind the categorical universal property of the affine invariant quotient Spec A ⟶ Spec Aᴳ for arbitrary target schemes.

Main definitions

• TauCeti.FixedPoints.localizationRingAut M: the action of G on M⁻¹A for a submonoid M of invariants, which provides the instance MulSemiringAction G (Localization (Algebra.algebraMapSubmonoid A M)).
• The instance Algebra (FixedPoints.subring A G) (FixedPoints.subring (Localization (Algebra.algebraMapSubmonoid A M)) G) given by A → M⁻¹A.

Main results

• TauCeti.FixedPoints.smul_algebraMap_localization: A → M⁻¹A is G-equivariant.
• TauCeti.FixedPoints.smul_mk': G acts on a fraction a / s through its numerator.
• TauCeti.FixedPoints.isLocalization_of_mem_range_iff: the elements of a localization fixed by finitely many compatible ring endomorphisms are the localization of the fixed elements.
• TauCeti.FixedPoints.isLocalization: for finite G, (M⁻¹A)ᴳ is the localization of Aᴳ at M.
• Ideal.exists_mem_forall_smul_notMem: for finite G, prime avoidance for the translates g⁻¹ • Q of a prime Q.
• Ideal.exists_notMem_dvd_of_forall_smul_notMem: for finite G, an element outside every g⁻¹ • Q divides an invariant outside Q.
• TauCeti.FixedPoints.localRingHom_injective: for finite G, (Aᴳ)_P → A_Q is injective.

References

• M. Demazure and A. Grothendieck, Schémas en groupes (SGA 3), Exposé V, §1.

theorem TauCeti.FixedPoints.isLocalization_of_mem_range_iff {ι : Type u_1} {R : Type u_2} {A : Type u_3} {R' : Type u_4} {S : Type u_5} [Finite ι] [CommRing R] [CommRing A] [CommRing R'] [CommRing S] [Algebra R A] [Algebra A S] [Algebra R' S] [Algebra R R'] (M : Submonoid R) [IsLocalization (Algebra.algebraMapSubmonoid A M) S] (σ : ι → A →+* A) (τ : ι → S →+* S) (hστ : ∀ (i : ι) (a : A), (τ i) ((algebraMap A S) a) = (algebraMap A S) ((σ i) a)) (hR : Function.Injective ⇑(algebraMap R A)) (hσ : ∀ (a : A), a ∈ Set.range ⇑(algebraMap R A) ↔ ∀ (i : ι), (σ i) a = a) (hR' : Function.Injective ⇑(algebraMap R' S)) (hτ : ∀ (s : S), s ∈ Set.range ⇑(algebraMap R' S) ↔ ∀ (i : ι), (τ i) s = s) (h : ∀ (x : R), (algebraMap R' S) ((algebraMap R R') x) = (algebraMap A S) ((algebraMap R A) x)) : IsLocalization M R'

Fixed elements commute with localization. Let S be a localization of A at the image of a submonoid M of R, and let finitely many ring endomorphisms σ i of A and τ i of S be compatible with A → S. If R → A and R' → S are injective with images the elements fixed by every σ i, respectively every τ i, and R → R' is compatible with them, then R' is the localization of R at M. A fraction a / s fixed by every τ i satisfies t_i (σ i a - a) = 0 for some t_i ∈ M, which can be replaced by the product t of the t_i since there are finitely many i; then a / s = t a / (s t) with t a fixed.

noncomputable def TauCeti.FixedPoints.localizationRingAut {A : Type u_1} {G : Type u_2} [CommRing A] [Group G] [MulSemiringAction G A] (M : Submonoid ↥(FixedPoints.subring A G)) : G →* RingAut (Localization (Algebra.algebraMapSubmonoid A M))

The action of G on the localization M⁻¹A at a submonoid M of invariants, induced by its action on A.

@[instance_reducible]

noncomputable instance TauCeti.FixedPoints.instMulSemiringActionLocalization {A : Type u_1} {G : Type u_2} [CommRing A] [Group G] [MulSemiringAction G A] (M : Submonoid ↥(FixedPoints.subring A G)) : MulSemiringAction G (Localization (Algebra.algebraMapSubmonoid A M))

The action of G on M⁻¹A given by localizationRingAut.

theorem TauCeti.FixedPoints.localizationRingAut_apply {A : Type u_1} {G : Type u_2} [CommRing A] [Group G] [MulSemiringAction G A] (M : Submonoid ↥(FixedPoints.subring A G)) (g : G) (x : Localization (Algebra.algebraMapSubmonoid A M)) : ((localizationRingAut M) g) x = g • x

localizationRingAut M g is the action of g on M⁻¹A.

@[simp]

theorem TauCeti.FixedPoints.smul_algebraMap_localization {A : Type u_1} {G : Type u_2} [CommRing A] [Group G] [MulSemiringAction G A] (M : Submonoid ↥(FixedPoints.subring A G)) (g : G) (a : A) : g • (algebraMap A (Localization (Algebra.algebraMapSubmonoid A M))) a = (algebraMap A (Localization (Algebra.algebraMapSubmonoid A M))) (g • a)

The action of G on M⁻¹A extends the action on A.

@[simp]

theorem TauCeti.FixedPoints.smul_mk' {A : Type u_1} {G : Type u_2} [CommRing A] [Group G] [MulSemiringAction G A] (M : Submonoid ↥(FixedPoints.subring A G)) (g : G) (a : A) (s : ↥(Algebra.algebraMapSubmonoid A M)) : g • IsLocalization.mk' (Localization (Algebra.algebraMapSubmonoid A M)) a s = IsLocalization.mk' (Localization (Algebra.algebraMapSubmonoid A M)) (g • a) s

The action of G on M⁻¹A on fractions: g • (a / s) = (g • a) / s, since the denominator s is invariant.

theorem TauCeti.FixedPoints.algebraMap_mem_fixedPoints {A : Type u_1} {G : Type u_2} [CommRing A] [Group G] [MulSemiringAction G A] (M : Submonoid ↥(FixedPoints.subring A G)) (a : ↥(FixedPoints.subring A G)) : (algebraMap A (Localization (Algebra.algebraMapSubmonoid A M))) ↑a ∈ FixedPoints.subring (Localization (Algebra.algebraMapSubmonoid A M)) G

The localization map A → M⁻¹A sends invariants to invariants.

@[instance_reducible]

noncomputable instance TauCeti.FixedPoints.instAlgebraLocalization {A : Type u_1} {G : Type u_2} [CommRing A] [Group G] [MulSemiringAction G A] (M : Submonoid ↥(FixedPoints.subring A G)) : Algebra ↥(FixedPoints.subring A G) ↥(FixedPoints.subring (Localization (Algebra.algebraMapSubmonoid A M)) G)

The algebra structure of (M⁻¹A)ᴳ over Aᴳ given by the localization map A → M⁻¹A.

@[simp]

theorem TauCeti.FixedPoints.coe_algebraMap_localization {A : Type u_1} {G : Type u_2} [CommRing A] [Group G] [MulSemiringAction G A] (M : Submonoid ↥(FixedPoints.subring A G)) (a : ↥(FixedPoints.subring A G)) : ↑((algebraMap ↥(FixedPoints.subring A G) ↥(FixedPoints.subring (Localization (Algebra.algebraMapSubmonoid A M)) G)) a) = (algebraMap A (Localization (Algebra.algebraMapSubmonoid A M))) ↑a

The algebra map Aᴳ → (M⁻¹A)ᴳ is the localization map A → M⁻¹A.

instance TauCeti.FixedPoints.isLocalization {A : Type u_1} {G : Type u_2} [CommRing A] [Group G] [MulSemiringAction G A] (M : Submonoid ↥(FixedPoints.subring A G)) [Finite G] : IsLocalization M ↥(FixedPoints.subring (Localization (Algebra.algebraMapSubmonoid A M)) G)

Invariants commute with localization at invariant elements. For a finite group G and a submonoid M of the invariants Aᴳ, the invariants of M⁻¹A are the localization of Aᴳ at M.

theorem Ideal.exists_mem_forall_smul_notMem {A : Type u_1} {G : Type u_2} [CommRing A] [Group G] [MulSemiringAction G A] [Finite G] (Q : Ideal A) [Q.IsPrime] {I : Ideal A} (hI : ∀ (g : G), ¬I ≤ comap (MulSemiringAction.toRingHom G A g) Q) : ∃ u ∈ I, ∀ (g : G), g • u ∉ Q

Prime avoidance for the translates of a prime. For a finite group G, if an ideal I of A is contained in no translate g⁻¹ • Q of a prime Q, then some u ∈ I satisfies g • u ∉ Q for every g.

theorem Ideal.exists_notMem_dvd_of_forall_smul_notMem {A : Type u_1} {G : Type u_2} [CommRing A] [Group G] [MulSemiringAction G A] [Finite G] (Q : Ideal A) [Q.IsPrime] {u : A} (hu : ∀ (g : G), g • u ∉ Q) : ∃ (r : ↥(FixedPoints.subring A G)), ↑r ∉ Q ∧ u ∣ ↑r

Norms of elements avoiding every translate of a prime. For a finite group G, if g • u ∉ Q for every g, then the invariant norm ∏ g, g • u lies outside Q and is divisible by u.

theorem TauCeti.FixedPoints.exists_mul_eq_zero_of_mul_eq_zero {A : Type u_1} {G : Type u_2} [CommRing A] [Group G] [MulSemiringAction G A] [Finite G] (Q : Ideal A) [Q.IsPrime] (x : ↥(FixedPoints.subring A G)) {t : A} (htQ : t ∉ Q) (htx : t * ↑x = 0) : ∃ s ∈ FixedPoints.subring A G, s ∉ Q ∧ s * ↑x = 0

If an invariant x is killed by an element outside a prime Q, it is killed by an invariant element outside Q. This is prime avoidance for the G-stable annihilator of x and the finitely many primes g⁻¹ • Q.

theorem TauCeti.FixedPoints.localRingHom_injective {A : Type u_1} {G : Type u_2} [CommRing A] [Group G] [MulSemiringAction G A] [Finite G] (P : Ideal ↥(FixedPoints.subring A G)) (Q : Ideal A) [P.IsPrime] [Q.IsPrime] (hPQ : P = Ideal.comap (algebraMap (↥(FixedPoints.subring A G)) A) Q) : Function.Injective ⇑(Localization.localRingHom P Q (algebraMap (↥(FixedPoints.subring A G)) A) hPQ)

Invariants inject into stalks. For a finite group G, a prime Q of A and the prime P of Aᴳ below it, the induced homomorphism of local rings (Aᴳ)_P → A_Q is injective.