Module

CommonRegularElement.lean

Nyll.SchemeTheory.RingTheory.CommonRegularElement

1 declaration indexed from sourceView source ↗

Module documentation

A common regular element for two finite modules

If the maximal ideal of a noetherian local ring is not an associated prime of either finite module, it contains an element whose scalar multiplication is injective on both modules.

Imports4

Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
Mathlib.RingTheory.Regular.IsSMulRegular
Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
Mathlib.RingTheory.Ideal.Prime

Imported by3

theorem

exists_mem_maximalIdeal_isSMulRegular_isSMulRegular

L31 ↗

Module.exists_mem_maximalIdeal_isSMulRegular_isSMulRegular

Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_exists_mem_maximalIdeal_isSMulRegular_isSMulRegular

Lean source · statement

theorem _root_.Module.exists_mem_maximalIdeal_isSMulRegular_isSMulRegular
    {R : Type*} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (N₁ N₂ : Type*) [AddCommGroup N₁] [Module R N₁] [Module.Finite R N₁]
    [AddCommGroup N₂] [Module R N₂] [Module.Finite R N₂]
    (h₁ : ¬ IsAssociatedPrime (IsLocalRing.maximalIdeal R) N₁)
    (h₂ : ¬ IsAssociatedPrime (IsLocalRing.maximalIdeal R) N₂) :
    ∃ z ∈ IsLocalRing.maximalIdeal R, IsSMulRegular N₁ z ∧ IsSMulRegular N₂ z

Module documentation

A common regular element for two finite modules

Declarations

exists_mem_maximalIdeal_isSMulRegular_isSMulRegular