NYLL
Module

stalkMap_surjective_and_ker_stalkMap_eq_map_ker_of_isPullback_of_surjective.lean

Nyll.AlgebraicCurves.Geometry.Schemes.stalkMap_surjective_and_ker_stalkMap_eq_map_ker_of_isPullback_of_surjective
2 declarations indexed from sourceView source ↗

Module documentation

stalk Map surjective and ker stalk Map eq map ker of is Pullback of surjective

Imports1
Imported by1

Declarations

theorem

fromSpec_comp_eq_specMap_of_hom_spec

L36 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.stalkMap_surjective_and_ker_stalkMap_eq_map_ker_of_isPullback_of_surjective.AlgebraicGeometry.IsAffineOpen.fromSpec_comp_eq_specMap_of_hom_spec
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace stalkMap_surjective_and_ker_stalkMap_eq_map_ker_of_isPullback_of_surjective
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
universe u
open scoped _root_.AlgebraicGeometry _root_.AlgebraicGeometry.IsAffineOpen in
Lean source · statement
theorem AlgebraicGeometry.IsAffineOpen.fromSpec_comp_eq_specMap_of_hom_spec
    {O : Type u} [CommRing O] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of O)) {U : X.Opens} (hU
      : IsAffineOpen U) :
    hU.fromSpec ≫ f = Spec.map (CommRingCat.ofHom ((X.presheaf.map (homOfLE (le_top : U ≤
      ⊤)).op).hom.comp
      ((f.appTop).hom.comp (Scheme.ΓSpecIso (CommRingCat.of O)).inv.hom)))
theorem

stalkMap_surjective_and_ker_stalkMap_eq_map_ker_of_isPullback_of_surjective

L56 ↗
AlgebraicGeometry.stalkMap_surjective_and_ker_stalkMap_eq_map_ker_of_isPullback_of_surjective
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits
universe u
open _root_.AlgebraicCurves.Geometry.Schemes.Proofs in
open stalkMap_surjective_and_ker_stalkMap_eq_map_ker_of_isPullback_of_surjective in
Lean source · statement
theorem stalkMap_surjective_and_ker_stalkMap_eq_map_ker_of_isPullback_of_surjective
    {O κ : Type u} [CommRing O] [CommRing κ] (q : O →+* κ) (hq : Function.Surjective q)
    {X Y : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of O)) (g : Y ⟶ X) (t : Y ⟶ Spec (CommRingCat.of
      κ))
    (H : IsPullback g t f (Spec.map (CommRingCat.ofHom q))) (y : Y) :
    Function.Surjective (g.stalkMap y).hom ∧
      RingHom.ker (g.stalkMap y).hom =
        Ideal.map ((X.presheaf.germ ⊤ (g.base y) trivial).hom.comp
          ((f.appTop).hom.comp (Scheme.ΓSpecIso (CommRingCat.of O)).inv.hom)) (RingHom.ker q)

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