Symmetric continuous bilinear maps

Symmetric continuous bilinear maps form a closed linear subspace. Simultaneous change of variables preserves this subspace. These restricted coordinate changes provide the model fibres and gluing maps for bundles of symmetric bilinear tensors.

ContinuousLinearEquiv.symmetricBilinearMapsCongr restricts Mathlib's iterated arrowCongr using ContinuousLinearEquiv.ofSubmodules. It needs only the topology of the original spaces, so it applies to bundle fibres without choosing fibre norms. The identity, inverse and composition laws give consistent coordinates on overlaps. In finite dimensions these equivalences also identify the dimensions of the symmetric fibres.

ContinuousLinearMap.symmetricBilinearMapsComp pulls symmetric bilinear maps back along a continuous linear map, in both arguments simultaneously; the symmetric coordinates of a change of variables are the pullback along its inverse. On normed spaces the symmetric subspace carries the restricted operator norm, and the pullback depends continuously on the map it pulls back along.

On a normed model fibre, ContinuousLinearMap.symmetrizeBilinear is the continuous linear retraction b ↦ (b + bᵀ) / 2 when two is nonzero. It commutes with changes of variables, so its image is independent of the chosen fibre coordinates. Taking real-valued maps on tangent spaces gives the fibre model for symmetric covariant two-tensors, the ambient tensors for metrics.

def TauCeti.symmetricBilinearMaps (𝕜 : Type u_1) [NormedField 𝕜] (E : Type u_2) [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] (G : Type u_3) [AddCommGroup G] [Module 𝕜 G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜 G] : Submodule 𝕜 (E →L[𝕜] E →L[𝕜] G)

The linear subspace of symmetric continuous bilinear maps.

@[simp]

theorem TauCeti.mem_symmetricBilinearMaps (𝕜 : Type u_1) [NormedField 𝕜] (E : Type u_2) [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] (G : Type u_3) [AddCommGroup G] [Module 𝕜 G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜 G] (b : E →L[𝕜] E →L[𝕜] G) : b ∈ symmetricBilinearMaps 𝕜 E G ↔ ∀ (v w : E), (b v) w = (b w) v

theorem TauCeti.isClosed_symmetricBilinearMaps (𝕜 : Type u_1) [NormedField 𝕜] (E : Type u_2) [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] (G : Type u_3) [AddCommGroup G] [Module 𝕜 G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜 G] [ContinuousSMul 𝕜 E] [T2Space G] : IsClosed ↑(symmetricBilinearMaps 𝕜 E G)

Symmetry is closed in the topology of continuous bilinear maps.

The generic submodule instances would have to solve nested instance problems on the iterated space of continuous linear maps, which exceed the default depth of pending instance problems. These shortcuts make the symmetric subspace usable as a model fibre.

@[instance_reducible]

instance TauCeti.instAddCommGroupSubtypeContinuousLinearMapIdMemSubmoduleSymmetricBilinearMaps (𝕜 : Type u_1) [NormedField 𝕜] (E : Type u_2) [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] (G : Type u_3) [AddCommGroup G] [Module 𝕜 G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜 G] : AddCommGroup ↥(symmetricBilinearMaps 𝕜 E G)

@[instance_reducible]

instance TauCeti.instModuleSubtypeContinuousLinearMapIdMemSubmoduleSymmetricBilinearMaps (𝕜 : Type u_1) [NormedField 𝕜] (E : Type u_2) [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] (G : Type u_3) [AddCommGroup G] [Module 𝕜 G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜 G] : Module 𝕜 ↥(symmetricBilinearMaps 𝕜 E G)

def ContinuousLinearMap.symmetricBilinearMapsComp {𝕜 : Type u_1} [NormedField 𝕜] {E : Type u_2} {E' : Type u_3} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup E'] [Module 𝕜 E'] [TopologicalSpace E'] {G : Type u_5} [AddCommGroup G] [Module 𝕜 G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜 G] (A : E' →L[𝕜] E) : ↥(TauCeti.symmetricBilinearMaps 𝕜 E G) →L[𝕜] ↥(TauCeti.symmetricBilinearMaps 𝕜 E' G)

