Theorems · Theorem · commutative algebra

IsNoetherianRing.induction_on_isQuotientEquivQuotientPrime

∀ (A : Type u) [inst : CommRing A] [IsNoetherianRing A] ⦃M : Type v⦄ [inst_2 : AddCommGroup M] [inst_3 : Module A M]
  (x : Module.Finite A M)
  {motive : (N : Type v) → [inst_4 : AddCommGroup N] → [inst_5 : Module A N] → [Module.Finite A N] → Prop},
  (∀ (N : Type v) [inst_4 : AddCommGroup N] [inst_5 : Module A N] [inst : Module.Finite A N] [Subsingleton N],
      motive N) →
    (∀ (N : Type v) [inst_4 : AddCommGroup N] [inst_5 : Module A N] [inst_6 : Module.Finite A N] (p : PrimeSpectrum A)
        (a : N ≃ₗ[A] A ⧸ p.asIdeal), motive N) →
      (∀ (N₁ : Type v) [inst_4 : AddCommGroup N₁] [inst_5 : Module A N₁] [inst_6 : Module.Finite A N₁] (N₂ : Type v)
          [inst_7 : AddCommGroup N₂] [inst_8 : Module A N₂] [inst_9 : Module.Finite A N₂] (N₃ : Type v)
          [inst_10 : AddCommGroup N₃] [inst_11 : Module A N₃] [inst_12 : Module.Finite A N₃] (f : N₁ →ₗ[A] N₂)
          (g : N₂ →ₗ[A] N₃),
          Function.Injective ⇑f → Function.Surjective ⇑g → Function.Exact ⇑f ⇑g → motive N₁ → motive N₃ → motive N₂) →
        motive M

If a property on finitely generated modules over a Noetherian ring satisfies that: - it holds for zero module (it's formalized as it holds for any module which is subsingleton), - it holds for A ⧸ p for every prime ideal p of A (to avoid universe problem, it's formalized as it holds for any module isomorphic to A ⧸ p), - it is stable by short exact sequences, then the property holds for every finitely generated modules. NOTE: This should be the induction principle for M, but due to the bug https://github.com/leanprover/lean4/issues/4246 currently it is induction for Module.Finite A M.

Defined in

Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness

Cited by

1 results in Mathlib

Foundations

Depth 93 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingIsNoetherianRingAddCommGroupModule