Theorems · Definition · linear algebra

PiTensorProduct.liftAddHom

{ι : Type u_1} →
  {R : Type u_4} →
    [inst : CommSemiring R] →
      {s : ι → Type u_7} →
        [inst_1 : (i : ι) → AddCommMonoid (s i)] →
          [inst_2 : (i : ι) → Module R (s i)] →
            {F : Type u_10} →
              [inst_3 : AddCommMonoid F] →
                (φ : R × ((i : ι) → s i) → F) →
                  (∀ (r : R) (f : (i : ι) → s i) (i : ι), f i = 0 → φ (r, f) = 0) →
                    (∀ (f : (i : ι) → s i), φ (0, f) = 0) →
                      (∀ [inst : DecidableEq ι] (r : R) (f : (i : ι) → s i) (i : ι) (m₁ m₂ : s i),
                          φ (r, Function.update f i m₁) + φ (r, Function.update f i m₂) =
                            φ (r, Function.update f i (m₁ + m₂))) →
                        (∀ (r r' : R) (f : (i : ι) → s i), φ (r, f) + φ (r', f) = φ (r + r', f)) →
                          (∀ [inst_4 : DecidableEq ι] (r : R) (f : (i : ι) → s i) (i : ι) (r' : R),
                              φ (r, Function.update f i (r' • f i)) = φ (r' * r, f)) →
                            (PiTensorProduct R fun i => s i) →+ F

Construct an AddMonoidHom from (⨂[R] i, s i) to some space F from a function φ : (R × Π i, s i) → F with the appropriate properties.

Defined in

Mathlib.LinearAlgebra.PiTensorProduct.Basic

Cited by

1 results in Mathlib

Foundations

Depth 45 from the axioms · uses propext, Quot.sound

Assumes

CommSemiringAddCommMonoidModuleAddCommMonoid