NYLL
Module

eq_of_section_of_base_closedPoint_eq_of_ker_stalkMap_le.lean

Nyll.AlgebraicCurves.Geometry.Schemes.eq_of_section_of_base_closedPoint_eq_of_ker_stalkMap_le
7 declarations indexed from sourceView source ↗

Module documentation

eq of section of base closed Point eq of ker stalk Map le

Imports1
  • Mathlib.AlgebraicGeometry.Stalk
Imported by1

Declarations

theorem

presheaf_map_eqToHom_op_apply

L30 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.eq_of_section_of_base_closedPoint_eq_of_ker_stalkMap_le.B12C5.presheaf_map_eqToHom_op_apply
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace eq_of_section_of_base_closedPoint_eq_of_ker_stalkMap_le
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Topology
namespace B12C5
Lean source · full declaration
theorem presheaf_map_eqToHom_op_apply {X : Scheme.{u}} {U V : X.Opens} (h : U = V)
    (t : Γ(X, V)) : (X.presheaf.map (eqToHom h).op).hom t = cast (by rw [h]) t := by
  subst h; simp
def

const

L38 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.eq_of_section_of_base_closedPoint_eq_of_ker_stalkMap_le.B12C5.const
Documentation

The global section obtained by pulling back an element of the base ring.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace eq_of_section_of_base_closedPoint_eq_of_ker_stalkMap_le
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Topology
namespace B12C5
variable {A : Type u} [CommRing A] [IsLocalRing A] {X : Scheme.{u}} (c : X ⟶ Spec (CommRingCat.of
  A))
Lean source · statement
def const (a : A) : Γ(X, ⊤)
theorem

app_top_const

L41 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.eq_of_section_of_base_closedPoint_eq_of_ker_stalkMap_le.B12C5.app_top_const
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace eq_of_section_of_base_closedPoint_eq_of_ker_stalkMap_le
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Topology
namespace B12C5
variable {A : Type u} [CommRing A] [IsLocalRing A] {X : Scheme.{u}} (c : X ⟶ Spec (CommRingCat.of
  A))
omit [IsLocalRing A] in
Lean source · statement
theorem app_top_const (σ : Spec (CommRingCat.of A) ⟶ X) (hσ : σ ≫ c = 𝟙 _) (a : A) :
    (σ.app ⊤).hom (const c a) = (Scheme.ΓSpecIso (CommRingCat.of A)).inv.hom a
theorem

stalkClosedPointTo_germ_const

L50 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.eq_of_section_of_base_closedPoint_eq_of_ker_stalkMap_le.B12C5.stalkClosedPointTo_germ_const
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace eq_of_section_of_base_closedPoint_eq_of_ker_stalkMap_le
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Topology
namespace B12C5
variable {A : Type u} [CommRing A] [IsLocalRing A] {X : Scheme.{u}} (c : X ⟶ Spec (CommRingCat.of
  A))
Lean source · statement
theorem stalkClosedPointTo_germ_const (σ : Spec (CommRingCat.of A) ⟶ X) (hσ : σ ≫ c = 𝟙 _) (a : A)
    (U : X.Opens) (hU : σ.base (IsLocalRing.closedPoint A) ∈ U) :
    (Scheme.stalkClosedPointTo σ).hom
      ((X.presheaf.germ U (σ.base (IsLocalRing.closedPoint A)) hU).hom
        ((X.presheaf.map (homOfLE (le_top (a := U))).op).hom (const c a))) = a
theorem

stalkClosedPointTo_apply

L94 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.eq_of_section_of_base_closedPoint_eq_of_ker_stalkMap_le.B12C5.stalkClosedPointTo_apply
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace eq_of_section_of_base_closedPoint_eq_of_ker_stalkMap_le
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Topology
namespace B12C5
variable {A : Type u} [CommRing A] [IsLocalRing A] {X : Scheme.{u}} (c : X ⟶ Spec (CommRingCat.of
  A))
omit [IsLocalRing A] in
Lean source · statement
theorem stalkClosedPointTo_apply [IsLocalRing A] (σ : Spec (CommRingCat.of A) ⟶ X) (z :
  X.presheaf.stalk (σ.base (IsLocalRing.closedPoint A))) :
    (Scheme.stalkClosedPointTo σ).hom z = (stalkClosedPointIso (CommRingCat.of A)).hom.hom
      ((σ.stalkMap (IsLocalRing.closedPoint A)).hom z)
theorem

stalkMap_eq_zero_iff

L99 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.eq_of_section_of_base_closedPoint_eq_of_ker_stalkMap_le.B12C5.stalkMap_eq_zero_iff
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace eq_of_section_of_base_closedPoint_eq_of_ker_stalkMap_le
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Topology
namespace B12C5
variable {A : Type u} [CommRing A] [IsLocalRing A] {X : Scheme.{u}} (c : X ⟶ Spec (CommRingCat.of
  A))
Lean source · statement
theorem stalkMap_eq_zero_iff (σ : Spec (CommRingCat.of A) ⟶ X) (z : X.presheaf.stalk (σ.base
  (IsLocalRing.closedPoint A))) :
    (σ.stalkMap (IsLocalRing.closedPoint A)).hom z = 0 ↔ (Scheme.stalkClosedPointTo σ).hom z = 0
