StrictPushoutGeneration.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Fibers of actual labelled pushouts

The published input is Ara--Maltsiniotis (2014), Lemma 2.8, arXiv:1305.5086v3, pp.14--15: either endpoint-fiber functor on the slice over the walking arrow has a right adjoint. The consequence used is preservation of small colimits by the concrete fiber functors. The same statement applies in every positive finite dimension and in omega dimension.

def OAI.Thomason.Construction.StrictOmegaCategory.finiteInterval line 27
Source documentation
The walking arrow as an actual strict positive finite category.
```
def finiteInterval (n : ℕ) : Truncated (n + 1) :=
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Truncated
def OAI.Thomason.Construction.StrictOmegaCategory.finiteLabelFiberFunctor line 34
Source documentation
Endpoint fibers of finite strict categories, formed by the same full subcategories of their ambient omega-categories.
```
def finiteLabelFiberFunctor (n : ℕ) (e : Fin 2) :
    Over (finiteInterval n) ⥤ Truncated (n + 1) where
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.finiteInterval, OAI.Thomason.Construction.StrictOmegaCategory.Truncated
structure OAI.Thomason.Construction.PublishedLabelFiberInput line 51
Source documentation
The small-colimit consequence of the precise published endpoint-fiber adjunction, on the actual functors defined above.
```
structure PublishedLabelFiberInput : Prop where
…
```

theorem OAI.Thomason.Construction.PublishedLabelFiberInput.omega_isPushout line 64

Source documentation

A labelled attaching pushout remains a pushout on either full endpoint fiber.

theorem omega_isPushout (e : Fin 2)
    {A B X Y : Over (StrictPoset.category (Fin 2))}
    {i : A ⟶ B} {a : A ⟶ X} {b : B ⟶ Y} {j : X ⟶ Y}
    (hp : IsPushout i a b j) :
    IsPushout ((StrictOmegaCategory.labelFiberFunctor (Fin 2) e).map i)
      ((StrictOmegaCategory.labelFiberFunctor (Fin 2) e).map a)
      ((StrictOmegaCategory.labelFiberFunctor (Fin 2) e).map b)
      ((StrictOmegaCategory.labelFiberFunctor (Fin 2) e).map j) := by
…

Mentions: OAI.Thomason.Construction.StrictPoset.category, OAI.Thomason.Construction.StrictOmegaCategory.labelFiberFunctor

theorem OAI.Thomason.Construction.PublishedLabelFiberInput.finite_isPushout line 76

Source documentation

The same statement uses genuine pushouts in the finite category.

theorem finite_isPushout (n : ℕ) (e : Fin 2)
    {A B X Y : Over (StrictOmegaCategory.finiteInterval n)}
    {i : A ⟶ B} {a : A ⟶ X} {b : B ⟶ Y} {j : X ⟶ Y}
    (hp : IsPushout i a b j) :
    IsPushout ((StrictOmegaCategory.finiteLabelFiberFunctor n e).map i)
      ((StrictOmegaCategory.finiteLabelFiberFunctor n e).map a)
      ((StrictOmegaCategory.finiteLabelFiberFunctor n e).map b)
      ((StrictOmegaCategory.finiteLabelFiberFunctor n e).map j) := by
…

Mentions: OAI.Thomason.Construction.StrictOmegaCategory.finiteInterval, OAI.Thomason.Construction.StrictOmegaCategory.finiteLabelFiberFunctor

theorem OAI.Thomason.Construction.StrictOmegaCategory.CompositionExpression.substitute line 110

Source documentation

Substitute actual expressions for the mapped generators of a strict composition expression.

theorem substitute {C D : StrictOmegaCategory.{0}} {I J : Type} {g : I → C} {h : J → D}
    (F : C ⟶ D) (hh : ∀ i, Nonempty (CompositionExpression D h (F.toFun (g i))))
    {x : C} (t : CompositionExpression C g x) :
    Nonempty (CompositionExpression D h (F.toFun x)) := by
…

Mentions: OAI.Thomason.Construction.StrictOmegaCategory.CompositionExpression

theorem OAI.Thomason.Construction.StrictOmegaCategory.CompositionExpression.face line 125
abbrev OAI.Thomason.Construction.StrictOmegaCategory.PushoutGeneration.category line 158
def OAI.Thomason.Construction.StrictOmegaCategory.PushoutGeneration.generators line 160
theorem OAI.Thomason.Construction.StrictOmegaCategory.PushoutGeneration.generators_face line 164
def OAI.Thomason.Construction.StrictOmegaCategory.PushoutGeneration.generated line 181
def OAI.Thomason.Construction.StrictOmegaCategory.PushoutGeneration.inclusion line 206
def OAI.Thomason.Construction.StrictOmegaCategory.PushoutGeneration.left line 211
def OAI.Thomason.Construction.StrictOmegaCategory.PushoutGeneration.right line 218
theorem OAI.Thomason.Construction.StrictOmegaCategory.PushoutGeneration.condition line 225
theorem OAI.Thomason.Construction.StrictOmegaCategory.PushoutGeneration.generated_by_pieces line 232
Source documentation
Every actual cell in a strict pushout is a finite composite of piece cells.
```
theorem generated_by_pieces (x : category f g) :
    Nonempty (CompositionExpression _ (generators f g) x) := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.PushoutGeneration.category, OAI.Thomason.Construction.StrictOmegaCategory.CompositionExpression, OAI.Thomason.Construction.StrictOmegaCategory.PushoutGeneration.generators