Theorems · Definition · functional analysis

Unitization.splitMul

(𝕜 : Type u_1) →
  (A : Type u_2) →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NonUnitalNormedRing A] →
        [inst_2 : NormedSpace 𝕜 A] →
          [inst_3 : IsScalarTower 𝕜 A A] → [inst_4 : SMulCommClass 𝕜 A A] → Unitization 𝕜 A →ₐ[𝕜] 𝕜 × (A →L[𝕜] A)

Given (k, a) : Unitization 𝕜 A, the second coordinate of Unitization.splitMul (k, a) is the natural representation of Unitization 𝕜 A on A given by multiplication on the left in A →L[𝕜] A; note that this is not just NonUnitalAlgHom.Lmul for a few reasons: (a) that would either be A acting on A, or (b) Unitization 𝕜 A acting on Unitization 𝕜 A, and (c) that's a NonUnitalAlgHom but here we need an AlgHom. In addition, the first coordinate of Unitization.splitMul (k, a) should just be k. See Unitization.splitMul_apply also.

Defined in

Mathlib.Analysis.Normed.Algebra.Unitization

Cited by

6 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNonUnitalNormedRingNormedSpaceIsScalarTowerSMulCommClass