Balancing a sesquilinear form against a conjugate-semilinear map

A sesquilinear form H on a module and a star-semilinear map K of that module are unrelated data. This file makes them compatible: the balanced form

balance H K x y = H x y + star (H (K x) (K y))

is again sesquilinear -- each argument of the second summand picks up a conjugation from K, and the outer conjugation restores the shape -- and it satisfies

balance H K (K x) (K y) = star (balance H K x y)

as soon as K ∘ K is a scalar of modulus one, which an arbitrary H need not. That is the only property balancing adds: being Hermitian and being nonnegative pass from H to balance H K unchanged, and for nonnegative H so does being definite off the origin, since balance H K x x is nonzero wherever H x x is.

The construction and its compatibility are plain star-ring algebra, so they are stated over a commutative star semiring. Nonnegativity and definiteness off the origin need an order on the scalars compatible with the star, and are stated over a commutative star-ordered semiring, such as ℂ with its partial order ComplexOrder.

Main definitions

• LinearMap.balance: the balanced form x, y ↦ H x y + star (H (K x) (K y)).

Main results

• LinearMap.balance_apply: the defining formula of the balanced form.
• LinearMap.balance_map_map: the balanced form is compatible with the map it was balanced against, once that map squares to a scalar of modulus one.
• LinearMap.isSymm_balance and LinearMap.isNonneg_balance: balancing preserves Hermitian symmetry and nonnegativity.
• LinearMap.balance_apply_self_ne_zero: for nonnegative H, the balanced form is nonzero on the diagonal wherever H is, so balancing preserves definiteness off the origin.

def LinearMap.balance {R : Type u_1} {V : Type u_2} [CommSemiring R] [StarRing R] [AddCommMonoid V] [Module R V] (H : V →ₗ⋆[R] V →ₗ[R] R) (K : V →ₗ⋆[R] V) : V →ₗ⋆[R] V →ₗ[R] R

The balanced form of a sesquilinear form H against a star-semilinear map K: x, y ↦ H x y + star (H (K x) (K y)). Each argument of the second summand picks up a conjugation from K, and the outer conjugation restores the shape of a sesquilinear form, conjugate-linear in the first argument and linear in the second. Adding it to H is what forces the compatibility balance H K (K x) (K y) = star (balance H K x y) whenever K ∘ K is a scalar of modulus one.

@[simp]

theorem LinearMap.balance_apply {R : Type u_1} {V : Type u_2} [CommSemiring R] [StarRing R] [AddCommMonoid V] [Module R V] (H : V →ₗ⋆[R] V →ₗ[R] R) (K : V →ₗ⋆[R] V) (x y : V) : ((H.balance K) x) y = (H x) y + (starRingEnd R) ((H (K x)) (K y))

The defining formula of the balanced form.

theorem LinearMap.balance_map_map {R : Type u_1} {V : Type u_2} [CommSemiring R] [StarRing R] [AddCommMonoid V] [Module R V] {H : V →ₗ⋆[R] V →ₗ[R] R} {K : V →ₗ⋆[R] V} {ε : R} (hε : star ε * ε = 1) (hK : ∀ (x : V), K (K x) = ε • x) (x y : V) : ((H.balance K) (K x)) (K y) = (starRingEnd R) (((H.balance K) x) y)

The balanced form is compatible with the map it was balanced against: replacing both arguments by their K-images conjugates the value, as soon as K ∘ K is a scalar ε of modulus one. The conjugation of the first argument of H turns the two ε-factors into star ε * ε, so no more than star ε * ε = 1 is used; the real signs ε = 1 and ε = -1 (an involution, or a quaternionic structure) are the main examples. This is the only property of balance that H alone does not already have, and the whole point of the construction.

theorem LinearMap.isSymm_balance {R : Type u_1} {V : Type u_2} [CommSemiring R] [StarRing R] [AddCommMonoid V] [Module R V] {H : V →ₗ⋆[R] V →ₗ[R] R} (hH : H.IsSymm) (K : V →ₗ⋆[R] V) : (H.balance K).IsSymm

The balanced form is Hermitian if H is.

theorem LinearMap.isNonneg_balance {R : Type u_1} {V : Type u_2} [CommSemiring R] [StarRing R] [AddCommMonoid V] [Module R V] [PartialOrder R] [StarOrderedRing R] {H : V →ₗ⋆[R] V →ₗ[R] R} (hH : H.IsNonneg) (K : V →ₗ⋆[R] V) : (H.balance K).IsNonneg

The balanced form is nonnegative if H is: both summands are, the second because conjugation fixes a nonnegative scalar.

theorem LinearMap.balance_apply_self_ne_zero {R : Type u_1} {V : Type u_2} [CommSemiring R] [StarRing R] [AddCommMonoid V] [Module R V] [PartialOrder R] [StarOrderedRing R] {H : V →ₗ⋆[R] V →ₗ[R] R} (hH : H.IsNonneg) (K : V →ₗ⋆[R] V) {x : V} (hx : (H x) x ≠ 0) : ((H.balance K) x) x ≠ 0

For nonnegative H, the balanced form is nonzero on the diagonal wherever H is: both summands are nonnegative and the first is nonzero. In particular, balancing a nonnegative form that is definite off the origin gives a form that is again definite off the origin.