Module

CurveModel_surjective_and_eq_genericPoint_or_isClosed_singleton_of_isIso_stalkMap.lean

Nyll.AlgebraicCurves.Models.CurveModel_surjective_and_eq_genericPoint_or_isClosed_singleton_of_isIso_stalkMap

2 declarations indexed from sourceView source ↗

Module documentation

Curve Model surjective and eq generic Point or is Closed singleton of is Iso stalk Map

Imports5

Imported by4

theorem

eq_genericPoint_of_isField

L33 ↗

AlgebraicCurves.Models.Proofs.CurveModelPointClassification.PointsL8.eq_genericPoint_of_isField

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModelPointClassification
universe u v
open CategoryTheory AlgebraicGeometry AlgebraicCurve
namespace PointsL8

Lean source · statement

theorem eq_genericPoint_of_isField {C : Scheme.{u}} [IsIntegral C] (x : C)
    (hfield : IsField (C.presheaf.stalk x)) : x = genericPoint C

theorem

surjective_and_eq_genericPoint_or_isClosed_singleton_of_isIso_stalkMap

L66 ↗

AlgebraicCurve.CurveModel.surjective_and_eq_genericPoint_or_isClosed_singleton_of_isIso_stalkMap

Source context 6 commands