Theorems · Theorem · commutative algebra

LocalizedModule.lift_unique

∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M'' : Type u_4} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M''] [inst_3 : Module R M] [inst_4 : Module R M''] (g : M →ₗ[R] M'')
  (h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)) (l : LocalizedModule S M →ₗ[R] M''),
  l ∘ₗ LocalizedModule.mkLinearMap S M = g → LocalizedModule.lift S g h = l

If g is a linear map M → M'' such that all scalar multiplication by s : S is invertible and l is another linear map LocalizedModule S M ⟶ M'' such that l ∘ mkLinearMap = g then l = lift g

Defined in

Mathlib.Algebra.Module.LocalizedModule.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidAddCommMonoidModuleModule