Module

Scheme_eq_of_forall_mem_valuationSubring_of_isSeparated.lean

Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_eq_of_forall_mem_valuationSubring_of_isSeparated

3 declarations indexed from sourceView source ↗

Module documentation

Scheme eq of forall mem valuation Subring of is Separated

Imports3

Mathlib.AlgebraicGeometry.FunctionField
Mathlib.AlgebraicGeometry.Stalk
Mathlib.AlgebraicGeometry.ValuativeCriterion

Imported by1

Nyll.AlgebraicCurves.Geometry.Schemes.All

lemma

spec_hom_ext_of_injective

L32 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_eq_of_forall_mem_valuationSubring_of_isSeparated.M3aVCU.spec_hom_ext_of_injective

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_eq_of_forall_mem_valuationSubring_of_isSeparated
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing
namespace M3aVCU

Lean source · statement

lemma spec_hom_ext_of_injective {O V K : CommRingCat.{u}} (ι : V ⟶ K)
    (hι : Function.Injective ι.hom) (g₁ g₂ : Spec V ⟶ Spec O)
    (h : Spec.map ι ≫ g₁ = Spec.map ι ≫ g₂) : g₁ = g₂

lemma

exists_lift

L45 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_eq_of_forall_mem_valuationSubring_of_isSeparated.M3aVCU.exists_lift

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_eq_of_forall_mem_valuationSubring_of_isSeparated
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing
namespace M3aVCU

Lean source · statement

lemma exists_lift {X : Scheme.{u}} [IsIntegral X] (V : ValuationSubring X.functionField) (c : X)
    (hc : ∀ s : X.presheaf.stalk c, algebraMap (X.presheaf.stalk c) X.functionField s ∈ V)
    (hc' : ∀ s ∈ IsLocalRing.maximalIdeal (X.presheaf.stalk c),
      algebraMap (X.presheaf.stalk c) X.functionField s ∈ V.nonunits) :
    ∃ l : Spec (CommRingCat.of V) ⟶ X,
      Spec.map (CommRingCat.ofHom (algebraMap V X.functionField)) ≫ l =
        X.fromSpecStalk (genericPoint X) ∧
      l.base (closedPoint V) = c

theorem

eq_of_forall_mem_valuationSubring_of_isSeparated

L86 ↗

AlgebraicGeometry.Scheme.eq_of_forall_mem_valuationSubring_of_isSeparated

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_eq_of_forall_mem_valuationSubring_of_isSeparated
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing
open M3aVCU in

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.eq_of_forall_mem_valuationSubring_of_isSeparated
    {O : Type u} [CommRing O] {X : Scheme.{u}} [IsIntegral X]
    (f : X ⟶ Spec (CommRingCat.of O)) [IsSeparated f]
    (V : ValuationSubring X.functionField) (c₁ c₂ : X)
    (h₁ : ∀ s : X.presheaf.stalk c₁, algebraMap (X.presheaf.stalk c₁) X.functionField s ∈ V)
    (h₁' : ∀ s ∈ IsLocalRing.maximalIdeal (X.presheaf.stalk c₁),
      algebraMap (X.presheaf.stalk c₁) X.functionField s ∈ V.nonunits)
    (h₂ : ∀ s : X.presheaf.stalk c₂, algebraMap (X.presheaf.stalk c₂) X.functionField s ∈ V)
    (h₂' : ∀ s ∈ IsLocalRing.maximalIdeal (X.presheaf.stalk c₂),
      algebraMap (X.presheaf.stalk c₂) X.functionField s ∈ V.nonunits) :
    c₁ = c₂

Module documentation

Scheme eq of forall mem valuation Subring of is Separated

Declarations

spec_hom_ext_of_injective

exists_lift

eq_of_forall_mem_valuationSubring_of_isSeparated