ModuleEtaleRegularity.lean
Nyll.SchemeTheory.Divisors.EtaleRegularity
7 declarations indexed from sourceView source ↗ Module documentation
Regularity under etale morphisms
This file proves that regularity of local rings ascends along the local ring maps induced by etale morphisms. Consequently, regularity along the support of an ideal sheaf is preserved after etale pullback.
Imports8
- Nyll.SchemeTheory.Divisors.Basic
- Mathlib.LinearAlgebra.Dimension.Constructions
- Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
- Mathlib.RingTheory.Ideal.CotangentBaseChange
- Mathlib.RingTheory.Ideal.KrullsHeightTheorem
- Mathlib.RingTheory.Localization.Submodule
- Mathlib.RingTheory.LocalRing.Length
- Mathlib.RingTheory.Unramified.LocalRing
Imported by4
Declarations
RingHom.isRegularLocalRing_of_flat_of_formallyUnramified_of_essFiniteType
DocumentationA flat, formally unramified, essentially finite type local homomorphism with regular source has regular target.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
open TensorProduct
open scoped TensorProduct
namespace RingHom
universe u
RingHom.isRegularLocalRing_of_flat_of_formallyUnramified_of_essFiniteType_of_target
DocumentationA flat, formally unramified, essentially finite type local homomorphism with regular target and Noetherian source has regular source.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
open TensorProduct
open scoped TensorProduct
namespace RingHom
universe u
AlgebraicGeometry.Scheme.IsRegularAt.of_etale
DocumentationRegularity at a point ascends along an etale morphism.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
open TensorProduct
open scoped TensorProduct
namespace AlgebraicGeometry
universe u
namespace Scheme
AlgebraicGeometry.Scheme.IsRegularAt.descend_of_etale
DocumentationRegularity at the source point descends to its image along an etale morphism when the target scheme is locally Noetherian.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
open TensorProduct
open scoped TensorProduct
namespace AlgebraicGeometry
universe u
namespace Scheme
AlgebraicGeometry.Scheme.IdealSheafData.IsAmbientRegularAlongSupport.comap_of_etale
DocumentationIf the ambient scheme is regular along the support of an ideal sheaf, then the source of an etale morphism is regular along the support of its pullback.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
open TensorProduct
open scoped TensorProduct
namespace AlgebraicGeometry
universe u
namespace Scheme
namespace IdealSheafData
variable {X Y : Scheme.{u}}
AlgebraicGeometry.Scheme.IdealSheafData.IsNormalCrossingsAt.isRegularAt
DocumentationAt a point of its support, a normal-crossings ideal sheaf has regular ambient local ring. The regularity is read on a strict-normal-crossings etale chart and then descended along the chart map.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
open TensorProduct
open scoped TensorProduct
namespace AlgebraicGeometry
universe u
namespace Scheme
namespace IdealSheafData
variable {X Y : Scheme.{u}}
AlgebraicGeometry.Scheme.IdealSheafData.IsNormalCrossings.isAmbientRegularAlongSupport
DocumentationNormal crossings force regularity of the ambient locally Noetherian scheme along the divisor support.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
open TensorProduct
open scoped TensorProduct
namespace AlgebraicGeometry
universe u
namespace Scheme
namespace IdealSheafData
variable {X Y : Scheme.{u}}