BimoduleTensor.lean`

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DerivedBar.BimoduleTensor.relations line 16
Source documentation
Noncommutative balancing relations for an arbitrary (D,D)-bimodule X.
```
def relations : Submodule D (X ⊗[k] V) :=
…
```
abbrev OAI.DerivedBar.BimoduleTensor.tensor line 21
Source documentation
Genuine balanced X ⊗_D V, with its exterior left D-action.
```
abbrev tensor := (X ⊗[k] V) ⧸ relations k D X V
```
Mentions: OAI.DerivedBar.BimoduleTensor.relations
def OAI.DerivedBar.BimoduleTensor.quotient line 23
theorem OAI.DerivedBar.BimoduleTensor.balanced line 26
theorem OAI.DerivedBar.BimoduleTensor.map_relations line 37
def OAI.DerivedBar.BimoduleTensor.map line 47
theorem OAI.DerivedBar.BimoduleTensor.map_quotient line 52
theorem OAI.DerivedBar.BimoduleTensor.map_comp line 56
theorem OAI.DerivedBar.BimoduleTensor.map_zero line 63
theorem OAI.DerivedBar.BimoduleTensor.map_id line 70
theorem OAI.DerivedBar.BimoduleTensor.map_add line 76
def OAI.DerivedBar.BimoduleTensor.rightMul line 89
Source documentation
The bimodule right action, bilinear over the field.
```
def rightMul : X →ₗ[k] D →ₗ[k] X where
…
```
def OAI.DerivedBar.BimoduleTensor.rightAction line 98
Source documentation
Multiplication X ⊗_k D → X respects the arbitrary exterior D-action.
```
def rightAction : X ⊗[k] D →ₗ[D] X :=
…
```
theorem OAI.DerivedBar.BimoduleTensor.rightAction_tmul line 110
def OAI.DerivedBar.BimoduleTensor.collapse line 116
Source documentation
Collapse the first two slots using the right D-action on X.
```
def collapse : X ⊗[k] (D ⊗[k] W) →ₗ[D] X ⊗[k] W :=
…
```
theorem OAI.DerivedBar.BimoduleTensor.collapse_tmul line 132
theorem OAI.DerivedBar.BimoduleTensor.relations_le_ker_collapse line 136
Source documentation
The collapse descends through the actual balancing relations.
```
theorem relations_le_ker_collapse : relations k D X (D ⊗[k] W) ≤ (collapse k D X W).ker := by
…
```
Mentions: OAI.DerivedBar.BimoduleTensor.relations, OAI.DerivedBar.BimoduleTensor.collapse
def OAI.DerivedBar.BimoduleTensor.descend line 148
def OAI.DerivedBar.BimoduleTensor.insert line 151
theorem OAI.DerivedBar.BimoduleTensor.descend_quotient line 155
theorem OAI.DerivedBar.BimoduleTensor.insert_tmul line 159
theorem OAI.DerivedBar.BimoduleTensor.descend_insert line 162
theorem OAI.DerivedBar.BimoduleTensor.insert_descend line 168
def OAI.DerivedBar.BimoduleTensor.freeEquiv line 181
Source documentation
Genuine X ⊗_D (D ⊗_k W) ≅ X ⊗_k W, with no flatness of X.
```
def freeEquiv : tensor k D X (D ⊗[k] W) ≃ₗ[D] X ⊗[k] W :=
…
```
Mentions: OAI.DerivedBar.BimoduleTensor.tensor