TensorProjection.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

def OAI.LittleFinitistic.TensorProjection.rightMap line 15
Source documentation
Tensor a k-linear map with the identity while retaining the actual right B-action.
```
def rightMap (f : M →ₗ[k] M') : (M ⊗[k] N) →ₗ[Bᵐᵒᵖ] (M' ⊗[k] N) where
…
```
theorem OAI.LittleFinitistic.TensorProjection.rightMap_tmul line 22
def OAI.LittleFinitistic.TensorProjection.rightCongr line 26
Source documentation
Transport a first-factor vector-space equivalence as an actual right-module equivalence.
```
def rightCongr (e : M ≃ₗ[k] M') : (M ⊗[k] N) ≃ₗ[Bᵐᵒᵖ] (M' ⊗[k] N) where
…
```
def OAI.LittleFinitistic.TensorProjection.fixed line 41
Source documentation
The actual fixed submodule for a projector on the first tensor factor.
```
def fixed : Submodule Bᵐᵒᵖ (M ⊗[k] N) := (rightMap (B := B) p - LinearMap.id).ker
```
Mentions: OAI.LittleFinitistic.TensorProjection.rightMap
theorem OAI.LittleFinitistic.TensorProjection.mem_fixed line 43
theorem OAI.LittleFinitistic.TensorProjection.range_fixed line 46
def OAI.LittleFinitistic.TensorProjection.imageTensorEquiv line 52
Source documentation
The eigenspace e(M tensor N) is exactly (eM) tensor N as a right module.
```
def imageTensorEquiv (hp : p.comp p = p) : (p.range ⊗[k] N) ≃ₗ[Bᵐᵒᵖ] fixed (B := B) (N := N) p where
…
```
Mentions: OAI.LittleFinitistic.TensorProjection.fixed