NYLL
Module

CurveModel_isFinite_of_isIso_stalkMap.lean

Nyll.AlgebraicCurves.Models.CurveModel_isFinite_of_isIso_stalkMap
5 declarations indexed from sourceView source ↗

Module documentation

Curve Model is Finite of is Iso stalk Map

Imports9
Imported by2

Declarations

theorem

eq_genericPoint_of_isField

L38 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isFinite_of_isIso_stalkMap.NuFinK11.eq_genericPoint_of_isField
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isFinite_of_isIso_stalkMap
open _root_.AlgebraicCurve.CurveModel
universe u v
open CategoryTheory AlgebraicGeometry AlgebraicCurve TopologicalSpace
namespace NuFinK11
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

stalkSpecializes_surjective_of_isIso_stalkMap

L59 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isFinite_of_isIso_stalkMap.NuFinK11.stalkSpecializes_surjective_of_isIso_stalkMap
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isFinite_of_isIso_stalkMap
open _root_.AlgebraicCurve.CurveModel
universe u v
open CategoryTheory AlgebraicGeometry AlgebraicCurve TopologicalSpace
namespace NuFinK11
Lean source · statement
theorem stalkSpecializes_surjective_of_isIso_stalkMap {X Y : Scheme.{u}} (f : X ⟶ Y) (x x' : X) (h
  : x ⤳ x')
    (he : f.base x = f.base x') [IsIso (f.stalkMap x)] :
    Function.Surjective (X.presheaf.stalkSpecializes h)
theorem

eq_genericPoint_of_stalkSpecializes_surjective

L77 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isFinite_of_isIso_stalkMap.NuFinK11.eq_genericPoint_of_stalkSpecializes_surjective
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isFinite_of_isIso_stalkMap
open _root_.AlgebraicCurve.CurveModel
universe u v
open CategoryTheory AlgebraicGeometry AlgebraicCurve TopologicalSpace
namespace NuFinK11
Lean source · statement
theorem eq_genericPoint_of_stalkSpecializes_surjective {X : Scheme.{u}} [IsIntegral X] (x : X)
    (hsurj : Function.Surjective (X.presheaf.stalkSpecializes ((genericPoint_spec X).specializes
      (Set.mem_univ x)))) :
    x = genericPoint X
theorem

finite_of_isClosed_of_forall_isClosed_singleton

L89 ↗
AlgebraicCurves.Models.Proofs.CurveModel_isFinite_of_isIso_stalkMap.NuFinK11.finite_of_isClosed_of_forall_isClosed_singleton
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isFinite_of_isIso_stalkMap
open _root_.AlgebraicCurve.CurveModel
universe u v
open CategoryTheory AlgebraicGeometry AlgebraicCurve TopologicalSpace
namespace NuFinK11
Lean source · statement
theorem finite_of_isClosed_of_forall_isClosed_singleton {α : Type*} [TopologicalSpace α]
  [NoetherianSpace α] [QuasiSober α]
    (Z : Set α) (hZ : IsClosed Z) (hpt : ∀ z ∈ Z, IsClosed ({z} : Set α)) : Z.Finite
theorem

isFinite_of_isIso_stalkMap

L105 ↗
AlgebraicCurve.CurveModel.isFinite_of_isIso_stalkMap
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_isFinite_of_isIso_stalkMap
open _root_.AlgebraicCurve.CurveModel
universe u v
open CategoryTheory AlgebraicGeometry AlgebraicCurve TopologicalSpace
Lean source · statement
theorem _root_.AlgebraicCurve.CurveModel.isFinite_of_isIso_stalkMap
    (k : Type u) [Field k] [IsAlgClosed k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k))
      [IsIntegral C] [IsProper c]
    {F : Type v} [Field F] [Algebra k F] (M : AlgebraicCurve.CurveModel k F)
    (ν : M.C ⟶ C) (hν : ν ≫ c = M.toBase)
    (hbir : IsIso (ν.stalkMap (genericPoint M.C))) :
    IsFinite ν

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.