instCStarModuleProd — Mathlib

English

The product of C*-modules carries a natural C*-module structure componentwise, with inner product sum across components.

Русский

Произведение C*-модулей наделяется естественной структурой C*-модуля по компонентам, скалярное произведение суммируется по компонентам.

LaTeX

$$$\\text{WithCStarModuleProd}: CStarModule A (E \\times F) \\\\text{ defined by } \\langle (x_1,x_2),(y_1,y_2)\\rangle = \\langle x_1,y_1\\rangle + \\langle x_2,y_2\\rangle$$$

Lean4

noncomputable instance : CStarModule A C⋆ᵐᵒᵈ(A, E × F)
    where
  inner x y := ⟪x.1, y.1⟫_A + ⟪x.2, y.2⟫_A
  inner_add_right {x y z} := by simpa using add_add_add_comm ..
  inner_self_nonneg := add_nonneg CStarModule.inner_self_nonneg CStarModule.inner_self_nonneg
  inner_self
    {x} := by
    refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
    apply equiv A (E × F) |>.injective
    ext
    · refine inner_self.mp <| le_antisymm ?_ (inner_self_nonneg (A := A))
      exact le_add_of_nonneg_right CStarModule.inner_self_nonneg |>.trans_eq h
    · refine inner_self.mp <| le_antisymm ?_ (inner_self_nonneg (A := A))
      exact le_add_of_nonneg_left CStarModule.inner_self_nonneg |>.trans_eq h
  inner_op_smul_right := by simp [mul_add]
  inner_smul_right_complex := by simp [smul_add]
  star_inner x y := by simp
  norm_eq_sqrt_norm_inner_self {x} := by with_reducible_and_instances rfl

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