NYLL
Module

UnramifiedIntrinsicInertia.lean

Nyll.EtaleFundamentalGroups.Inertia.UnramifiedIntrinsicInertia
1 declaration indexed from sourceView source ↗

Module documentation

Trivial intrinsic inertia on an unramified domain

The literal coefficient automorphisms in ideal inertia agree modulo the prime. Prime rigidity proves equality on the original domain itself, so the intrinsic inertia group has at most one element.

Imports6
Imported by2

Declarations

theorem

commAlgIdealInertia_subsingleton_of_unramified

L30 ↗
EtaleFundamentalGroups.Inertia.commAlgIdealInertia_subsingleton_of_unramified
Documentation

Actual coefficient-automorphism inertia is trivial on an unramified domain. Neither the acting automorphism group nor the base needs to be finite.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v
Lean source · statement
theorem commAlgIdealInertia_subsingleton_of_unramified
    (A : Type u) [CommRing A] (B : CommAlgCat.{v} A) [IsDomain B.carrier]
    [Algebra.FormallyUnramified A B.carrier] [Algebra.EssFiniteType A B.carrier]
    (Q : Ideal B.carrier) [Q.IsPrime] :
    Subsingleton (commAlgIdealInertiaGroup A B Q).carrier

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.