finite_quotient_smul — Mathlib

English

Let R be a ring, M an R-module, N a submodule of finite index, and I an ideal of finite index. If N has finite index, then I·N has finite index in M, given N is finitely generated.

Русский

Пусть R — кольцо, M — R-модуль, N — подмодуль с конечным индексом, и I — идеал с конечным индексом. Тогда I·N имеет конечный индекс в M, если N конечно порожден.

LaTeX

$$$$\text{Finite}(M/(I\cdot N)).$$$$

Lean4

/-- Let `N` be a finite index f.g. `R`-submodule, and `I` be a finite index ideal.
Then `I • N` also has finite index. -/
theorem finite_quotient_smul [Finite (R ⧸ I)] [Finite (M ⧸ N)] (hN : N.FG) : Finite (M ⧸ I • N) :=
  by
  suffices (I • N).toAddSubgroup.FiniteIndex by exact (I • N).toAddSubgroup.finite_quotient_of_finiteIndex
  suffices Nat.card (N ⧸ (I • N).comap N.subtype) ≠ 0 by
    constructor
    rw [← AddSubgroup.relIndex_mul_index (H := (I • N).toAddSubgroup) (K := N.toAddSubgroup) Submodule.smul_le_right]
    have inst : Finite (M ⧸ N.toAddSubgroup) := ‹_›
    exact mul_ne_zero this AddSubgroup.index_ne_zero_of_finite
  let e : (N ⧸ (I • N).comap N.subtype) ≃ₗ[R] (R ⧸ I) ⊗[R] N :=
    Submodule.quotEquivOfEq _ (I • (⊤ : Submodule R N))
        (Submodule.map_injective_of_injective N.injective_subtype (by simp [Submodule.smul_le_right])) ≪≫ₗ
      (quotTensorEquivQuotSMul N I).symm
  rw [Nat.card_congr e.toEquiv]
  have : Module.Finite R N := Module.Finite.iff_fg.mpr hN
  have : Finite ((R ⧸ I) ⊗[R] N) := Module.finite_of_finite (R ⧸ I)
  exact Nat.card_pos.ne'

Похожие утверждения