ModuleReduced.lean
Nyll.SchemeTheory.Divisors.Reduced
3 declarations indexed from sourceView source ↗ Module documentation
Reduced ideal sheaves and their closed subschemes
An ideal sheaf is radical exactly when its associated closed subscheme is reduced. This is checked on the canonical affine cover by the quotients Spec (Γ(X, U) / I(U)).
Declarations
AlgebraicGeometry.Scheme.IdealSheafData.IsReduced.subscheme
DocumentationA radical ideal sheaf defines a reduced closed subscheme.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory
namespace AlgebraicGeometry
universe u
namespace Scheme.IdealSheafData
variable {X : Scheme.{u}} (I : X.IdealSheafData)
AlgebraicGeometry.Scheme.IdealSheafData.isReduced_of_subscheme
DocumentationIf the closed subscheme of an ideal sheaf is reduced, the ideal sheaf is radical.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory
namespace AlgebraicGeometry
universe u
namespace Scheme.IdealSheafData
variable {X : Scheme.{u}} (I : X.IdealSheafData)
AlgebraicGeometry.Scheme.IdealSheafData.isReduced_iff_subscheme_isReduced
DocumentationRadicality of an ideal sheaf is equivalent to reducedness of its closed subscheme.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory
namespace AlgebraicGeometry
universe u
namespace Scheme.IdealSheafData
variable {X : Scheme.{u}} (I : X.IdealSheafData)