ModuleCartierEtale.lean
Nyll.SchemeTheory.Divisors.CartierEtale
5 declarations indexed from sourceView source ↗ Module documentation
Effective Cartier divisors under affine flat pullback
The pullback ideal of a locally principal non-zero-divisor remains locally principal and is generated by the image of that non-zero-divisor. Flatness preserves its regularity.
Declarations
AlgebraicGeometry.Scheme.IdealSheafData.IsEffectiveCartier.comap_of_flat_of_isAffineHom
DocumentationEffective Cartier ideal sheaves remain effective Cartier after affine flat pullback.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory
namespace AlgebraicGeometry
universe u
namespace Scheme
namespace IdealSheafData
variable {X Y : Scheme.{u}}
AlgebraicGeometry.Scheme.EffectiveCartierDivisor.comap
DocumentationPullback of an effective Cartier divisor along an affine flat morphism.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory
namespace AlgebraicGeometry
universe u
namespace Scheme
namespace EffectiveCartierDivisor
variable {X Y : Scheme.{u}}
AlgebraicGeometry.Scheme.EffectiveCartierDivisor.coe_comap
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory
namespace AlgebraicGeometry
universe u
namespace Scheme
namespace EffectiveCartierDivisor
variable {X Y : Scheme.{u}}
AlgebraicGeometry.Scheme.EffectiveCartierDivisor.comapFiniteEtale
DocumentationPullback along a finite-etale object, with all morphism-property instances supplied by the object itself.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory
namespace AlgebraicGeometry
universe u
namespace Scheme
namespace EffectiveCartierDivisor
variable {X Y : Scheme.{u}}
AlgebraicGeometry.Scheme.EffectiveCartierDivisor.coe_comapFiniteEtale
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory
namespace AlgebraicGeometry
universe u
namespace Scheme
namespace EffectiveCartierDivisor
variable {X Y : Scheme.{u}}