Module

exists_over_hom_base_closedPoint_eq_of_isClosed_singleton.lean

Nyll.AlgebraicCurves.Geometry.Schemes.exists_over_hom_base_closedPoint_eq_of_isClosed_singleton

1 declaration indexed from sourceView source ↗

Module documentation

Rational points corresponding to closed points

Over an algebraically closed field, a closed point of a scheme locally of finite type is the image of the closed point under a morphism over the field.

Imports1

Mathlib.AlgebraicGeometry.AlgClosed.Basic

Imported by6

theorem

exists_over_hom_base_closedPoint_eq_of_isClosed_singleton

L31 ↗

AlgebraicGeometry.exists_over_hom_base_closedPoint_eq_of_isClosed_singleton

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_over_hom_base_closedPoint_eq_of_isClosed_singleton
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry

Lean source · statement

theorem _root_.AlgebraicGeometry.exists_over_hom_base_closedPoint_eq_of_isClosed_singleton
    (k : Type u) [Field k] [IsAlgClosed k] {X : Scheme.{u}} (t : X ⟶ Spec (CommRingCat.of k))
    [LocallyOfFiniteType t] (x : X) (hx : IsClosed ({x} : Set X)) :
    ∃ z : Over.mk (𝟙 (Spec (CommRingCat.of k))) ⟶ Over.mk t, z.left.base
        (IsLocalRing.closedPoint k) = x

Module documentation

Rational points corresponding to closed points

Declarations

exists_over_hom_base_closedPoint_eq_of_isClosed_singleton