class LinearMap.IsCompatibleDual {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) : Prop

A linear topology on E is compatible with the bilinear form B if the every continuous linear functional on E has the form B.flip f for exactly one f : F.

• range_eq_range : B.flip.range = (ContinuousLinearMap.coeLM 𝕜).range
• injective : Function.Injective ⇑B.flip

@[simp]

theorem LinearMap.ContinuousLinearMap.coeLM_injective {R : Type u_4} {M : Type u_5} {N : Type u_6} (S : Type u_7) [Semiring R] [Semiring S] [TopologicalSpace M] [AddCommMonoid M] [Module R M] [TopologicalSpace N] [AddCommMonoid N] [Module R N] [Module S N] [SMulCommClass R S N] [ContinuousConstSMul S N] [ContinuousAdd N] : Function.Injective ⇑(ContinuousLinearMap.coeLM S)

theorem LinearEquiv.IsCompatibleDual {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (e : F ≃ₗ[𝕜] StrongDual 𝕜 E) (hB : B.flip = ContinuousLinearMap.coeLM 𝕜 ∘ₗ ↑e) : B.IsCompatibleDual

theorem LinearMap.IsCompatibleDual.continuous {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) [h : B.IsCompatibleDual] (x : F) : Continuous ⇑(B.flip x)

noncomputable def LinearMap.IsCompatibleDual.equiv {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) [h : B.IsCompatibleDual] : F ≃ₗ[𝕜] StrongDual 𝕜 E

Linear equivalence of F with StrongDual 𝕜 E obtained from B.IsCompatibleDual.

Equations

• LinearMap.IsCompatibleDual.equiv B = LinearEquiv.ofBijective { toFun := fun (x : F) => { toLinearMap := B.flip x, cont := ⋯ }, map_add' := ⋯, map_smul' := ⋯ } ⋯

@[simp]

theorem LinearMap.IsCompatibleDual.equiv_apply_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) [h : B.IsCompatibleDual] (y : F) (x : E) : ((equiv B) y) x = (B x) y

theorem LinearMap.IsCompatibleDual.equiv_apply' {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) [h : B.IsCompatibleDual] (y : F) : (equiv B) y = { toLinearMap := B.flip y, cont := ⋯ }

noncomputable def LinearMap.IsCompatibleDual.weakSpaceCLE {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) [h : B.IsCompatibleDual] : WeakBilin B ≃L[𝕜] WeakSpace 𝕜 E

Continuous linear equivalence of WeakBilin B with WeakSpace 𝕜 E obtained from B.IsCompatibleDual.

Equations

• LinearMap.IsCompatibleDual.weakSpaceCLE B = (WeakBilin.congr B (LinearEquiv.refl 𝕜 E) (LinearMap.IsCompatibleDual.equiv B) (topDualPairing 𝕜 E).flip ⋯).trans WeakSpace.weakBilinCLE.symm

noncomputable def LinearMap.IsCompatibleDual.weakDualCLE {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) [h : B.IsCompatibleDual] : WeakBilin B.flip ≃L[𝕜] WeakDual 𝕜 E

Continuous linear equivalence of WeakBilin B.flip with WeakDual 𝕜 E obtained from B.IsCompatibleDual.

Equations

• LinearMap.IsCompatibleDual.weakDualCLE B = (WeakBilin.congr B.flip (LinearMap.IsCompatibleDual.equiv B) (LinearEquiv.refl 𝕜 E) (topDualPairing 𝕜 E) ⋯).trans WeakDual.weakBilinCLE.symm