NYLL
Module

ringKrullDim_stalk_eq_of_locallyQuasiFinite_endomorphism.lean

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

Module documentation

ring Krull Dim stalk eq of locally Quasi Finite endomorphism

Imports62
  • Batteries.Tactic.Init
  • Mathlib.Algebra.Algebra.Basic
  • Mathlib.Algebra.Algebra.Defs
  • Mathlib.Algebra.Algebra.Equiv
  • Mathlib.Algebra.Algebra.Hom
  • Mathlib.Algebra.Algebra.Subalgebra.Basic
  • Mathlib.Algebra.Algebra.Tower
  • Mathlib.Algebra.Category.Ring.Basic
  • Mathlib.Algebra.Group.Hom.Defs
  • Mathlib.Algebra.Group.Monoid
  • Mathlib.Algebra.Group.Submonoid.Membership
  • Mathlib.Algebra.GroupWithZero.NonZeroDivisors
  • Mathlib.Algebra.Module.Submodule.Lattice
  • Mathlib.Algebra.NeZero
  • Mathlib.Algebra.Ring.Hom.Defs
  • Mathlib.AlgebraicGeometry.AffineScheme
  • Mathlib.AlgebraicGeometry.FunctionField
  • Mathlib.AlgebraicGeometry.Morphisms.FiniteType
  • Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
  • Mathlib.AlgebraicGeometry.Properties
  • Mathlib.AlgebraicGeometry.Scheme
  • Mathlib.CategoryTheory.Category.Basic
  • Mathlib.Data.Set.Disjoint
  • Mathlib.GroupTheory.MonoidLocalization.Away
  • Mathlib.GroupTheory.OreLocalization.Basic
  • Mathlib.Order.BoundedOrder.Basic
  • Mathlib.Order.Defs.PartialOrder
  • Mathlib.RingTheory.Algebraic.Basic
  • Mathlib.RingTheory.Algebraic.Integral
  • Mathlib.RingTheory.AlgebraicIndependent.Basic
  • Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
  • Mathlib.RingTheory.AlgebraicIndependent.Transcendental
  • Mathlib.RingTheory.FiniteType
  • Mathlib.RingTheory.Finiteness.Basic
  • Mathlib.RingTheory.Finiteness.Defs
  • Mathlib.RingTheory.Ideal.Height
  • Mathlib.RingTheory.Ideal.Maps
  • Mathlib.RingTheory.Ideal.Over
  • Mathlib.RingTheory.Ideal.Prime
  • Mathlib.RingTheory.Ideal.Quotient.Basic
  • Mathlib.RingTheory.Ideal.Quotient.Defs
  • Mathlib.RingTheory.Ideal.Quotient.Operations
  • Mathlib.RingTheory.IntegralClosure.Algebra.Basic
  • Mathlib.RingTheory.IntegralClosure.Algebra.Defs
  • Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
  • Mathlib.RingTheory.KrullDimension.Basic
  • Mathlib.RingTheory.Localization.AtPrime.Basic
  • Mathlib.RingTheory.Localization.Away.Basic
  • Mathlib.RingTheory.Localization.Basic
  • Mathlib.RingTheory.Localization.Defs
  • Mathlib.RingTheory.Localization.FractionRing
  • Mathlib.RingTheory.Localization.Ideal
  • Mathlib.RingTheory.OreLocalization.Ring
  • Mathlib.RingTheory.QuasiFinite.Basic
  • Mathlib.RingTheory.Spectrum.Prime.Defs
  • Mathlib.RingTheory.ZariskisMainTheorem
  • Mathlib.Tactic.Conv
  • Mathlib.Topology.Sheaves.CommRingCat
  • Mathlib.Topology.Sheaves.Stalks
  • Mathlib.Topology.Sober
  • Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Ideal_height_eq_height_under_of_finiteType_of_isIntegral
  • Nyll.AlgebraicCurves.Foundations.Algebra.Algebra_trdeg_quotient_lt
Imported by2

Declarations

theorem

height_eq_height_under_of_quasiFiniteAt

