Module

ringKrullDim_stalk_eq_of_isFinite_endomorphism.lean

Nyll.AlgebraicCurves.Geometry.Schemes.ringKrullDim_stalk_eq_of_isFinite_endomorphism

5 declarations indexed from sourceView source ↗

Module documentation

ring Krull Dim stalk eq of is Finite endomorphism

Imports4

Mathlib.AlgebraicGeometry.FunctionField
Mathlib.AlgebraicGeometry.Morphisms.Finite
Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Ideal_height_eq_height_under_of_finiteType_of_isIntegral
Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.AlgHom_injective_of_finite_of_isFractionRing

Imported by3

def

secAlg

L36 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.ringKrullDim_stalk_eq_of_isFinite_endomorphism.P2mWs11DimEndo.secAlg

Documentation

The scalar ring homomorphism into sections on an open of a scheme over the base field.

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ringKrullDim_stalk_eq_of_isFinite_endomorphism
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mWs11DimEndo
variable {k : Type u} [Field k] {X : Scheme.{u}} {f : X ⟶ Spec (CommRingCat.of k)}

Lean source · statement

def secAlg (f : X ⟶ Spec (CommRingCat.of k)) (U : X.Opens) : k →+* Γ(X, U)

theorem

app_comp_secAlg

L40 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.ringKrullDim_stalk_eq_of_isFinite_endomorphism.P2mWs11DimEndo.app_comp_secAlg

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ringKrullDim_stalk_eq_of_isFinite_endomorphism
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mWs11DimEndo
variable {k : Type u} [Field k] {X : Scheme.{u}} {f : X ⟶ Spec (CommRingCat.of k)}

Lean source · statement

theorem app_comp_secAlg (h : X ⟶ X) (hov : h ≫ f = f) (U : X.Opens) :
    (h.app U).hom.comp (secAlg f U) = secAlg f (h ⁻¹ᵁ U)

theorem

germ_comp_secAlg

L51 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.ringKrullDim_stalk_eq_of_isFinite_endomorphism.P2mWs11DimEndo.germ_comp_secAlg

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ringKrullDim_stalk_eq_of_isFinite_endomorphism
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mWs11DimEndo
variable {k : Type u} [Field k] {X : Scheme.{u}} {f : X ⟶ Spec (CommRingCat.of k)}

Lean source · statement

theorem germ_comp_secAlg (U : X.Opens) (x : X) (hx : x ∈ U) :
    (X.presheaf.germ U x hx).hom.comp (secAlg f U) =
      ((Spec (CommRingCat.of k)).presheaf.germ ⊤ (f.base x) trivial ≫ f.stalkMap x).hom.comp
        (Scheme.ΓSpecIso (CommRingCat.of k)).inv.hom

theorem

main

L65 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.ringKrullDim_stalk_eq_of_isFinite_endomorphism.P2mWs11DimEndo.main

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ringKrullDim_stalk_eq_of_isFinite_endomorphism
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mWs11DimEndo
variable {k : Type u} [Field k] {X : Scheme.{u}} {f : X ⟶ Spec (CommRingCat.of k)}

Lean source · statement

theorem main [LocallyOfFiniteType f] [IsIntegral X]
    (h : X ⟶ X) (hov : h ≫ f = f) [IsFinite h] (x : X) :
    ringKrullDim (X.presheaf.stalk x) = ringKrullDim (X.presheaf.stalk (h.base x))

theorem

ringKrullDim_stalk_eq_of_isFinite_endomorphism

L129 ↗

AlgebraicGeometry.ringKrullDim_stalk_eq_of_isFinite_endomorphism

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ringKrullDim_stalk_eq_of_isFinite_endomorphism
universe u
open CategoryTheory AlgebraicGeometry

Lean source · statement

theorem _root_.AlgebraicGeometry.ringKrullDim_stalk_eq_of_isFinite_endomorphism
    {k : Type u} [Field k] {X : Scheme.{u}} {f : X ⟶ Spec (CommRingCat.of k)}
    [LocallyOfFiniteType f] [IsIntegral X]
    (h : X ⟶ X) (hov : h ≫ f = f) [IsFinite h] (x : X) :
    ringKrullDim (X.presheaf.stalk x) = ringKrullDim (X.presheaf.stalk (h.base x))

Module documentation

ring Krull Dim stalk eq of is Finite endomorphism

Declarations

secAlg

app_comp_secAlg

germ_comp_secAlg

main

ringKrullDim_stalk_eq_of_isFinite_endomorphism