Pullback of symmetric bilinear maps along a continuous linear map, applied to both arguments simultaneously.

@[simp]

theorem ContinuousLinearMap.symmetricBilinearMapsComp_apply {𝕜 : Type u_1} [NormedField 𝕜] {E : Type u_2} {E' : Type u_3} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup E'] [Module 𝕜 E'] [TopologicalSpace E'] {G : Type u_5} [AddCommGroup G] [Module 𝕜 G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜 G] (A : E' →L[𝕜] E) (b : ↥(TauCeti.symmetricBilinearMaps 𝕜 E G)) (v w : E') : (↑(A.symmetricBilinearMapsComp b) v) w = (↑b (A v)) (A w)

@[simp]

theorem ContinuousLinearMap.symmetricBilinearMapsComp_id {𝕜 : Type u_1} [NormedField 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {G : Type u_5} [AddCommGroup G] [Module 𝕜 G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜 G] : (ContinuousLinearMap.id 𝕜 E).symmetricBilinearMapsComp = ContinuousLinearMap.id 𝕜 ↥(TauCeti.symmetricBilinearMaps 𝕜 E G)

theorem ContinuousLinearMap.symmetricBilinearMapsComp_comp {𝕜 : Type u_1} [NormedField 𝕜] {E : Type u_2} {E' : Type u_3} {E'' : Type u_4} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup E'] [Module 𝕜 E'] [TopologicalSpace E'] [AddCommGroup E''] [Module 𝕜 E''] [TopologicalSpace E''] {G : Type u_5} [AddCommGroup G] [Module 𝕜 G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜 G] (A : E' →L[𝕜] E) (B : E'' →L[𝕜] E') : (A ∘SL B).symmetricBilinearMapsComp = B.symmetricBilinearMapsComp ∘SL A.symmetricBilinearMapsComp

def ContinuousLinearEquiv.symmetricBilinearMapsCongr {𝕜 : Type u_1} [NormedField 𝕜] {E : Type u_2} {F : Type u_3} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] {G : Type u_4} [AddCommGroup G] [Module 𝕜 G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜 G] (e : E ≃L[𝕜] F) : ↥(TauCeti.symmetricBilinearMaps 𝕜 E G) ≃L[𝕜] ↥(TauCeti.symmetricBilinearMaps 𝕜 F G)

A change of variables identifies the spaces of symmetric bilinear maps.

@[simp]

theorem ContinuousLinearEquiv.symmetricBilinearMapsCongr_apply {𝕜 : Type u_1} [NormedField 𝕜] {E : Type u_2} {F : Type u_3} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] {G : Type u_4} [AddCommGroup G] [Module 𝕜 G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜 G] (e : E ≃L[𝕜] F) (b : ↥(TauCeti.symmetricBilinearMaps 𝕜 E G)) (v w : F) : (↑(e.symmetricBilinearMapsCongr b) v) w = (↑b (e.symm v)) (e.symm w)

@[simp]

theorem ContinuousLinearEquiv.symmetricBilinearMapsCongr_refl {𝕜 : Type u_1} [NormedField 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {G : Type u_4} [AddCommGroup G] [Module 𝕜 G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜 G] : (ContinuousLinearEquiv.refl 𝕜 E).symmetricBilinearMapsCongr = ContinuousLinearEquiv.refl 𝕜 ↥(TauCeti.symmetricBilinearMaps 𝕜 E G)

The identity change of variables gives the identity symmetric coordinates.

@[simp]

theorem ContinuousLinearEquiv.symmetricBilinearMapsCongr_symm {𝕜 : Type u_1} [NormedField 𝕜] {E : Type u_2} {F : Type u_3} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] {G : Type u_4} [AddCommGroup G] [Module 𝕜 G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜 G] (e : E ≃L[𝕜] F) : e.symmetricBilinearMapsCongr.symm = e.symm.symmetricBilinearMapsCongr

Reversing a change of variables reverses the induced symmetric coordinates.

@[simp]

