TwoSided.lean`

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DerivedBar.FreeBaseChange.coefficient line 17
Source documentation
Replace only the free leading algebra coefficient along f.
```
def coefficient : A ⊗[k] V →ₗ[k] D ⊗[k] V :=
…
```
theorem OAI.DerivedBar.FreeBaseChange.coefficient_tmul line 20
theorem OAI.DerivedBar.FreeBaseChange.coefficient_smul line 24
Source documentation
Coefficient change intertwines the two regular left actions.
```
theorem coefficient_smul (a : A) (z : A ⊗[k] V) :
    coefficient f V (a • z) = f a • coefficient f V z := by
…
```
Mentions: OAI.DerivedBar.FreeBaseChange.coefficient
def OAI.DerivedBar.FreeBaseChange.map line 31
Source documentation
Scalar extension of a morphism between explicitly free A-modules.
```
def map (h : A ⊗[k] V →ₗ[A] A ⊗[k] W) : D ⊗[k] V →ₗ[D] D ⊗[k] W :=
…
```
theorem OAI.DerivedBar.FreeBaseChange.map_tmul line 36
theorem OAI.DerivedBar.FreeBaseChange.map_coefficient line 40
Source documentation
Extension commutes with the map on arbitrary free tensors, not just generators.
```
theorem map_coefficient (h : A ⊗[k] V →ₗ[A] A ⊗[k] W) (z : A ⊗[k] V) :
    map f V W h (coefficient f V z) = coefficient f W (h z) := by
…
```
Mentions: OAI.DerivedBar.FreeBaseChange.map, OAI.DerivedBar.FreeBaseChange.coefficient
theorem OAI.DerivedBar.FreeBaseChange.map_comp line 51
Source documentation
Composition of actual free-module maps is preserved by extension.
```
theorem map_comp (h : A ⊗[k] V →ₗ[A] A ⊗[k] W)
    (g : A ⊗[k] W →ₗ[A] A ⊗[k] U) :
    map f V U (g.comp h) = (map f W U g).comp (map f V W h) := by
…
```
Mentions: OAI.DerivedBar.FreeBaseChange.map
theorem OAI.DerivedBar.FreeBaseChange.map_zero line 60
theorem OAI.DerivedBar.FreeBaseChange.map_id line 65
def OAI.DerivedBar.twoSidedDifferential line 78
Source documentation
The two-sided absolute bar differential after changing the free coefficient A to D.
```
def twoSidedDifferential (n : ℕ) :
    D ⊗[k] term k A N (n+1) →ₗ[D] D ⊗[k] term k A N n :=
…
```
Mentions: OAI.DerivedBar.term
theorem OAI.DerivedBar.twoSidedDifferential_tmul line 83
Source documentation
The endpoint face minus the remaining absolute bar faces, with their actual signs.
```
theorem twoSidedDifferential_tmul (n : ℕ) (d : D) (z : term k A N (n+1)) :
    twoSidedDifferential k A D N f n (d ⊗ₜ[k] z) =
      d • FreeBaseChange.coefficient f (term k A N n) z -
        d ⊗ₜ[k] differential k A N n z := by
…
```
Mentions: OAI.DerivedBar.term, OAI.DerivedBar.twoSidedDifferential, OAI.DerivedBar.FreeBaseChange.coefficient, OAI.DerivedBar.differential
theorem OAI.DerivedBar.twoSidedDifferential_sq line 92
def OAI.DerivedBar.twoSidedComplex line 99
Source documentation
Actual D-linear two-sided bar complex with degree-n term D ⊗_k A^⊗n ⊗_k N.
```
def twoSidedComplex : ChainComplex (ModuleCat D) ℕ :=
…
```