DualEmbedding.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Transposed embeddings

A surjective intertwiner yields an injective intertwiner in the opposite direction when both modules carry compatible perfect pairings. This is an algebraic alternative to splitting a representation by complete reducibility.

def OAI.Problem346.DualEmbedding.flipPairing line 24
Source documentation
Reverse a perfect pairing when the first module is reflexive. This turns the usual chart E' ≃ Dual E into the orientation needed by transpose.
```
def flipPairing [Module.IsReflexive R E] (e : E' ≃ₗ[R] Module.Dual R E) :
    E ≃ₗ[R] Module.Dual R E' :=
…
```
theorem OAI.Problem346.DualEmbedding.flipPairing_apply line 29

def OAI.Problem346.DualEmbedding.transpose line 34

Source documentation

Transport the dual of a linear map along two perfect pairings.

def transpose (e : E ≃ₗ[R] Module.Dual R E')
    (f : F ≃ₗ[R] Module.Dual R F') (μ : E' →ₗ[R] F') : F →ₗ[R] E :=
…

theorem OAI.Problem346.DualEmbedding.pairing_transpose line 39

theorem OAI.Problem346.DualEmbedding.transpose_injective line 45

Source documentation

Surjectivity of a map implies injectivity of its transported transpose.

theorem transpose_injective (e : E ≃ₗ[R] Module.Dual R E')
    (f : F ≃ₗ[R] Module.Dual R F') (μ : E' →ₗ[R] F')
    (hμ : Function.Surjective μ) : Function.Injective (transpose e f μ) := by
…

Mentions: OAI.Problem346.DualEmbedding.transpose

theorem OAI.Problem346.DualEmbedding.transpose_intertwines line 53

Source documentation

Transposition reverses an intertwining identity, with the two adjoint identities expressed directly as evaluations of the perfect pairings.

theorem transpose_intertwines
    (e : E ≃ₗ[R] Module.Dual R E') (f : F ≃ₗ[R] Module.Dual R F')
    (μ : E' →ₗ[R] F') (A : E →ₗ[R] E) (A' : E' →ₗ[R] E')
    (B : F →ₗ[R] F) (B' : F' →ₗ[R] F')
    (he : ∀ x z, e (A x) z = e x (A' z))
    (hf : ∀ y w, f (B y) w = f y (B' w))
    (hμ : μ.comp A' = B'.comp μ) :
    A.comp (transpose e f μ) = (transpose e f μ).comp B := by
…

Mentions: OAI.Problem346.DualEmbedding.transpose

theorem OAI.Problem346.DualEmbedding.exists_intertwining_injection_of_surjective line 71

Source documentation

A family of compatible adjoint actions transports a surjective equivariant map into an injective equivariant map in the reverse direction. No group structure or finite-dimensionality is needed by this argument.

theorem exists_intertwining_injection_of_surjective {G : Type*}
    (e : E ≃ₗ[R] Module.Dual R E') (f : F ≃ₗ[R] Module.Dual R F')
    (A : G → E →ₗ[R] E) (B : G → F →ₗ[R] F)
    (A' : G → E' →ₗ[R] E') (B' : G → F' →ₗ[R] F')
    (he : ∀ g x z, e (A g x) z = e x (A' g z))
    (hf : ∀ g y w, f (B g y) w = f y (B' g w))
    (μ : E' →ₗ[R] F') (hμ : Function.Surjective μ)
    (hcomm : ∀ g, μ.comp (A' g) = (B' g).comp μ) :
    ∃ ι : F →ₗ[R] E, Function.Injective ι ∧
      ∀ g, (A g).comp ι = ι.comp (B g) := by
…