theorem ContinuousLinearEquiv.symmetricBilinearMapsCongr_trans {𝕜 : Type u_1} [NormedField 𝕜] {E : Type u_2} {F : Type u_3} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] {G : Type u_4} [AddCommGroup G] [Module 𝕜 G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜 G] {W : Type u_5} [AddCommGroup W] [Module 𝕜 W] [TopologicalSpace W] (e : E ≃L[𝕜] F) (f : F ≃L[𝕜] W) : (e.trans f).symmetricBilinearMapsCongr = e.symmetricBilinearMapsCongr.trans f.symmetricBilinearMapsCongr

Symmetric coordinates respect composition, giving the overlap cocycle law.

theorem ContinuousLinearEquiv.coe_symmetricBilinearMapsCongr {𝕜 : Type u_1} [NormedField 𝕜] {E : Type u_2} {F : Type u_3} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] {G : Type u_4} [AddCommGroup G] [Module 𝕜 G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜 G] (e : E ≃L[𝕜] F) : ↑e.symmetricBilinearMapsCongr = (↑e.symm).symmetricBilinearMapsComp

The symmetric coordinates of a change of variables are pullback along its inverse.

@[instance_reducible]

noncomputable instance TauCeti.instNormedAddCommGroupSubtypeContinuousLinearMapIdMemSubmoduleSymmetricBilinearMaps {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace 𝕜 V] {G : Type u_3} [NormedAddCommGroup G] [NormedSpace 𝕜 G] : NormedAddCommGroup ↥(symmetricBilinearMaps 𝕜 V G)

The restricted operator norm on symmetric bilinear maps.

@[instance_reducible]

noncomputable instance TauCeti.instNormedSpaceSubtypeContinuousLinearMapIdMemSubmoduleSymmetricBilinearMaps {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace 𝕜 V] {G : Type u_3} [NormedAddCommGroup G] [NormedSpace 𝕜 G] : NormedSpace 𝕜 ↥(symmetricBilinearMaps 𝕜 V G)

noncomputable def ContinuousLinearMap.symmetrizeBilinear {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {G : Type u_2} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {V : Type u_3} [NormedAddCommGroup V] [NormedSpace 𝕜 V] : (V →L[𝕜] V →L[𝕜] G) →L[𝕜] ↥(TauCeti.symmetricBilinearMaps 𝕜 V G)

Averaging a bilinear map with its transpose, with codomain the symmetric subspace.

@[simp]

theorem ContinuousLinearMap.symmetrizeBilinear_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {G : Type u_2} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {V : Type u_3} [NormedAddCommGroup V] [NormedSpace 𝕜 V] (b : V →L[𝕜] V →L[𝕜] G) (v w : V) : (↑(symmetrizeBilinear b) v) w = 2⁻¹ • ((b v) w + (b w) v)

@[simp]

theorem ContinuousLinearMap.symmetrizeBilinear_coe {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {G : Type u_2} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {V : Type u_3} [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NeZero 2] (b : ↥(TauCeti.symmetricBilinearMaps 𝕜 V G)) : symmetrizeBilinear ↑b = b

Symmetrization is the identity on symmetric bilinear maps.

theorem ContinuousLinearMap.symmetrizeBilinear_surjective {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {G : Type u_2} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {V : Type u_3} [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NeZero 2] : Function.Surjective ⇑symmetrizeBilinear

Every symmetric bilinear map is the symmetrization of a continuous bilinear map.

theorem ContinuousLinearMap.symmetrizeBilinear_bilinearComp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {G : Type u_2} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {V : Type u_3} [NormedAddCommGroup V] [NormedSpace 𝕜 V] {W : Type u_4} [NormedAddCommGroup W] [NormedSpace 𝕜 W] (b : V →L[𝕜] V →L[𝕜] G) (A : W →L[𝕜] V) : ↑(symmetrizeBilinear (b.bilinearComp A A)) = (↑(symmetrizeBilinear b)).bilinearComp A A

Symmetrization commutes with simultaneous pullback of its two arguments.

theorem ContinuousOn.symmetricBilinearMapsComp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} {F' : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {X : Type u_5} [TopologicalSpace X] {P : X → F' →L[𝕜] F} {s : Set X} (hP : ContinuousOn P s) : ContinuousOn (fun (x : X) => (P x).symmetricBilinearMapsComp) s

Symmetric pullback depends continuously on the map it pulls back along.