InducedColumns.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

def OAI.ExternalTensor.leftIdeal line 14
Source documentation
The actual principal left ideal B e, the image of right multiplication by e.
```
def leftIdeal (e : B) : Submodule B B := (LinearMap.mulRight B e).range
```
theorem OAI.ExternalTensor.mem_leftIdeal line 16
theorem OAI.ExternalTensor.leftIdeal_finiteDimensional line 19
abbrev OAI.ExternalTensor.Column line 30
Source documentation
The induced column in Section 4, with its external actions.
```
abbrev Column (e : B) := (leftIdeal B e) ⊗[k] N
```
Mentions: OAI.ExternalTensor.leftIdeal
theorem OAI.ExternalTensor.column_projective line 32
theorem OAI.ExternalTensor.column_finite_right line 36
theorem OAI.ExternalTensor.column_finiteDimensional line 40

theorem OAI.ExternalTensor.induced_column line 46

Source documentation

The full induced-column assertion required for each summand of L'_0,L'_1,L'_2.

theorem induced_column [FiniteDimensional k B] (e : B)
    [Module.Finite Bᵐᵒᵖ N] [Module.Projective Bᵐᵒᵖ N] :
    FiniteDimensional k (Column k B N e) ∧
      Module.Finite Bᵐᵒᵖ (Column k B N e) ∧
      Module.Projective Bᵐᵒᵖ (Column k B N e) :=
…

Mentions: OAI.ExternalTensor.Column

def OAI.ExternalTensor.generator line 56
Source documentation
The distinguished generator e of the principal left ideal.
```
def generator (e : B) : leftIdeal B e := ⟨e, ⟨1, one_mul e⟩⟩
```
Mentions: OAI.ExternalTensor.leftIdeal
def OAI.ExternalTensor.columnInclusion line 59
Source documentation
The right-linear insertion used in the vertex maps iota_i.
```
def columnInclusion (e : B) : N →ₗ[Bᵐᵒᵖ] Column k B N e where
…
```
Mentions: OAI.ExternalTensor.Column
theorem OAI.ExternalTensor.columnInclusion_apply line 64
def OAI.ExternalTensor.pathMap line 70
Source documentation
Right multiplication by a path a: i→j maps B e_j to B e_i. Only the relation a e_i = a is needed for membership in the target ideal.
```
def pathMap (ei ej a : B) (ha : a * ei = a) :
    leftIdeal B ej →ₗ[B] leftIdeal B ei where
…
```
Mentions: OAI.ExternalTensor.leftIdeal
theorem OAI.ExternalTensor.pathMap_apply line 76
def OAI.ExternalTensor.columnPath line 81
Source documentation
The path-multiplication component c tensor n ↦ ca tensor n of the rectification maps.
```
def columnPath (ei ej a : B) (ha : a * ei = a) :
    Column k B N ej →ₗ[B ⊗[k] Bᵐᵒᵖ] Column k B N ei :=
…
```
Mentions: OAI.ExternalTensor.Column
theorem OAI.ExternalTensor.columnPath_tmul line 85
def OAI.ExternalTensor.columnMap line 93
Source documentation
The differential or relation-homotopy component c tensor n ↦ c tensor f(n).
```
def columnMap (e : B) (f : N →ₗ[Bᵐᵒᵖ] N') :
    Column k B N e →ₗ[B ⊗[k] Bᵐᵒᵖ] Column k B N' e :=
…
```
Mentions: OAI.ExternalTensor.Column
theorem OAI.ExternalTensor.columnMap_tmul line 97