Module

FreeModuleRegularSequenceAux.lean

Nyll.SchemeTheory.RingTheory.FreeModuleRegularSequenceAux

1 declaration indexed from sourceView source ↗

Module documentation

Weak regularity on a nontrivial free module

Weak regularity of a sequence on a nontrivial free module is equivalent to weak regularity on the ring. This auxiliary proof compares quotient modules and proceeds by induction on the sequence length.

Imports5

Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Mathlib.RingTheory.Regular.RegularSequence
Mathlib.RingTheory.QuotSMulTop
Nyll.SchemeTheory.RingTheory.FreeModuleRegularScalar
Mathlib.RingTheory.TensorProduct.Free

Imported by2

theorem

isWeaklyRegular_of_free_aux

L39 ↗

RingTheory.Sequence.isWeaklyRegular_of_free_aux

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace RingTheory_Sequence_isWeaklyRegular_of_free_aux
open scoped Pointwise TensorProduct

Lean source · statement

theorem _root_.RingTheory.Sequence.isWeaklyRegular_of_free_aux.{u, v}
    {R : Type u} {M : Type max u v} [CommRing R] [AddCommGroup M] [Module R M]
    [Module.Free R M] [Nontrivial M] {s : List R} :
    RingTheory.Sequence.IsWeaklyRegular M s ↔ RingTheory.Sequence.IsWeaklyRegular R s

Module documentation

Weak regularity on a nontrivial free module

Declarations

isWeaklyRegular_of_free_aux