Continuous perfect pairings

This file defines continuous perfect pairings.

For a topological ring R and two topological modules M and N, a continuous perfect pairing is a continuous bilinear map M × N → R that is bijective in both arguments.

We require continuity in the forward direction only so that we can put several different topologies on the continuous dual (e.g., strong, weak, weak-*). For example, if M is weakly reflexive then there is a continuous perfect pairing between M and WeakDual R M, even though the map WeakDual R M ≃ₗ[R] (M →L[R] R) (where M →L[R] R is equipped with its strong topology) is not in general a homeomorphism.

TODO

Adapt PerfectPairing to this Prop-valued typeclass paradigm

class LinearMap.IsContPerfPair {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [TopologicalSpace R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [AddCommGroup N] [Module R N] [TopologicalSpace N] (p : M →ₗ[R] N →ₗ[R] R) : Prop

For a topological ring R and two topological modules M and N, a continuous perfect pairing is a continuous bilinear map M × N → R that is bijective in both arguments.

We require continuity in the forward direction only so that we can put several different topologies on the continuous dual: strong, weak, weak-* topology...

• continuous_uncurry : Continuous fun (x : M × N) => match x with | (x, y) => (p x) y
• bijective_left : Function.Bijective fun (x : M) => { toLinearMap := p x, cont := ⋯ }
• bijective_right : Function.Bijective fun (y : N) => { toLinearMap := p.flip y, cont := ⋯ }

theorem LinearMap.IsContPerfPair.ext_iff {R : Type u_1} {M : Type u_2} {N : Type u_3} {inst✝ : CommRing R} {inst✝¹ : TopologicalSpace R} {inst✝² : AddCommGroup M} {inst✝³ : Module R M} {inst✝⁴ : TopologicalSpace M} {inst✝⁵ : AddCommGroup N} {inst✝⁶ : Module R N} {inst✝⁷ : TopologicalSpace N} {p : M →ₗ[R] N →ₗ[R] R} {x y : p.IsContPerfPair} : x = y ↔ True

theorem LinearMap.IsContPerfPair.ext {R : Type u_1} {M : Type u_2} {N : Type u_3} {inst✝ : CommRing R} {inst✝¹ : TopologicalSpace R} {inst✝² : AddCommGroup M} {inst✝³ : Module R M} {inst✝⁴ : TopologicalSpace M} {inst✝⁵ : AddCommGroup N} {inst✝⁶ : Module R N} {inst✝⁷ : TopologicalSpace N} {p : M →ₗ[R] N →ₗ[R] R} {x y : p.IsContPerfPair} : x = y

theorem LinearMap.continuous_uncurry_of_isContPerfPair {R : Type u_1} {M : Type u_2} {N : Type u_3} {inst✝ : CommRing R} {inst✝¹ : TopologicalSpace R} {inst✝² : AddCommGroup M} {inst✝³ : Module R M} {inst✝⁴ : TopologicalSpace M} {inst✝⁵ : AddCommGroup N} {inst✝⁶ : Module R N} {inst✝⁷ : TopologicalSpace N} (p : M →ₗ[R] N →ₗ[R] R) [self : p.IsContPerfPair] : Continuous fun (x : M × N) => match x with | (x, y) => (p x) y

Alias of LinearMap.IsContPerfPair.continuous_uncurry.

instance LinearMap.flip.instIsContPerfPair {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [TopologicalSpace R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [AddCommGroup N] [Module R N] [TopologicalSpace N] (p : M →ₗ[R] N →ₗ[R] R) [p.IsContPerfPair] : p.flip.IsContPerfPair

Given a perfect pairing between Mand N, we may interchange the roles of M and N.

theorem LinearMap.continuous_of_isContPerfPair {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [TopologicalSpace R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [AddCommGroup N] [Module R N] [TopologicalSpace N] (p : M →ₗ[R] N →ₗ[R] R) {x : M} [p.IsContPerfPair] : Continuous ⇑(p x)

noncomputable def LinearMap.toContPerfPair {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [TopologicalSpace R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [AddCommGroup N] [Module R N] [TopologicalSpace N] (p : M →ₗ[R] N →ₗ[R] R) [p.IsContPerfPair] [IsTopologicalRing R] : M ≃ₗ[R] N →L[R] R

Turn a continuous perfect pairing between M and N into a map from M to continuous linear maps N → R.

Equations

• p.toContPerfPair = LinearEquiv.ofBijective { toFun := fun (x : M) => { toLinearMap := p x, cont := ⋯ }, map_add' := ⋯, map_smul' := ⋯ } ⋯

@[simp]

theorem LinearMap.toLinearMap_toContPerfPair {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [TopologicalSpace R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [AddCommGroup N] [Module R N] [TopologicalSpace N] (p : M →ₗ[R] N →ₗ[R] R) [p.IsContPerfPair] [IsTopologicalRing R] (x : M) : ↑(p.toContPerfPair x) = p x

@[simp]

theorem LinearMap.toContPerfPair_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [TopologicalSpace R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [AddCommGroup N] [Module R N] [TopologicalSpace N] (p : M →ₗ[R] N →ₗ[R] R) [p.IsContPerfPair] [IsTopologicalRing R] (x : M) (y : N) : (p.toContPerfPair x) y = (p x) y