NYLL
Module

RegularSystem.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.RegularSystem
2 declarations indexed from sourceView source ↗

Module documentation

Regular systems under a finite étale local extension

A finite étale local algebra is faithfully flat over its local base. Hence a regular system remains regular after applying the algebra map. Formal unramifiedness identifies the extension of the source maximal ideal with the target maximal ideal, so the mapped system still generates the maximal ideal.

For a module-finite extension of a Noetherian base, the target is Noetherian. The regular-system geometry developed in Kummer.RegularSystemDomain then supplies the domain, regular-local, prime-parameter, and quotient conclusions.

Imports3
Imported by4

Declarations

theorem

regularSystem_map_of_etale_local

L39 ↗
EtaleFundamentalGroups.regularSystem_map_of_etale_local
Documentation

A regular system of parameters remains a regular system of parameters under an étale local extension.

The regularity is faithfully-flat descent along the local flat map. The maximal-ideal equality is the cotangent-space consequence of formal unramifiedness, rather than an extra assumption on the residue extension.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open RingTheory.Sequence
universe u v
Lean source · statement
theorem regularSystem_map_of_etale_local
    {A : Type u} {C : Type v}
    [CommRing A] [CommRing C] [Algebra A C]
    [IsLocalRing A] [IsLocalRing C]
    [Algebra.Etale A C]
    [IsLocalHom (algebraMap A C)]
    {ps : List A}
    (hreg : IsRegular A ps)
    (hgen : Ideal.ofList ps = maximalIdeal A) :
    IsRegular C (ps.map (algebraMap A C)) ∧
      Ideal.ofList (ps.map (algebraMap A C)) = maximalIdeal C
theorem

finiteEtale_regularSystem_geometry

L70 ↗
EtaleFundamentalGroups.finiteEtale_regularSystem_geometry
Documentation

Full local geometry of the mapped parameter system in a finite étale local extension of a Noetherian local ring.

No domain, regular-local, or primality hypothesis is imposed on the target. They are all produced from the mapped regular system. In particular, every mapped parameter cuts out a regular local domain.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open RingTheory.Sequence
universe u v
Lean source · statement
theorem finiteEtale_regularSystem_geometry
    {A : Type u} {C : Type v}
    [CommRing A] [CommRing C] [Algebra A C]
    [IsLocalRing A] [IsLocalRing C] [IsNoetherianRing A]
    [Module.Finite A C] [Algebra.Etale A C]
    [IsLocalHom (algebraMap A C)]
    {ps : List A}
    (hreg : IsRegular A ps)
    (hgen : Ideal.ofList ps = maximalIdeal A) :
    IsNoetherianRing C ∧
      IsDomain C ∧
      IsRegular C (ps.map (algebraMap A C)) ∧
      Ideal.ofList (ps.map (algebraMap A C)) = maximalIdeal C ∧
      IsRegularLocalRing C ∧
      (∀ p ∈ ps.map (algebraMap A C), Prime p) ∧
      (∀ p ∈ ps.map (algebraMap A C),
        IsDomain (C ⧸ Ideal.span {p}) ∧
          IsRegularLocalRing (C ⧸ Ideal.span {p}))

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