AlgebraicGeometry.dense_setOf_exists_section_of_isAlgClosed
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.dense_setOf_exists_section_of_isAlgClosed
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometryLean source · statement
theorem _root_.AlgebraicGeometry.dense_setOf_exists_section_of_isAlgClosed
{k : Type u} [Field k] [IsAlgClosed k] {X : Scheme.{u}} (f : X ⟶ Spec (.of k))
[LocallyOfFiniteType f] :
Dense {x : X | ∃ s : Spec (.of k) ⟶ X, s ≫ f = 𝟙 _ ∧ s (IsLocalRing.closedPoint k) = x}