AlgebraicGeometry.exists_mem_isClosed_singleton_ne_of_isIrreducible
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.exists_mem_isClosed_singleton_ne_of_isIrreducible
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometryLean source · statement
theorem _root_.AlgebraicGeometry.exists_mem_isClosed_singleton_ne_of_isIrreducible
(k : Type u) [Field k] {X : Scheme.{u}} (t : X ⟶ Spec (CommRingCat.of k)) [LocallyOfFiniteType
t]
(Z : Set X) (hZ : IsClosed Z) (_hZ' : IsIrreducible Z)
(x : X) (hxZ : x ∈ Z) (hx : IsClosed ({x} : Set X)) (hne : Z ≠ {x}) :
∃ x' ∈ Z, IsClosed ({x'} : Set X) ∧ x' ≠ x