Module

Scheme_Hom_map_germ_ker_ideal_eq_ker_stalkMap.lean

Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_Hom_map_germ_ker_ideal_eq_ker_stalkMap

2 declarations indexed from sourceView source ↗

Module documentation

Scheme Hom map germ ker ideal eq ker stalk Map

Imports5

Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Mathlib.AlgebraicGeometry.AffineScheme
Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Mathlib.RingTheory.Localization.Basic
Mathlib.Tactic.Set

Imported by2

theorem

map_germ_ker_ideal_eq_ker_stalkMap

L33 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Hom_map_germ_ker_ideal_eq_ker_stalkMap.PtGerm.map_germ_ker_ideal_eq_ker_stalkMap

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Hom_map_germ_ker_ideal_eq_ker_stalkMap
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace
namespace PtGerm

Lean source · statement

theorem map_germ_ker_ideal_eq_ker_stalkMap {X Y : Scheme.{u}} (σ : Y ⟶ X) [IsClosedImmersion σ] (y
  : Y)
    (U : X.affineOpens) (hx : σ.base y ∈ (U : X.Opens)) :
    Ideal.map (X.presheaf.germ (U : X.Opens) (σ.base y) hx).hom (σ.ker.ideal U) = RingHom.ker
      (σ.stalkMap y).hom

theorem

map_germ_ker_ideal_eq_ker_stalkMap

L95 ↗

AlgebraicGeometry.Scheme.Hom.map_germ_ker_ideal_eq_ker_stalkMap

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Hom_map_germ_ker_ideal_eq_ker_stalkMap
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.Hom.map_germ_ker_ideal_eq_ker_stalkMap {X Y : Scheme.{u}}
  (σ : Y ⟶ X) [IsClosedImmersion σ]
    (y : Y) (U : X.affineOpens) (hx : σ.base y ∈ (U : X.Opens)) :
    Ideal.map (X.presheaf.germ (U : X.Opens) (σ.base y) hx).hom (σ.ker.ideal U) = RingHom.ker
      (σ.stalkMap y).hom

Module documentation

Scheme Hom map germ ker ideal eq ker stalk Map

Declarations

map_germ_ker_ideal_eq_ker_stalkMap

map_germ_ker_ideal_eq_ker_stalkMap