OrdinaryFullTensorTerms.lean`

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

instance OAI.LittleFinitistic.OrdinarySimulation.BimoduleO.commuteRightTensor line 14
abbrev OAI.LittleFinitistic.OrdinarySimulation.FullTensorTerm line 18
Source documentation
Every degree of Q_T tensor_BC O, carrying the actual outside B-actions.
```
abbrev FullTensorTerm (n : ℕ) := TwoSidedTensor k (B ⊗[k] ChainAlgebra k l) B Bᵐᵒᵖ
…
```
Mentions: OAI.LittleFinitistic.TwoSidedTensor, OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra
def OAI.LittleFinitistic.OrdinarySimulation.FullTensorTerm.supportedIdealEquiv line 25
Source documentation
Supported extended ideals are the same right ideals as the finite vertex terms.
```
def supportedIdealEquiv (n : ℕ) (hn : n ≤ l) :
    TensorResolution.term k B l n ≃ₗ[(B ⊗[k] ChainAlgebra k l)ᵐᵒᵖ]
      IdempotentTensor.rightIdeal (TensorIdeal.vertex (k := k) (B := B) (vertex k l ⟨n,by omega⟩)) where
…
```
Mentions: OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.term, OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra, OAI.LittleFinitistic.IdempotentTensor.rightIdeal, OAI.LittleFinitistic.OrdinarySimulation.TensorIdeal.vertex
def OAI.LittleFinitistic.OrdinarySimulation.FullTensorTerm.finiteModel line 42
def OAI.LittleFinitistic.OrdinarySimulation.FullTensorTerm.supportedEquiv line 54
Source documentation
Actual degreewise B-bimodule comparison throughout the supported range.
```
def supportedEquiv (n : ℕ) (hn : n ≤ l) : FullTensorTerm P a l n ≃ₗ[Enveloping k B] P.X (a+(n:ℤ)) :=
…
```
Mentions: OAI.LittleFinitistic.OrdinarySimulation.FullTensorTerm, OAI.LittleFinitistic.OrdinarySimulation.Enveloping
theorem OAI.LittleFinitistic.OrdinarySimulation.FullTensorTerm.subsingleton_above line 59
def OAI.LittleFinitistic.OrdinarySimulation.FullTensorTerm.outsideEquiv line 66
Source documentation
Use precisely the source's upper support bound for all remaining degrees.
```
def outsideEquiv (n : ℕ) (hn : l < n) (hP : IsZero (P.X (a+(n:ℤ)))) :
    FullTensorTerm P a l n ≃ₗ[Enveloping k B] P.X (a+(n:ℤ)) := by
…
```
Mentions: OAI.LittleFinitistic.OrdinarySimulation.FullTensorTerm, OAI.LittleFinitistic.OrdinarySimulation.Enveloping
def OAI.LittleFinitistic.OrdinarySimulation.FullTensorTerm.termEquiv line 78
Source documentation
No extra support assumptions: P is required to vanish only above a+l here.
```
def termEquiv (hP : ∀ n : ℕ, l < n → IsZero (P.X (a+(n:ℤ)))) (n : ℕ) :
    FullTensorTerm P a l n ≃ₗ[Enveloping k B] P.X (a+(n:ℤ)) :=
…
```
Mentions: OAI.LittleFinitistic.OrdinarySimulation.FullTensorTerm, OAI.LittleFinitistic.OrdinarySimulation.Enveloping