Module

LocallyQuasiFinite_ringKrullDim_stalk_quotient_eq_zero.lean

Nyll.AlgebraicCurves.Geometry.Schemes.LocallyQuasiFinite_ringKrullDim_stalk_quotient_eq_zero

2 declarations indexed from sourceView source ↗

Module documentation

Locally Quasi Finite ring Krull Dim stalk quotient eq zero

Imports9

Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Mathlib.RingTheory.QuasiFinite.Basic
Mathlib.RingTheory.LocalRing.ResidueField.Fiber
Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Mathlib.RingTheory.LocalRing.RingHom.Basic
Mathlib.RingTheory.TensorProduct.Quotient
Mathlib.RingTheory.HopkinsLevitzki
Mathlib.RingTheory.KrullDimension.Zero
Mathlib.RingTheory.Artinian.Module

Imported by2

theorem

ringKrullDim_quotient_map_maximalIdeal_eq_zero

L40 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.LocallyQuasiFinite_ringKrullDim_stalk_quotient_eq_zero.LQFfibre.ringKrullDim_quotient_map_maximalIdeal_eq_zero

Source context 7 commands

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

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

L62 ↗

AlgebraicGeometry.LocallyQuasiFinite.ringKrullDim_stalk_quotient_eq_zero

Source context 5 commands