Nyll.ValuedFieldTheory.Ramification.ProfiniteInvariant

Module documentation

Profinite invariant rings: normality on prime residue fields

The finite invariant-ring API proves that a prime residue extension is normal. The residue-action exact sequence also needs the corresponding profinite statement. The proof is the same finite-orbit argument as in this construction: an element of the discrete ring is fixed by an open normal subgroup, so its orbit polynomial is computed in a finite quotient.

theorem

normal_of_profinite

L45 ↗

RamificationTheory.Ideal.Quotient.normal_of_profinite

Documentation

Profinite version of Ideal.Quotient.normal.

Every element has a finite orbit because the action on B is continuous and B is discrete. Passing to an open normal subgroup fixing a representative reduces the splitting calculation to the finite quotient action.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace RamificationTheory
noncomputable section
open scoped Pointwise
variable {A B : Type*} [CommRing A] [CommRing B] [Algebra A B]
variable {G : Type*} [Group G] [MulSemiringAction G B] [SMulCommClass G A B]
variable [TopologicalSpace G] [CompactSpace G] [TotallyDisconnectedSpace G]
variable [IsTopologicalGroup G] [TopologicalSpace B] [DiscreteTopology B]
variable [ContinuousSMul G B] [Algebra.IsInvariant A B G]
namespace Ideal.Quotient
attribute [local instance] Ideal.Quotient.field
include G

Lean source · statement

theorem normal_of_profinite
    (P : Ideal A) (Q : Ideal B) [P.IsMaximal] [Q.IsMaximal] [Q.LiesOver P] :
    Normal (A ⧸ P) (B ⧸ Q)

Module documentation

Profinite invariant rings: normality on prime residue fields

Declarations

normal_of_profinite