Module

maximalIdeal_stalk_eq_span_stalkSpecializes_of_ker_stalkMap_eq_span.lean

Nyll.AlgebraicCurves.Geometry.Schemes.maximalIdeal_stalk_eq_span_stalkSpecializes_of_ker_stalkMap_eq_span

4 declarations indexed from sourceView source ↗

Module documentation

maximal Ideal stalk eq span stalk Specializes of ker stalk Map eq span

Imports4

Mathlib.AlgebraicGeometry.FunctionField
Mathlib.AlgebraicGeometry.Scheme
Mathlib.RingTheory.Localization.LocalizationLocalization
Mathlib.RingTheory.Localization.Ideal

Imported by1

Nyll.AlgebraicCurves.Geometry.Schemes.All

theorem

map_comap_stalkSpecializes

L42 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.maximalIdeal_stalk_eq_span_stalkSpecializes_of_ker_stalkMap_eq_span.AlgebraicGeometry.Scheme.map_comap_stalkSpecializes

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace maximalIdeal_stalk_eq_span_stalkSpecializes_of_ker_stalkMap_eq_span
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Topology
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open scoped _root_.AlgebraicGeometry.Scheme in

Lean source · statement

theorem Scheme.map_comap_stalkSpecializes {X : Scheme.{u}} {x y : X} (h : y ⤳ x)
    (J : Ideal (X.presheaf.stalk y)) :
    (J.comap (X.presheaf.stalkSpecializes h).hom).map (X.presheaf.stalkSpecializes h).hom = J

theorem

functionField_algebraMap_injective

L73 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.maximalIdeal_stalk_eq_span_stalkSpecializes_of_ker_stalkMap_eq_span.AlgebraicGeometry.Scheme.functionField_algebraMap_injective

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace maximalIdeal_stalk_eq_span_stalkSpecializes_of_ker_stalkMap_eq_span
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Topology
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry

Lean source · statement

theorem Scheme.functionField_algebraMap_injective (Y : Scheme.{u}) [IsIntegral Y]
    (y : Y) : Function.Injective (algebraMap (Y.presheaf.stalk y) Y.functionField)

theorem

stalkSpecializes_genericPoint_closedPoint_injective

L78 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.maximalIdeal_stalk_eq_span_stalkSpecializes_of_ker_stalkMap_eq_span.AlgebraicGeometry.Scheme.stalkSpecializes_genericPoint_closedPoint_injective

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace maximalIdeal_stalk_eq_span_stalkSpecializes_of_ker_stalkMap_eq_span
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Topology
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open scoped _root_.AlgebraicGeometry.Scheme in

Lean source · statement

theorem Scheme.stalkSpecializes_genericPoint_closedPoint_injective
    (A : Type u) [CommRing A] [IsDomain A] [IsLocalRing A] :
    Function.Injective ((Spec (CommRingCat.of A)).presheaf.stalkSpecializes
      (genericPoint_specializes (IsLocalRing.closedPoint A))).hom

theorem

maximalIdeal_stalk_eq_span_stalkSpecializes_of_ker_stalkMap_eq_span

L87 ↗

AlgebraicGeometry.maximalIdeal_stalk_eq_span_stalkSpecializes_of_ker_stalkMap_eq_span

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace maximalIdeal_stalk_eq_span_stalkSpecializes_of_ker_stalkMap_eq_span
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Topology
open maximalIdeal_stalk_eq_span_stalkSpecializes_of_ker_stalkMap_eq_span.AlgebraicGeometry.Scheme in

Lean source · statement

theorem _root_.AlgebraicGeometry.maximalIdeal_stalk_eq_span_stalkSpecializes_of_ker_stalkMap_eq_span
    {A : Type u} [CommRing A] [IsDomain A] [IsLocalRing A] {X : Scheme.{u}} (c : X ⟶ Spec
      (CommRingCat.of A))
    (σ : Spec (CommRingCat.of A) ⟶ X) (_hσ : σ ≫ c = 𝟙 _)
    (t : X.presheaf.stalk (σ.base (IsLocalRing.closedPoint A)))
    (ht : RingHom.ker (σ.stalkMap (IsLocalRing.closedPoint A)).hom = Ideal.span {t}) :
    IsLocalRing.maximalIdeal (X.presheaf.stalk (σ.base (genericPoint ↥(Spec (CommRingCat.of A))))) =
      Ideal.span {(X.presheaf.stalkSpecializes
        (((genericPoint_specializes (IsLocalRing.closedPoint A)).map σ.continuous) :
          σ.base (genericPoint ↥(Spec (CommRingCat.of A))) ⤳ σ.base (IsLocalRing.closedPoint
            A))).hom t}

Module documentation

maximal Ideal stalk eq span stalk Specializes of ker stalk Map eq span

Declarations

map_comap_stalkSpecializes

functionField_algebraMap_injective

stalkSpecializes_genericPoint_closedPoint_injective

maximalIdeal_stalk_eq_span_stalkSpecializes_of_ker_stalkMap_eq_span