Module

Module_Flat_of_isLocalHom_of_isRegularLocalRing_of_ringKrullDim_quotient_eq_zero.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Module_Flat_of_isLocalHom_of_isRegularLocalRing_of_ringKrullDim_quotient_eq_zero

3 declarations indexed from sourceView source ↗

Module documentation

Module Flat of is Local Hom of is Regular Local Ring of ring Krull Dim quotient eq zero

Imports6

Imported by4

theorem

core

L35 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_of_isLocalHom_of_isRegularLocalRing_of_ringKrullDim_quotient_eq_zero.Ws14MiracleFlat.core

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_of_isLocalHom_of_isRegularLocalRing_of_ringKrullDim_quotient_eq_zero
open IsLocalRing CategoryTheory CategoryTheory.Limits
namespace Ws14MiracleFlat
universe u

Lean source · statement

theorem core (R S : Type u) [CommRing R] [CommRing S]
    [IsRegularLocalRing R] [IsRegularLocalRing S] [Algebra R S]
    [IsLocalHom (algebraMap R S)]
    (hfib : ringKrullDim (S ⧸ (maximalIdeal R).map (algebraMap R S)) = 0)
    (hdim : ringKrullDim S = ringKrullDim R) :
    Module.Flat R S

theorem

main

L75 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_of_isLocalHom_of_isRegularLocalRing_of_ringKrullDim_quotient_eq_zero.Ws14MiracleFlat.main

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_of_isLocalHom_of_isRegularLocalRing_of_ringKrullDim_quotient_eq_zero
open IsLocalRing CategoryTheory CategoryTheory.Limits
namespace Ws14MiracleFlat
universe u
universe v

Lean source · statement

theorem main (R : Type u) (S : Type v) [CommRing R] [CommRing S]
    [IsRegularLocalRing R] [IsRegularLocalRing S] [Algebra R S]
    [IsLocalHom (algebraMap R S)]
    (hfib : ringKrullDim (S ⧸ (maximalIdeal R).map (algebraMap R S)) = 0)
    (hdim : ringKrullDim S = ringKrullDim R) :
    Module.Flat R S

theorem

of_isLocalHom_of_isRegularLocalRing_of_ringKrullDim_quotient_eq_zero

L127 ↗

Module.Flat.of_isLocalHom_of_isRegularLocalRing_of_ringKrullDim_quotient_eq_zero

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_of_isLocalHom_of_isRegularLocalRing_of_ringKrullDim_quotient_eq_zero
open IsLocalRing CategoryTheory CategoryTheory.Limits
open IsLocalRing in

Lean source · statement

theorem _root_.Module.Flat.of_isLocalHom_of_isRegularLocalRing_of_ringKrullDim_quotient_eq_zero
    (R S : Type*) [CommRing R] [CommRing S]
    [IsRegularLocalRing R] [IsRegularLocalRing S] [Algebra R S]
    [IsLocalHom (algebraMap R S)]
    (hfib : ringKrullDim (S ⧸ (maximalIdeal R).map (algebraMap R S)) = 0)
    (hdim : ringKrullDim S = ringKrullDim R) :
    Module.Flat R S

Module documentation

Module Flat of is Local Hom of is Regular Local Ring of ring Krull Dim quotient eq zero

Declarations

core

main

of_isLocalHom_of_isRegularLocalRing_of_ringKrullDim_quotient_eq_zero