EtaleFundamentalGroups.moduleFinite_localizationAtPrime_of_henselian_of_etale
A chosen prime-local factor of an etale algebra over a Henselian local ring is finite over the base ring.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups
universe u vLean source · statement
theorem moduleFinite_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)] :
Module.Finite R (Localization.AtPrime q)