ModuleSmoothConnected.lean
Nyll.EtaleFundamentalGroups.FiniteEtale.GenericFiber.SmoothConnected
2 declarations indexed from sourceView source ↗ Module documentation
Connected generic fibres of smooth algebras over normal domains
For a smooth algebra over a normal domain, every idempotent in the generic fibre is the image of a unique idempotent of the original algebra. Indeed, idempotents are integral and smooth base change commutes with integral closure. Flatness makes the map to the generic fibre injective.
Consequently, a connected affine smooth scheme has connected generic fibre. This applies to a connected finite-etale cover of an affine smooth arithmetic scheme, since its composite structure morphism is smooth. The result concerns the ordinary generic fibre; geometric connectedness requires the additional arithmetic argument about the field of constants.
Declarations
EtaleFundamentalGroups.existsUnique_isIdempotentElem_genericFiber_of_smooth
DocumentationEvery idempotent of the generic fibre of a smooth algebra over a normal domain descends uniquely to an idempotent of the original algebra.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
open Polynomial
universe uR uS uK
variable {R : Type uR} {S : Type uS} {K : Type uK}
variable [CommRing R] [IsDomain R] [IsIntegrallyClosed R]
variable [CommRing S] [Algebra R S] [Algebra.Smooth R S]
variable [Field K] [Algebra R K] [IsFractionRing R K]
EtaleFundamentalGroups.connectedSpace_primeSpectrum_genericFiber_of_smooth
DocumentationA connected smooth affine scheme over a normal domain has connected ordinary generic fibre. No properness or finiteness as a module is required.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
open Polynomial
universe uR uS uK
variable {R : Type uR} {S : Type uS} {K : Type uK}
variable [CommRing R] [IsDomain R] [IsIntegrallyClosed R]
variable [CommRing S] [Algebra R S] [Algebra.Smooth R S]
variable [Field K] [Algebra R K] [IsFractionRing R K]