ModuleUnramifiedHomExt.lean
Nyll.SchemeTheory.Morphisms.UnramifiedHomExt
2 declarations indexed from sourceView source ↗ Module documentation
Unramified morphisms are determined on a dense source
The equalizer of two relative morphisms into an unramified scheme is an open subscheme. If the target is also separated, the equalizer is closed. Thus agreement after a dominant morphism forces the equalizer to be the entire source, without a reducedness assumption.
Imports8
- Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
- Mathlib.AlgebraicGeometry.Morphisms.IsIso
- Mathlib.AlgebraicGeometry.Morphisms.Separated
- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
- Mathlib.AlgebraicGeometry.OpenImmersion
- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Imported by11
Declarations
AlgebraicGeometry.isOpenImmersion_equalizer_ι_left
DocumentationThe relative equalizer of two maps into an unramified scheme is open.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public section
open CategoryTheory CategoryTheory.Limits
noncomputable section
universe u
namespace AlgebraicGeometry
AlgebraicGeometry.Over.hom_ext_of_isDominant_of_unramified
DocumentationRelative maps into a separated unramified scheme are determined after a dominant map, even when the source is nonreduced.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public section
open CategoryTheory CategoryTheory.Limits
noncomputable section
universe u
namespace AlgebraicGeometry