ModuleEtalePostcomposition.lean
Nyll.SchemeTheory.Morphisms.EtalePostcomposition
2 declarations indexed from sourceView source ↗ Module documentation
Cancelling an etale second morphism
If the second map of a factorization is etale, its graph is an open immersion into the base change of the composite. Flatness, local finite presentation, and geometric reducedness of the composite therefore hold for the first map as well. The graph and its open immersion are constructed from the actual diagonal; no graph or comparison is supplied as input.
Imports6
- Mathlib.AlgebraicGeometry.Geometrically.Reduced
- Mathlib.AlgebraicGeometry.Morphisms.Etale
- Mathlib.AlgebraicGeometry.Morphisms.Flat
- Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
- Mathlib.CategoryTheory.MorphismProperty.Limits
Imported by5
Declarations
AlgebraicGeometry.GeometricallyReduced.comp_of_isOpenImmersion
DocumentationAn open subscheme of a geometrically reduced scheme remains geometrically reduced over the same base.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry
universe u
AlgebraicGeometry.flat_finitePresentation_geometricallyReduced_of_comp_etale
DocumentationFlatness, local finite presentation, and geometric reducedness descend through etale postcomposition by expressing the first map as its open graph followed by the base change of the composite.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry
universe u