AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_subset_basicOpen_or_disjoint_of_isProper_of_isIrreducible.C2E5.isIntegral_subscheme_vanishingIdeal
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_subset_basicOpen_or_disjoint_of_isProper_of_isIrreducible
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace C2E5Lean source · statement
theorem isIntegral_subscheme_vanishingIdeal {X : Scheme.{u}} (Z : Set X) (hZ : IsClosed Z) (hZ' :
IsIrreducible Z) :
IsIntegral (Scheme.IdealSheafData.vanishingIdeal ⟨Z, hZ⟩).subscheme