ModuleProperLocalCover.lean
Nyll.SchemeTheory.Etale.ProperLocalCover
2 declarations indexed from sourceView source ↗ Module documentation
Detecting étale coverings on the closed fiber of a proper local scheme
For a universally closed scheme over a local spectrum, an étale morphism is surjective exactly when its base change to the closed fiber is surjective. The open image of the étale morphism contains the entire closed fiber. The existing closed-map neighborhood theorem then supplies an open neighborhood of the closed point, which must be the entire local spectrum.
In particular this applies to every proper morphism over a local ring. It is the covering-detection input for descent from the closed fiber in the proper-local comparison. It asserts no cohomological base-change theorem.
Imports10
- Nyll.SchemeTheory.Etale.FiniteNeighborhoodSection
- Mathlib.AlgebraicGeometry.Morphisms.Etale
- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
- Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
- Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
- Mathlib.AlgebraicGeometry.PullbackCarrier
- Mathlib.AlgebraicGeometry.Scheme
- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
- Mathlib.RingTheory.Spectrum.Prime.Topology
- Mathlib.Topology.Maps.Basic
Imported by2
Declarations
AlgebraicGeometry.Etale.surjective_of_closedFiber_subset_range
DocumentationAn étale morphism into a universally closed scheme over a local spectrum is surjective if its image contains the closed fiber.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.Etale
AlgebraicGeometry.Etale.surjective_iff_closedFiber
DocumentationSurjectivity of an étale morphism into a universally closed local scheme is detected after base change to its actual scheme-theoretic closed fiber.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.Etale