theorem
L30 ↗localizedFiniteAlgebra_isEtaleAt_away_from_closedPoint_of_minimal_base_nonEtaleCotangentSupport
EtaleFundamentalGroups.SpecialLocalPurity.localizedFiniteAlgebra_isEtaleAt_away_from_closedPoint_of_minimal_base_nonEtaleCotangentSupport
After localizing a finite algebra at a minimal bad base point, every target prime not lying over the closed point is etale. The target prime is contracted through the prime-localization correspondence, where its base contraction becomes strictly smaller than the chosen minimal point.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups.SpecialLocalPurity
universe u vLean source · statement
theorem
localizedFiniteAlgebra_isEtaleAt_away_from_closedPoint_of_minimal_base_nonEtaleCotangentSupport
{R : Type u} {S : Type v} [CommRing R] [CommRing S]
[Algebra R S] [Module.Finite R S]
(p : PrimeSpectrum R)
(hp : Minimal
(· ∈ Module.support R Ω[S⁄R] ∪
Module.support R (Algebra.H1Cotangent R S)) p)
(Q : PrimeSpectrum
(Localization (Algebra.algebraMapSubmonoid S p.asIdeal.primeCompl)))
(hQ :
PrimeSpectrum.comap
(algebraMap (Localization.AtPrime p.asIdeal)
(Localization (Algebra.algebraMapSubmonoid S p.asIdeal.primeCompl))) Q ≠
⟨IsLocalRing.maximalIdeal (Localization.AtPrime p.asIdeal), inferInstance⟩) :
Algebra.IsEtaleAt (Localization.AtPrime p.asIdeal) Q.asIdeal