KaroubiEvaluation.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.LittleFinitistic.QuadraticEncoding.splitKaroubiIso line 13

Source documentation

An actual splitting realizes the corresponding formal Karoubi object.

def splitKaroubiIso {A I : C} (p : A ⟶ A) (hp : p ≫ p = p)
    (π : A ⟶ I) (ι : I ⟶ A) (hπι : π ≫ ι = p) (hιπ : ι ≫ π = 𝟙 I) :
    (⟨A,p,hp⟩ : Karoubi C) ≅ (toKaroubi C).obj I where
…

def OAI.LittleFinitistic.QuadraticEncoding.transportKaroubiIso line 22
Source documentation
An isomorphism commuting with idempotents identifies their formal summands.
```
def transportKaroubiIso (A B : Karoubi C) (e : A.X ≅ B.X)
    (h : A.p ≫ e.hom = e.hom ≫ B.p) : A ≅ B where
…
```
Mentions: OAI.LittleFinitistic.QuadraticEncoding.B
def OAI.LittleFinitistic.QuadraticEncoding.karoubiEvaluation line 43
def OAI.LittleFinitistic.QuadraticEncoding.quotientSummand line 47
def OAI.LittleFinitistic.QuadraticEncoding.stalkSummand line 52
def OAI.LittleFinitistic.QuadraticEncoding.evaluatedSummandIso line 60
Source documentation
The evaluated formal summand has precisely the idempotent induced by r on Y.
```
def evaluatedSummandIso (r : PresentedAlgebra P) (hr : r*r=r) :
    (karoubiEvaluation X).obj (quotientSummand r hr) ≅ stalkSummand X r hr :=
…
```
Mentions: OAI.LittleFinitistic.QuadraticEncoding.PresentedAlgebra, OAI.LittleFinitistic.QuadraticEncoding.karoubiEvaluation, OAI.LittleFinitistic.QuadraticEncoding.quotientSummand, OAI.LittleFinitistic.QuadraticEncoding.stalkSummand