Module

ChosenLocalizationEtale.lean

Nyll.SchemeTheory.FiniteEtale.Henselian.ChosenLocalizationEtale

1 declaration indexed from sourceView source ↗

Module documentation

Etaleness of a chosen Henselian local factor

An arbitrary localization of an etale algebra need not be finite over the original base. For the localization at a prime over the closed point of a Henselian local ring, Tag 00UJ supplies finiteness. Flatness then makes this finite module free over the local base, hence finitely presented. Together with formal etaleness of localization, this upgrades the chosen local factor itself to an etale algebra over the Henselian base.

Imports4

Mathlib.RingTheory.Finiteness.ModuleFinitePresentation
Mathlib.RingTheory.Flat.Localization
Mathlib.RingTheory.LocalRing.Module
Nyll.SchemeTheory.FiniteEtale.Henselian.ChosenLocalization

Imported by7

theorem

etale_localizationAtPrime_of_henselian_of_etale

L31 ↗

EtaleFundamentalGroups.etale_localizationAtPrime_of_henselian_of_etale

Documentation

A chosen prime-local factor of an etale algebra over a Henselian local ring is etale over the base ring. Unlike a raw localization-finiteness assertion, the finiteness used here is produced by moduleFinite_localizationAtPrime_of_henselian_of_etale.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe u v

Lean source · statement

theorem etale_localizationAtPrime_of_henselian_of_etale
    {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S]
    [HenselianLocalRing R] [Algebra.Etale R S]
    (q : Ideal S) [q.IsPrime] [q.LiesOver (IsLocalRing.maximalIdeal R)] :
    Algebra.Etale R (Localization.AtPrime q)

Module documentation

Etaleness of a chosen Henselian local factor

Declarations

etale_localizationAtPrime_of_henselian_of_etale