FormalSummandAction.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

instance OAI.LittleFinitistic.FormalSummandAction.karoubiHomSMul line 15
theorem OAI.LittleFinitistic.FormalSummandAction.smul_f line 18
instance OAI.LittleFinitistic.FormalSummandAction.karoubiHomModule line 21
instance OAI.LittleFinitistic.FormalSummandAction.karoubiLinear line 25
instance OAI.LittleFinitistic.FormalSummandAction.toKaroubiLinear line 29
def OAI.LittleFinitistic.FormalSummandAction.summand line 36
Source documentation
The formal image of the central selecting idempotent.
```
def summand : Karoubi C :=
…
```
lemma OAI.LittleFinitistic.FormalSummandAction.sandwich line 42
lemma OAI.LittleFinitistic.FormalSummandAction.compressed_mul line 48
def OAI.LittleFinitistic.FormalSummandAction.action line 52
Source documentation
The action on the formal summand, with restriction along alpha.
```
def action (α : R →ₐ[k] R) : R →ₐ[k] End (summand θ e he) where
…
```
Mentions: OAI.LittleFinitistic.FormalSummandAction.summand
theorem OAI.LittleFinitistic.FormalSummandAction.action_f line 75
def OAI.LittleFinitistic.FormalSummandAction.mapAction line 83
Source documentation
A linear functor transports an algebra action on endomorphisms.
```
def mapAction (F : C ⥤ D) [F.Additive] [F.Linear k] {X : C}
    (ρ : R →ₐ[k] End X) : R →ₐ[k] End (F.obj X) where
…
```

def OAI.LittleFinitistic.FormalSummandAction.biprodAction line 96

Source documentation

Direct sum of two actions of the same algebra.

noncomputable def biprodAction [HasBinaryBiproducts C] {X Y : C}
    (ρ : R →ₐ[k] End X) (σ : R →ₐ[k] End Y) : R →ₐ[k] End (X ⊞ Y) where
…

def OAI.LittleFinitistic.FormalSummandAction.transportAction line 116
Source documentation
Conjugating an action along an isomorphism.
```
def transportAction {X Y : C} (i : X ≅ Y) (ρ : R →ₐ[k] End Y) :
    R →ₐ[k] End X where
…
```
def OAI.LittleFinitistic.FormalSummandAction.oldAction line 132
Source documentation
An action on an old object in the completion is an actual old action.
```
def oldAction {X : C} (ρ : R →ₐ[k] End ((toKaroubi C).obj X)) :
    R →ₐ[k] End X where
…
```
theorem OAI.LittleFinitistic.FormalSummandAction.oldAction_lift line 141
instance OAI.LittleFinitistic.FormalSummandAction.formalShiftLinear line 150
def OAI.LittleFinitistic.FormalSummandAction.oddDoubleAction line 162
Source documentation
The selecting action on the odd double.
```
noncomputable def oddDoubleAction (α : R →ₐ[k] R) :
    R →ₐ[k] End (summand θ e he ⊞ OddDouble.formalShift (summand θ e he) 3) :=
…
```
Mentions: OAI.LittleFinitistic.FormalSummandAction.summand, OAI.LittleFinitistic.OddDouble.formalShift
theorem OAI.LittleFinitistic.FormalSummandAction.fixed_old_object_with_action line 168
Source documentation
The object and its unital action are both chosen before any evaluation module.
```
theorem fixed_old_object_with_action (α : R →ₐ[k] R) :
    ∃ (V₀ : C) (ρ₀ : R →ₐ[k] End V₀)
      (i : (toKaroubi C).obj V₀ ≅
        summand θ e he ⊞ OddDouble.formalShift (summand θ e he) 3),
      ∀ r : R, (toKaroubi C).map (ρ₀ r) ≫ i.hom =
        i.hom ≫ oddDoubleAction θ e he hc α r := by
…
```
Mentions: OAI.LittleFinitistic.FormalSummandAction.summand, OAI.LittleFinitistic.OddDouble.formalShift, OAI.LittleFinitistic.FormalSummandAction.oddDoubleAction