ModuleEtaleRadicial.lean
Nyll.SchemeTheory.Morphisms.EtaleRadicial
2 declarations indexed from sourceView source ↗ Module documentation
Universally injective étale morphisms
The diagonal of an étale morphism is an open immersion. Universal injectivity makes it surjective and hence an isomorphism. The morphism is therefore a monomorphism, and the flat finite-presentation criterion makes it an open immersion.
Imports4
- Mathlib.AlgebraicGeometry.Morphisms.Etale
- Mathlib.AlgebraicGeometry.Morphisms.FlatMono
- Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective
- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Imported by3
Declarations
AlgebraicGeometry.Etale.isOpenImmersion_of_universallyInjective
DocumentationA universally injective étale morphism is an open immersion.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public section
open CategoryTheory Limits
universe u
namespace AlgebraicGeometry.Etale
AlgebraicGeometry.Etale.isIso_of_universallyInjective_of_surjective
DocumentationA surjective universally injective étale morphism is an isomorphism.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public section
open CategoryTheory Limits
universe u
namespace AlgebraicGeometry.Etale