Module

IsFinite_ringKrullDim_stalk_quotient_eq_zero.lean

Nyll.AlgebraicCurves.Geometry.Schemes.IsFinite_ringKrullDim_stalk_quotient_eq_zero

2 declarations indexed from sourceView source ↗

Module documentation

Is Finite ring Krull Dim stalk quotient eq zero

Imports6

Mathlib.AlgebraicGeometry.Morphisms.Finite
Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Mathlib.RingTheory.LocalRing.ResidueField.Instances
Mathlib.RingTheory.TensorProduct.Quotient
Mathlib.RingTheory.HopkinsLevitzki

Imported by3

theorem

ringKrullDim_quotient_map_maximalIdeal_eq_zero

L36 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.IsFinite_ringKrullDim_stalk_quotient_eq_zero.FD0625672e.ringKrullDim_quotient_map_maximalIdeal_eq_zero

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.IsFinite_ringKrullDim_stalk_quotient_eq_zero
universe u
open CategoryTheory AlgebraicGeometry IsLocalRing
namespace FD0625672e
open scoped TensorProduct

Lean source · statement

theorem ringKrullDim_quotient_map_maximalIdeal_eq_zero
    (R S : Type*) [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S] [Algebra R S]
    [IsLocalHom (algebraMap R S)] [Algebra.QuasiFinite R S] :
    ringKrullDim (S ⧸ (maximalIdeal R).map (algebraMap R S)) = 0

theorem

ringKrullDim_stalk_quotient_eq_zero

L58 ↗

AlgebraicGeometry.IsFinite.ringKrullDim_stalk_quotient_eq_zero

Source context 4 commands