modulePi — Mathlib

English

R^n / I^n is isomorphic to (R/I)^n as a module over R/I.

Русский

Кольцо R^n / I^n изоморфно модулю (R/I)^n надR/I.

LaTeX

$$((ι → R) ⧸ pi fun _ ↦ I) ≃ₗ[R ⧸ I] ι → (R ⧸ I)$$

Lean4

/-- `R^n/I^n` is a `R/I`-module. -/
instance modulePi [I.IsTwoSided] : Module (R ⧸ I) ((ι → R) ⧸ pi fun _ ↦ I)
    where
  smul c
    m :=
    Quotient.liftOn₂' c m (fun r m ↦ Submodule.Quotient.mk <| r • m) <|
      by
      intro c₁ m₁ c₂ m₂ hc hm
      apply Ideal.Quotient.eq.2
      rw [Submodule.quotientRel_def] at hc hm
      intro i
      exact I.mul_sub_mul_mem hc (hm i)
  one_smul := by rintro ⟨a⟩; exact congr_arg _ (one_smul _ _)
  mul_smul := by rintro ⟨a⟩ ⟨b⟩ ⟨c⟩; exact congr_arg _ (mul_smul _ _ _)
  smul_add := by rintro ⟨a⟩ ⟨b⟩ ⟨c⟩; exact congr_arg _ (smul_add _ _ _)
  smul_zero := by rintro ⟨a⟩; exact congr_arg _ (smul_zero _)
  add_smul := by rintro ⟨a⟩ ⟨b⟩ ⟨c⟩; exact congr_arg _ (add_smul _ _ _)
  zero_smul := by rintro ⟨a⟩; exact congr_arg _ (zero_smul _ _)

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