PublishedInputs.lean`

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

def OAI.BoundedHochschild.CentralCorner.includeMap line 19
Source documentation
The inclusion of a corner into its ambient algebra.
```
def includeMap : Corner p hp →L[ℂ] M :=
…
```
def OAI.BoundedHochschild.CentralCorner.compressMap line 23
Source documentation
Compression to a central corner, which is an algebra homomorphism.
```
def compressMap : M →L[ℂ] Corner p hp :=
…
```
lemma OAI.BoundedHochschild.CentralCorner.includeMap_apply line 41
lemma OAI.BoundedHochschild.CentralCorner.compressMap_coe line 43
lemma OAI.BoundedHochschild.CentralCorner.compressMap_includeMap line 47
lemma OAI.BoundedHochschild.CentralCorner.compressMap_mul line 51
lemma OAI.BoundedHochschild.CentralCorner.compressMap_left_module line 57
lemma OAI.BoundedHochschild.CentralCorner.compressMap_right_module line 64
lemma OAI.BoundedHochschild.CentralCorner.compressMap_norm line 70
def OAI.BoundedHochschild.CentralCorner.restrict line 75
Source documentation
Restrict inputs to a central corner and compress the output.
```
def restrict {n : ℕ} (f : Cochain M n) : Cochain (Corner p hp) n :=
…
```
Mentions: OAI.BoundedHochschild.Cochain
def OAI.BoundedHochschild.CentralCorner.extend line 80
Source documentation
Pull a corner cochain back along central compression.
```
def extend {n : ℕ} (g : Cochain (Corner p hp) n) : Cochain M n :=
…
```
Mentions: OAI.BoundedHochschild.Cochain
lemma OAI.BoundedHochschild.CentralCorner.restrict_apply line 85
lemma OAI.BoundedHochschild.CentralCorner.extend_apply line 89
lemma OAI.BoundedHochschild.CentralCorner.restrict_norm line 93
lemma OAI.BoundedHochschild.CentralCorner.extend_norm line 99
lemma OAI.BoundedHochschild.CentralCorner.extend_supported line 108
lemma OAI.BoundedHochschild.CentralCorner.merge_include line 113
lemma OAI.BoundedHochschild.CentralCorner.merge_compress line 120
lemma OAI.BoundedHochschild.CentralCorner.differential_restrict line 129
Source documentation
Restriction to a central corner commutes with the Hochschild differential.
```
lemma differential_restrict {n : ℕ} (f : Cochain M n)
    (x : Fin (n + 1) → Corner p hp) :
    differentialValue (restrict p hp hc f) x =
      compressMap p hp hc (differentialValue f (fun i => (x i : M))) := by
…
```
Mentions: OAI.BoundedHochschild.Cochain, OAI.BoundedHochschild.differentialValue, OAI.BoundedHochschild.CentralCorner.restrict, OAI.BoundedHochschild.CentralCorner.compressMap
lemma OAI.BoundedHochschild.CentralCorner.restrict_cocycle line 137
lemma OAI.BoundedHochschild.CentralCorner.differential_extend line 145
Source documentation
A primitive on a central corner pulls back to a primitive of the central cut.
```
lemma differential_extend {n : ℕ} (g : Cochain (Corner p hp) n) (x : Fin (n + 1) → M) :
    differentialValue (extend p hp hc g) x =
      (differentialValue (M := Corner p hp) g (fun i => compressMap p hp hc (x i)) : M) := by
…
```
Mentions: OAI.BoundedHochschild.Cochain, OAI.BoundedHochschild.differentialValue, OAI.BoundedHochschild.CentralCorner.extend, OAI.BoundedHochschild.CentralCorner.compressMap
lemma OAI.BoundedHochschild.CentralCorner.extend_primitive line 159
theorem OAI.BoundedHochschild.CentralCorner.wstar line 174
Source documentation
A central corner carries the quotient predual of its ambient algebra.
```
theorem wstar : WStarAlgebra (Corner p hp) :=
…
```
lemma OAI.BoundedHochschild.CentralCorner.restrict_curryRight line 179
lemma OAI.BoundedHochschild.CentralCorner.restrict_last_normal line 191
Source documentation
Restriction to a central summand preserves normality in the last input.
```
lemma restrict_last_normal {n : ℕ} (f : Cochain M (n + 1))
    (hn : ∀ a : Fin n → M, HasPreadjoint e (f.curryRight a)) :
    ∀ a : Fin n → Corner p hp,
      HasPreadjoint (cornerPredualEquiv p hp e) ((restrict p hp hc f).curryRight a) := by
…
```
Mentions: OAI.BoundedHochschild.Cochain, OAI.BoundedHochschild.HasPreadjoint, OAI.BoundedHochschild.CentralCorner.restrict