L96 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ringKrullDim_stalk_eq_of_locallyQuasiFinite_endomorphism.LQFheight.height_eq_height_under_of_quasiFiniteAt
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace ringKrullDim_stalk_eq_of_locallyQuasiFinite_endomorphism
universe u
open CategoryTheory AlgebraicGeometry
namespace LQFheight
open _root_.Algebra
Lean source · statement
theorem height_eq_height_under_of_quasiFiniteAt
    (k A B : Type u) [Field k] [CommRing A] [IsDomain A] [Algebra k A] [Algebra.FiniteType k A]
    [CommRing B] [IsDomain B] [Algebra k B] [Algebra.FiniteType k B]
    [Algebra A B] [IsScalarTower k A B] [FaithfulSMul A B]
    (q : Ideal B) [q.IsPrime] [Algebra.QuasiFiniteAt A q] :
    q.height = (q.under A).height
theorem

injective_of_quasiFiniteAt_of_trdeg_eq

L154 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ringKrullDim_stalk_eq_of_locallyQuasiFinite_endomorphism.LQFheight.injective_of_quasiFiniteAt_of_trdeg_eq
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace ringKrullDim_stalk_eq_of_locallyQuasiFinite_endomorphism
universe u
open CategoryTheory AlgebraicGeometry
namespace LQFheight
open _root_.Algebra
Lean source · statement
theorem injective_of_quasiFiniteAt_of_trdeg_eq
    (k A B : Type u) [Field k] [CommRing A] [IsDomain A] [Algebra k A] [Algebra.FiniteType k A]
    [CommRing B] [IsDomain B] [Algebra k B] [Algebra.FiniteType k B]
    [Algebra A B] [IsScalarTower k A B]
    (htr : Algebra.trdeg k A = Algebra.trdeg k B)
    (q : Ideal B) [q.IsPrime] [Algebra.QuasiFiniteAt A q] :
    Function.Injective (algebraMap A B)
def

secAlg

L238 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ringKrullDim_stalk_eq_of_locallyQuasiFinite_endomorphism.LQFdimEndo.secAlg
Documentation

The base-ring homomorphism to sections on an open induced by the scheme structure morphism.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace ringKrullDim_stalk_eq_of_locallyQuasiFinite_endomorphism
universe u
open CategoryTheory AlgebraicGeometry
namespace LQFdimEndo
open CategoryTheory AlgebraicGeometry
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

appLE_comp_secAlg

L241 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ringKrullDim_stalk_eq_of_locallyQuasiFinite_endomorphism.LQFdimEndo.appLE_comp_secAlg
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace ringKrullDim_stalk_eq_of_locallyQuasiFinite_endomorphism
universe u
open CategoryTheory AlgebraicGeometry
namespace LQFdimEndo
open CategoryTheory AlgebraicGeometry
variable {k : Type u} [Field k] {X : Scheme.{u}} {f : X ⟶ Spec (CommRingCat.of k)}
Lean source · statement
theorem appLE_comp_secAlg (h : X ⟶ X) (hov : h ≫ f = f) (U V : X.Opens) (e : V ≤ h ⁻¹ᵁ U) :
    (h.appLE U V e).hom.comp (secAlg f U) = secAlg f V
theorem

germ_comp_secAlg

L251 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ringKrullDim_stalk_eq_of_locallyQuasiFinite_endomorphism.LQFdimEndo.germ_comp_secAlg
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace ringKrullDim_stalk_eq_of_locallyQuasiFinite_endomorphism
universe u
open CategoryTheory AlgebraicGeometry
namespace LQFdimEndo
open CategoryTheory AlgebraicGeometry
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

L264 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ringKrullDim_stalk_eq_of_locallyQuasiFinite_endomorphism.LQFdimEndo.main
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace ringKrullDim_stalk_eq_of_locallyQuasiFinite_endomorphism
universe u
open CategoryTheory AlgebraicGeometry
namespace LQFdimEndo
open CategoryTheory AlgebraicGeometry
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) [LocallyQuasiFinite h] (x : X) :
    ringKrullDim (X.presheaf.stalk x) = ringKrullDim (X.presheaf.stalk (h.base x))
theorem

ringKrullDim_stalk_eq_of_locallyQuasiFinite_endomorphism

L338 ↗
AlgebraicGeometry.ringKrullDim_stalk_eq_of_locallyQuasiFinite_endomorphism
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace ringKrullDim_stalk_eq_of_locallyQuasiFinite_endomorphism
universe u
open CategoryTheory AlgebraicGeometry
Lean source · statement
theorem _root_.AlgebraicGeometry.ringKrullDim_stalk_eq_of_locallyQuasiFinite_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) [LocallyQuasiFinite h] (x : X) :
    ringKrullDim (X.presheaf.stalk x) = ringKrullDim (X.presheaf.stalk (h.base x))

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