ExternalTensor.lean`

31 declarations, 0 contain sorry, 0 declared as axioms

def OAI.ExternalTensor.leftAction line 17
def OAI.ExternalTensor.rightAction line 20
theorem OAI.ExternalTensor.leftAction_tmul line 24
theorem OAI.ExternalTensor.rightAction_tmul line 28
theorem OAI.ExternalTensor.actions_commute line 31
def OAI.ExternalTensor.action line 38
Source documentation
The genuine enveloping algebra representation; the right action is encoded by Bᵐᵒᵖ.
```
def action : (B ⊗[k] Bᵐᵒᵖ) →ₐ[k] Module.End k (M ⊗[k] N) :=
…
```
def OAI.ExternalTensor.bimodule line 42
def OAI.ExternalTensor.rightModule line 45
theorem OAI.ExternalTensor.smul_tmul line 50
theorem OAI.ExternalTensor.right_smul_tmul line 54
def OAI.ExternalTensor.rightSwap line 59
Source documentation
Factor swap, with the external right action on the source.
```
def rightSwap : (M ⊗[k] N) ≃ₗ[Bᵐᵒᵖ] (N ⊗[k] M) where
…
```
theorem OAI.ExternalTensor.projective_right line 68
Source documentation
In fact no dimension restriction on M is needed for right projectivity.
```
theorem projective_right [Module.Projective Bᵐᵒᵖ N] :
    Module.Projective Bᵐᵒᵖ (M ⊗[k] N) :=
…
```
theorem OAI.ExternalTensor.finiteDimensional line 72
def OAI.ExternalTensor.rightBasisEquiv line 79
Source documentation
A k-basis of the left factor gives an actual right-module direct-sum decomposition.
```
def rightBasisEquiv {ι : Type*} [DecidableEq ι] (v : Module.Basis ι k M) :
    (M ⊗[k] N) ≃ₗ[Bᵐᵒᵖ] (ι →₀ N) where
…
```
theorem OAI.ExternalTensor.rightBasisEquiv_tmul line 94
theorem OAI.ExternalTensor.finite_right line 100
theorem OAI.ExternalTensor.right_eq_enveloping line 106
Source documentation
The chosen right action is the restriction of the enveloping action.
```
theorem right_eq_enveloping (c : Bᵐᵒᵖ) (x : M ⊗[k] N) :
    c • x = (1 ⊗ₜ[k] c : B ⊗[k] Bᵐᵒᵖ) • x := by
…
```
theorem OAI.ExternalTensor.left_eq_enveloping line 113
Source documentation
The usual left action on the first tensor factor is the other restriction.
```
theorem left_eq_enveloping (b : B) (x : M ⊗[k] N) :
    b • x = (b ⊗ₜ[k] (1 : Bᵐᵒᵖ)) • x := by
…
```
instance OAI.ExternalTensor.commutingActions line 119
instance OAI.ExternalTensor.rightScalarTower line 125
instance OAI.ExternalTensor.envelopingScalarTower line 131

def OAI.ExternalTensor.map line 143

Source documentation

Tensor of a left-module map and a right-module map is enveloping-linear.

def map (f : M →ₗ[B] M') (g : N →ₗ[Bᵐᵒᵖ] N') :
    (M ⊗[k] N) →ₗ[B ⊗[k] Bᵐᵒᵖ] (M' ⊗[k] N') where
…

theorem OAI.ExternalTensor.map_tmul line 154
theorem OAI.ExternalTensor.map_id line 157
theorem OAI.ExternalTensor.map_comp line 169
theorem OAI.ExternalTensor.map_add_left line 178
theorem OAI.ExternalTensor.map_add_right line 185
theorem OAI.ExternalTensor.map_smul_left line 193
theorem OAI.ExternalTensor.map_smul_right line 200

def OAI.ExternalTensor.rightMap line 208

Source documentation

The same tensor map as a map of right B-modules.

def rightMap (f : M →ₗ[B] M') (g : N →ₗ[Bᵐᵒᵖ] N') :
    (M ⊗[k] N) →ₗ[Bᵐᵒᵖ] (M' ⊗[k] N') where
…

theorem OAI.ExternalTensor.rightMap_tmul line 215