theorem

eq_of_section_of_base_closedPoint_eq_of_ker_stalkMap_le

L113 ↗
AlgebraicGeometry.eq_of_section_of_base_closedPoint_eq_of_ker_stalkMap_le
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace eq_of_section_of_base_closedPoint_eq_of_ker_stalkMap_le
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Topology
open B12C5 in
Lean source · full declaration
theorem _root_.AlgebraicGeometry.eq_of_section_of_base_closedPoint_eq_of_ker_stalkMap_le
    {A : Type u} [CommRing A] [IsLocalRing A] {X : Scheme.{u}} (c : X ⟶ Spec (CommRingCat.of A))
    (σ σ' : Spec (CommRingCat.of A) ⟶ X) (hσ : σ ≫ c = 𝟙 _) (hσ' : σ' ≫ c = 𝟙 _)
    (hx : σ'.base (IsLocalRing.closedPoint A) = σ.base (IsLocalRing.closedPoint A))
    (hker : ∀ (U : X.Opens) (hU : σ.base (IsLocalRing.closedPoint A) ∈ U) (s : X.presheaf.obj
      (Opposite.op U)),
      (σ.stalkMap (IsLocalRing.closedPoint A)).hom (X.presheaf.germ U (σ.base
        (IsLocalRing.closedPoint A)) hU s) = 0 →
      (σ'.stalkMap (IsLocalRing.closedPoint A)).hom
        (X.presheaf.germ U (σ'.base (IsLocalRing.closedPoint A)) (by rw [hx]; exact hU) s) = 0) :
    σ = σ' := by
  let e := SpecToEquivOfLocalRing X (CommRingCat.of A)
  apply e.injective
  rw [SpecToEquivOfLocalRing_eq_iff]
  refine ⟨hx.symm, ?_⟩
  change Scheme.stalkClosedPointTo σ = (X.presheaf.stalkCongr _).hom ≫ Scheme.stalkClosedPointTo σ'
  apply TopCat.Presheaf.stalk_hom_ext
  intro U hxU
  let p : Spec (CommRingCat.of A) := IsLocalRing.closedPoint A
  have hxU' : σ' p ∈ U := by rw [hx]; exact hxU
  have hxIns : Inseparable (σ p) (σ' p) := Inseparable.of_eq hx.symm
  let e' : X.presheaf.stalk (σ p) ≅ X.presheaf.stalk (σ' p) := X.presheaf.stalkCongr hxIns
  have hs : σ' p ⤳ σ p := hxIns.ge
  have hg : X.presheaf.germ U (σ p) hxU ≫ e'.hom = X.presheaf.germ U (σ' p) hxU' :=
    X.presheaf.germ_stalkSpecializes hxU hs
  have hmove : X.presheaf.germ U (σ p) hxU ≫ (e'.hom ≫ Scheme.stalkClosedPointTo σ') =
      X.presheaf.germ U (σ' p) hxU' ≫ Scheme.stalkClosedPointTo σ' :=
    (Category.assoc (X.presheaf.germ U (σ p) hxU) e'.hom (Scheme.stalkClosedPointTo σ')).symm.trans
      (congrArg (fun g : Γ(X, U) ⟶ X.presheaf.stalk (σ' p) => g ≫ Scheme.stalkClosedPointTo σ') hg)
  change X.presheaf.germ U (σ p) hxU ≫ Scheme.stalkClosedPointTo σ =
    X.presheaf.germ U (σ p) hxU ≫ (e'.hom ≫ Scheme.stalkClosedPointTo σ')
  apply Eq.trans (b := X.presheaf.germ U (σ' p) hxU' ≫ Scheme.stalkClosedPointTo σ') _ hmove.symm
  ext s
  simp only [CommRingCat.hom_comp, RingHom.comp_apply]
  set a : A := (Scheme.stalkClosedPointTo σ).hom ((X.presheaf.germ U (σ.base
    (IsLocalRing.closedPoint A)) hxU).hom s) with ha
  let s₁ : X.presheaf.obj (Opposite.op U) := s - (X.presheaf.map (homOfLE (le_top (a :=
    U))).op).hom (const c a)
  have h1 : (Scheme.stalkClosedPointTo σ).hom ((X.presheaf.germ U (σ.base (IsLocalRing.closedPoint
    A)) hxU).hom s₁) = 0 := by
    simp only [s₁, map_sub, stalkClosedPointTo_germ_const c σ hσ a U hxU]
    exact sub_self a
  have h2 := hker U hxU s₁ ((stalkMap_eq_zero_iff σ _).2 h1)
  have h3 : (Scheme.stalkClosedPointTo σ').hom ((X.presheaf.germ U (σ'.base
    (IsLocalRing.closedPoint A)) hxU').hom s₁) = 0 :=
    (stalkMap_eq_zero_iff σ' _).1 h2
  simp only [s₁, map_sub, stalkClosedPointTo_germ_const c σ' hσ' a U hxU'] at h3
  exact (sub_eq_zero.1 h3).symm

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