Invariant Extensions of Rings

In this file we generalize the results in Mathlib/RingTheory/Invariant/Basic.lean to profinite groups.

Main statements

Let G be a profinite group acting continuously on a commutative ring B (with the discrete topology) satisfying Algebra.IsInvariant A B G.

• Algebra.IsInvariant.isIntegral_of_profinite: B/A is an integral extension.
• Algebra.IsInvariant.exists_smul_of_under_eq_of_profinite: G acts transitivity on the prime ideals of B lying above a given prime ideal of A.
• Ideal.Quotient.stabilizerHom_surjective_of_profinite: if Q is a prime ideal of B lying over a prime ideal P of A, then the stabilizer subgroup of Q surjects onto Aut((B/Q)/(A/P)).

theorem Algebra.IsInvariant.isIntegral_of_profinite {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] {G : Type u} [Group G] [MulSemiringAction G B] [SMulCommClass G A B] [TopologicalSpace G] [CompactSpace G] [TotallyDisconnectedSpace G] [IsTopologicalGroup G] [TopologicalSpace B] [DiscreteTopology B] [ContinuousSMul G B] [IsInvariant A B G] : Algebra.IsIntegral A B

theorem Algebra.IsInvariant.exists_smul_of_under_eq_of_profinite {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] {G : Type u} [Group G] [MulSemiringAction G B] [SMulCommClass G A B] [TopologicalSpace G] [CompactSpace G] [TotallyDisconnectedSpace G] [IsTopologicalGroup G] [TopologicalSpace B] [DiscreteTopology B] [ContinuousSMul G B] [IsInvariant A B G] (P Q : Ideal B) [P.IsPrime] [Q.IsPrime] (hPQ : Ideal.under A P = Ideal.under A Q) : ∃ (g : G), Q = g • P

G acts transitively on the prime ideals of B above a given prime ideal of A.

theorem Ideal.Quotient.stabilizerHomSurjectiveAuxFunctor_aux {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] {G : Type u} [Group G] [MulSemiringAction G B] [SMulCommClass G A B] [TopologicalSpace G] (Q : Ideal B) {N N' : OpenNormalSubgroup G} (e : N ≤ N') (x : G ⧸ ↑N.toOpenSubgroup) (hx : x ∈ MulAction.stabilizer (G ⧸ ↑N.toOpenSubgroup) (under (↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup)) Q)) : (QuotientGroup.map (↑N.toOpenSubgroup) N'.toOpenSubgroup.1 (MonoidHom.id G) e) x ∈ MulAction.stabilizer (G ⧸ ↑N'.toOpenSubgroup) (under (↥(FixedPoints.subalgebra A B ↥↑N'.toOpenSubgroup)) Q)

def Ideal.Quotient.stabilizerHomSurjectiveAuxFunctor {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] {G : Type u} [Group G] [MulSemiringAction G B] [SMulCommClass G A B] [TopologicalSpace G] (P : Ideal A) (Q : Ideal B) [Q.LiesOver P] (σ : (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q) : CategoryTheory.Functor (OpenNormalSubgroup G) (Type u)

(Implementation) The functor taking an open normal subgroup N ≤ G to the set of lifts of σ in G ⧸ N. We will show that its inverse limit is nonempty to conclude that there exists a lift in G.

Equations

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

instance instFiniteObjOpenNormalSubgroupStabilizerHomSurjectiveAuxFunctor {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] {G : Type u} [Group G] [MulSemiringAction G B] [SMulCommClass G A B] [TopologicalSpace G] [CompactSpace G] [IsTopologicalGroup G] (P : Ideal A) (Q : Ideal B) [Q.LiesOver P] (σ : (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q) (N : OpenNormalSubgroup G) : Finite ((Ideal.Quotient.stabilizerHomSurjectiveAuxFunctor P Q σ).obj N)

instance instNonemptyObjOpenNormalSubgroupStabilizerHomSurjectiveAuxFunctor {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] {G : Type u} [Group G] [MulSemiringAction G B] [SMulCommClass G A B] [TopologicalSpace G] [CompactSpace G] [IsTopologicalGroup G] (P : Ideal A) (Q : Ideal B) [Q.IsPrime] [Q.LiesOver P] [Algebra.IsInvariant A B G] (σ : (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q) (N : OpenNormalSubgroup G) : Nonempty ((Ideal.Quotient.stabilizerHomSurjectiveAuxFunctor P Q σ).obj N)

theorem Ideal.Quotient.stabilizerHom_surjective_of_profinite {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] {G : Type u} [Group G] [MulSemiringAction G B] [SMulCommClass G A B] [TopologicalSpace G] [CompactSpace G] [TotallyDisconnectedSpace G] [IsTopologicalGroup G] [TopologicalSpace B] [DiscreteTopology B] [ContinuousSMul G B] (P : Ideal A) (Q : Ideal B) [Q.IsPrime] [Q.LiesOver P] [Algebra.IsInvariant A B G] : Function.Surjective ⇑(stabilizerHom Q P G)

The stabilizer subgroup of Q surjects onto Aut((B/Q)/(A/P)).