English
An induction principle: if a property holds for zero modules, for modules isomorphic to A/p, and is stable under short exact sequences, then it holds for all finitely generated modules over a Noetherian ring.
Русский
Принцип индукции: если свойство выполняется для нулевого модуля, для модулей, изоморфных A/p, и сохраняется в коротких точных последовательностях, то оно выполняется для всех конечно порожденных модулей над Noetherovским кольцом.
LaTeX
$$Свойство для всех модулей M следует из условий: subsingleton, quotient by prime, и краткие точные последовательности.$$
Lean4
/-- 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`. -/
@[elab_as_elim]
theorem induction_on_isQuotientEquivQuotientPrime ⦃M : Type v⦄ [AddCommGroup M] [Module A M] (_ : Module.Finite A M)
{motive : (N : Type v) → [AddCommGroup N] → [Module A N] → [Module.Finite A N] → Prop}
(subsingleton : (N : Type v) → [AddCommGroup N] → [Module A N] → [Module.Finite A N] → [Subsingleton N] → motive N)
(quotient :
(N : Type v) →
[AddCommGroup N] → [Module A N] → [Module.Finite A N] → (p : PrimeSpectrum A) → (N ≃ₗ[A] A ⧸ p.1) → motive N)
(exact :
(N₁ : Type v) →
[AddCommGroup N₁] →
[Module A N₁] →
[Module.Finite A N₁] →
(N₂ : Type v) →
[AddCommGroup N₂] →
[Module A N₂] →
[Module.Finite A N₂] →
(N₃ : Type v) →
[AddCommGroup N₃] →
[Module A N₃] →
[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 :=
by
have equiv (N₁ : Type v) [AddCommGroup N₁] [Module A N₁] [Module.Finite A N₁] (N₂ : Type v) [AddCommGroup N₂]
[Module A N₂] [Module.Finite A N₂] (f : N₁ ≃ₗ[A] N₂) (h : motive N₁) : motive N₂ :=
exact N₁ N₂ PUnit.{v + 1} f 0 f.injective (Function.surjective_to_subsingleton _)
((f.exact_zero_iff_surjective _).2 f.surjective) h (subsingleton _)
obtain ⟨s, hs1, hs2⟩ := IsNoetherianRing.exists_relSeries_isQuotientEquivQuotientPrime A M
suffices H : ∀ n, (h : n < s.length + 1) → motive (s ⟨n, h⟩)
by
replace H : motive s.last := H s.length s.length.lt_add_one
rw [hs2] at H
exact equiv _ _ Submodule.topEquiv H
intro n h
induction n with
| zero =>
change motive s.head
rw [hs1]
exact subsingleton _
| succ n ih =>
specialize ih (n.lt_add_one.trans h)
obtain ⟨hle, p, ⟨f⟩⟩ := s.step ⟨n, (add_lt_add_iff_right _).1 h⟩
replace ih := equiv _ _ (Submodule.submoduleOfEquivOfLe hle).symm ih
exact
exact _ _ _ _ _ (Submodule.injective_subtype _) (Submodule.mkQ_surjective _) (LinearMap.exact_subtype_mkQ _) ih
(quotient _ p f)
