Theorems · Theorem · linear algebra

Submodule.piQuotientLift_mk

∀ {ι : Type u_1} {R : Type u_2} [inst : CommRing R] {Ms : ι → Type u_3} [inst_1 : (i : ι) → AddCommGroup (Ms i)]
  [inst_2 : (i : ι) → Module R (Ms i)] {N : Type u_4} [inst_3 : AddCommGroup N] [inst_4 : Module R N]
  [inst_5 : Fintype ι] [inst_6 : DecidableEq ι] (p : (i : ι) → Submodule R (Ms i)) (q : Submodule R N)
  (f : (i : ι) → Ms i →ₗ[R] N) (hf : ∀ (i : ι), p i ≤ Submodule.comap (f i) q) (x : (i : ι) → Ms i),
  ((Submodule.piQuotientLift p q f hf) fun i => Submodule.Quotient.mk (x i)) =
    Submodule.Quotient.mk (((LinearMap.lsum R Ms R) f) x)

Defined in

Mathlib.LinearAlgebra.Quotient.Pi

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModuleAddCommGroupModuleFintypeDecidableEq