Balanced.lean`

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DerivedBar.Balanced.relations line 16
Source documentation
The balancing relations for the right A-action d·a = d*f(a).
```
def relations : Submodule D (D ⊗[k] V) :=
…
```
abbrev OAI.DerivedBar.Balanced.tensor line 21
Source documentation
Noncommutative balanced tensor D ⊗_A V, presented using tensors over the field.
```
abbrev tensor := (D ⊗[k] V) ⧸ relations f V
```
Mentions: OAI.DerivedBar.Balanced.relations
def OAI.DerivedBar.Balanced.quotient line 24
Source documentation
Its canonical D-linear quotient map.
```
def quotient : D ⊗[k] V →ₗ[D] tensor f V := (relations f V).mkQ
…
```
Mentions: OAI.DerivedBar.Balanced.tensor, OAI.DerivedBar.Balanced.relations
theorem OAI.DerivedBar.Balanced.balanced line 28
Source documentation
The defining balanced relation, as an equality in the actual quotient module.
```
theorem balanced (d : D) (a : A) (v : V) :
    quotient f V ((d*f a) ⊗ₜ[k] v) = quotient f V (d ⊗ₜ[k] (a • v)) := by
…
```
Mentions: OAI.DerivedBar.Balanced.quotient
theorem OAI.DerivedBar.Balanced.map_relations line 39
Source documentation
Balanced tensor acts on all A-linear maps.
```
theorem map_relations (h : V →ₗ[A] W) : relations f V ≤
    ((quotient f W).comp (AlgebraTensorModule.lTensor D D (h.restrictScalars k))).ker := by
…
```
Mentions: OAI.DerivedBar.Balanced.relations, OAI.DerivedBar.Balanced.quotient
def OAI.DerivedBar.Balanced.map line 49
theorem OAI.DerivedBar.Balanced.map_quotient_tmul line 54
theorem OAI.DerivedBar.Balanced.map_comp line 58
Source documentation
Composition preservation for the actual balanced tensor, proved from its quotient presentation.
```
theorem map_comp (h : V →ₗ[A] W) (g : W →ₗ[A] U) :
    map f V U (g.comp h) = (map f W U g).comp (map f V W h) := by
…
```
Mentions: OAI.DerivedBar.Balanced.map
theorem OAI.DerivedBar.Balanced.map_zero line 65
theorem OAI.DerivedBar.Balanced.map_id line 72
def OAI.DerivedBar.Balanced.collapse line 82
Source documentation
Evaluation of D ⊗_k (A ⊗_k W) on the two leading coefficients.
```
def collapse : D ⊗[k] (A ⊗[k] W) →ₗ[D] D ⊗[k] W :=
…
```
theorem OAI.DerivedBar.Balanced.collapse_tmul line 86
theorem OAI.DerivedBar.Balanced.relations_le_ker_collapse line 90
Source documentation
The evaluation kills all balancing relations, without commutativity of A or D.
```
theorem relations_le_ker_collapse : relations f (A ⊗[k] W) ≤ (collapse f W).ker := by
…
```
Mentions: OAI.DerivedBar.Balanced.relations, OAI.DerivedBar.Balanced.collapse
def OAI.DerivedBar.Balanced.descend line 98
Source documentation
Descent of coefficient evaluation to the balanced tensor.
```
def descend : tensor f (A ⊗[k] W) →ₗ[D] D ⊗[k] W :=
…
```
Mentions: OAI.DerivedBar.Balanced.tensor
def OAI.DerivedBar.Balanced.insert line 102
Source documentation
The inverse inserts a unit A coefficient before taking the balanced quotient.
```
def insert : D ⊗[k] W →ₗ[D] tensor f (A ⊗[k] W) :=
…
```
Mentions: OAI.DerivedBar.Balanced.tensor
theorem OAI.DerivedBar.Balanced.descend_quotient line 106
theorem OAI.DerivedBar.Balanced.insert_tmul line 109
theorem OAI.DerivedBar.Balanced.descend_insert line 113
Source documentation
One inverse identity of the actual balanced free-module tensor equivalence.
```
theorem descend_insert : (descend f W).comp (insert f W) = LinearMap.id := by
…
```
Mentions: OAI.DerivedBar.Balanced.descend, OAI.DerivedBar.Balanced.insert
theorem OAI.DerivedBar.Balanced.insert_descend line 119
Source documentation
The other inverse identity follows from balancing, not from flatness.
```
theorem insert_descend : (insert f W).comp (descend f W) = LinearMap.id := by
…
```
Mentions: OAI.DerivedBar.Balanced.insert, OAI.DerivedBar.Balanced.descend
def OAI.DerivedBar.Balanced.freeEquiv line 133
Source documentation
The standard identification D ⊗_A (A ⊗_k W) ≅ D ⊗_k W for arbitrary algebras.
```
def freeEquiv : tensor f (A ⊗[k] W) ≃ₗ[D] D ⊗[k] W :=
…
```
Mentions: OAI.DerivedBar.Balanced.tensor