AlgebraicCurves.Geometry.Schemes.Proofs.isReduced_of_etale.L3gen.isReduced_subscheme_vanishingIdeal
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.isReduced_of_etale
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits TopologicalSpace Opposite
universe u
namespace L3genLean source · statement
theorem isReduced_subscheme_vanishingIdeal {X : Scheme.{u}} (Z : Closeds X) :
IsReduced (Scheme.IdealSheafData.vanishingIdeal Z).subscheme