StrictCompositeListReplacement.lean`

79 declarations, 0 contain sorry, 0 declared as axioms

Removing maximal new objects

The finite induction in the couniversality proof splits the poset into two full sieves by deleting distinct maximal objects outside the old sieve. The restricted sieves retain the right adjoint.

theorem OAI.Thomason.Construction.two_maximal_of_no_greatest line 28

Source documentation

In a finite nonempty set with no greatest element, there are two distinct maximal elements.

theorem two_maximal_of_no_greatest {S : Set E} (hS : S.Finite) (hne : S.Nonempty)
    (hgreatest : ¬ ∃ x, x ∈ S ∧ ∀ y ∈ S, y ≤ x) :
    ∃ x y, Maximal (· ∈ S) x ∧ Maximal (· ∈ S) y ∧ x ≠ y := by
…

theorem OAI.Thomason.Construction.SieveRetraction.maximal_complement_is_maximal line 51
Source documentation
Maximality in the complement of a sieve implies maximality in the ambient poset; a morphism from a new object to an old object is impossible.
```
theorem maximal_complement_is_maximal {x : E} (hx : Maximal (· ∉ A) x) :
    Maximal (fun _ : E => True) x := by
…
```
theorem OAI.Thomason.Construction.SieveRetraction.delete_maximal_isLowerSet line 59
Source documentation
Deleting a maximal object leaves a sieve.
```
theorem delete_maximal_isLowerSet {x : E} (hx : Maximal (fun _ : E => True) x) :
    IsLowerSet {e : E | e ≠ x} := by
…
```
def OAI.Thomason.Construction.SieveRetraction.restrict line 67
Source documentation
Restriction to any full subposet containing the old part preserves the right-adjoint retraction. Downward closure of the subposet is not needed.
```
def restrict (S : Set E) (hAS : A ⊆ S) :
    SieveRetraction {e : S | (e : E) ∈ A} where
…
```
Mentions: OAI.Thomason.Construction.SieveRetraction
theorem OAI.Thomason.Construction.SieveRetraction.finite_two_sieve_cover line 80
Source documentation
The two-sieve cover used by the finite couniversality induction.
```
theorem finite_two_sieve_cover [Finite E]
    (hne : (Aᶜ).Nonempty) (hgreatest : ¬ ∃ x, GreatestNew (A := A) x) :
…
```
Mentions: OAI.Thomason.Construction.SieveRetraction.GreatestNew
structure OAI.Thomason.Construction.StrictOmegaCategory line 134
Source documentation
A strict globular omega-category with identities represented by the same cell at all higher dimensions. All compositions, units and interchange laws are strict equalities.
```
structure StrictOmegaCategory where
…
```
instance OAI.Thomason.Construction.StrictOmegaCategory.(instance at line 171) line 171
abbrev OAI.Thomason.Construction.StrictOmegaCategory.source line 173
abbrev OAI.Thomason.Construction.StrictOmegaCategory.target line 174
structure OAI.Thomason.Construction.StrictOmegaCategory.Hom line 178
Source documentation
A strict functor preserves both boundaries and every defined composition.
```
structure Hom (C : StrictOmegaCategory.{u}) (D : StrictOmegaCategory.{v}) where
…
```
instance OAI.Thomason.Construction.StrictOmegaCategory.(instance at line 185) line 185
def OAI.Thomason.Construction.StrictOmegaCategory.Hom.id line 190
def OAI.Thomason.Construction.StrictOmegaCategory.Hom.comp line 195
theorem OAI.Thomason.Construction.StrictOmegaCategory.Hom.id_apply line 204
theorem OAI.Thomason.Construction.StrictOmegaCategory.Hom.comp_apply line 205
instance OAI.Thomason.Construction.StrictOmegaCategory.(instance at line 210) line 210
def OAI.Thomason.Construction.StrictOmegaCategory.DimensionLE line 220
Source documentation
A cell has dimension at most n precisely when its n-boundaries are itself. Higher identity extensions require no extra cell data.
```
def DimensionLE (C : StrictOmegaCategory) (n : ℕ) (x : C) : Prop :=
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory
theorem OAI.Thomason.Construction.StrictOmegaCategory.face_face_same line 224
theorem OAI.Thomason.Construction.StrictOmegaCategory.face_dimensionLE line 228
theorem OAI.Thomason.Construction.StrictOmegaCategory.dimensionLE_mono line 232
theorem OAI.Thomason.Construction.StrictOmegaCategory.Hom.dimensionLE line 240

theorem OAI.Thomason.Construction.StrictOmegaCategory.dimensionLE_comp line 247

Source documentation

Composing along a strictly lower boundary preserves a dimension bound.

theorem dimensionLE_comp (C : StrictOmegaCategory) {n m : ℕ} (hnm : n < m)
    {x y : C} (hx : C.DimensionLE m x) (hy : C.DimensionLE m y)
    (h : C.target n x = C.source n y) : C.DimensionLE m (C.comp n x y h) := by
…

Mentions: OAI.Thomason.Construction.StrictOmegaCategory

def OAI.Thomason.Construction.StrictOmegaCategory.IsTruncated line 266
Source documentation
Strict n-categories are the full subcategory with a uniform dimension bound; no invertibility condition is imposed.
```
def IsTruncated (C : StrictOmegaCategory) (n : ℕ) : Prop :=
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory
def OAI.Thomason.Construction.StrictOmegaCategory.Truncated line 269
instance OAI.Thomason.Construction.StrictOmegaCategory.(instance at line 271) line 271
def OAI.Thomason.Construction.StrictOmegaCategory.inclusion line 280
Source documentation
The fully faithful inclusion of strict n-categories into omega-categories.
```
def inclusion (n : ℕ) : Truncated.{u} n ⥤ StrictOmegaCategory.{u} where
…
```
def OAI.Thomason.Construction.StrictOmegaCategory.FullCell line 308
Source documentation
All cells whose two object boundaries lie in the specified set.
```
def FullCell (x : C) : Prop := C.source 0 x ∈ S ∧ C.target 0 x ∈ S
```
theorem OAI.Thomason.Construction.StrictOmegaCategory.fullCell_face line 310
theorem OAI.Thomason.Construction.StrictOmegaCategory.zero_face_comp_succ line 325
Source documentation
A positive-dimensional composition has the object boundaries of its first factor. This follows directly from globularity.
```
theorem zero_face_comp_succ (a : Bool) (n : ℕ) (x y : C)
    (hxy : C.target (n + 1) x = C.source (n + 1) y) :
    C.face a 0 (C.comp (n + 1) x y hxy) = C.face a 0 x := by
…
```
theorem OAI.Thomason.Construction.StrictOmegaCategory.fullCell_comp line 333
def OAI.Thomason.Construction.StrictOmegaCategory.fullOn line 346
Source documentation
The full strict omega-subcategory on a set of object cells.
```
def fullOn : StrictOmegaCategory.{u} where
…
```
def OAI.Thomason.Construction.StrictOmegaCategory.fullInclusion line 367
Source documentation
The inclusion preserves all strict compositions and faces.
```
def fullInclusion : C.fullOn S ⟶ C where
…
```
theorem OAI.Thomason.Construction.StrictOmegaCategory.fullOn_isTruncated line 373
Source documentation
Full subcategories preserve any bound on dimension.
```
theorem fullOn_isTruncated {n : ℕ} (hC : C.IsTruncated n) : (C.fullOn S).IsTruncated n := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.IsTruncated
def OAI.Thomason.Construction.StrictOmegaCategory.fullMap line 378
Source documentation
Restrict a strict functor that sends the selected objects to selected objects.
```
def fullMap {D : StrictOmegaCategory.{u}} (T : Set D) (f : C ⟶ D)
    (h : ∀ x ∈ S, f.toFun x ∈ T) : C.fullOn S ⟶ D.fullOn T where
…
```

theorem OAI.Thomason.Construction.StrictOmegaCategory.fullMap_inclusion line 392

Source documentation

Restriction commutes strictly with the inclusions.

theorem fullMap_inclusion {D : StrictOmegaCategory.{u}} (T : Set D) (f : C ⟶ D)
    (h : ∀ x ∈ S, f.toFun x ∈ T) :
    C.fullMap S T f h ≫ D.fullInclusion T = C.fullInclusion S ≫ f := by
…

instance OAI.Thomason.Construction.StrictOmegaCategory.fullInclusion_mono line 399
Source documentation
Full-subcategory inclusions are monomorphisms of actual strict categories.
```
instance fullInclusion_mono : Mono (C.fullInclusion S) where
…
```
inductive OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Term line 429
Source documentation
Finite expressions over the cells of the small diagram.
```
inductive Term where
…
```
def OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Term.eval line 440
Source documentation
Evaluation in any given cocone. On inadmissible expressions the first factor supplies a harmless totalization; admitted terms never use it.
```
noncomputable def eval (s : Cocone F) (t : Term F) : s.pt := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Term
theorem OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Term.eval_gen line 447
theorem OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Term.eval_face line 450
theorem OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Term.eval_comp line 453
inductive OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Good line 462
Source documentation
Admissibility uses only boundary equations forced by the diagram.
```
inductive Good : Term F → Prop where
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Term
theorem OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Good.uniformDimension line 471
Source documentation
Each admitted finite expression has one finite dimension bound valid in every cocone. In particular the quotient will be an omega-category.
```
theorem Good.uniformDimension {t : Term F} (ht : Good F t) :
    ∃ n, ∀ s : Cocone F, s.pt.DimensionLE n (t.eval s) := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Term, OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Good
abbrev OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Admitted line 489
Source documentation
The small carrier before quotienting.
```
abbrev Admitted := {t : Term F // Good F t}
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Term, OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Good
def OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Rel line 492
Source documentation
Equality forced by every strict cocone on the diagram.
```
def Rel (x y : Admitted F) : Prop := ∀ s : Cocone F, x.val.eval s = y.val.eval s
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Admitted
instance OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.semanticSetoid line 494
abbrev OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Cell line 500
Source documentation
A small quotient: large cocones occur only in its defining proposition.
```
abbrev Cell := Quotient (semanticSetoid F)
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.semanticSetoid
def OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Cell.eval line 507
Source documentation
Interpret a quotient cell in any cocone.
```
noncomputable def eval (s : Cocone F) : Cell F → s.pt :=
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Cell
theorem OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Cell.eval_mk line 510
theorem OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Cell.ext line 514
Source documentation
The family of cocone evaluations jointly distinguishes quotient cells.
```
theorem ext {x y : Cell F} (he : ∀ s : Cocone F, eval s x = eval s y) : x = y := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Cell, OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Cell.eval
def OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Cell.representative line 539
Source documentation
A representative is used only to define operations; all evaluations below show that the resulting quotient cells are independent of it.
```
noncomputable def representative (x : Cell F) : Admitted F := Quotient.out x
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Cell, OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Admitted
theorem OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Cell.eval_representative line 541
def OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Cell.face line 545
theorem OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Cell.eval_face line 548
theorem OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Cell.composable_eval line 554
Source documentation
Matching quotient boundaries match in every testing cocone.
```
theorem composable_eval (n : ℕ) {x y : Cell F}
    (he : face true n x = face false n y) (s : Cocone F) :
    s.pt.target n (eval s x) = s.pt.source n (eval s y) := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Cell, OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Cell.face, OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Cell.eval
theorem OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Cell.representative_composable line 561
Source documentation
Consequently composition of any matching quotient cells is admitted.
```
theorem representative_composable (n : ℕ) {x y : Cell F}
    (he : face true n x = face false n y) (s : Cocone F) :
    s.pt.target n ((representative x).val.eval s) =
      s.pt.source n ((representative y).val.eval s) := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Cell, OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Cell.face, OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Cell.representative
def OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Cell.comp line 568
theorem OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Cell.eval_comp line 574
Source documentation
Every testing cocone preserves the quotient composition on all cells.
```
theorem eval_comp (s : Cocone F) (n : ℕ) (x y : Cell F)
    (he : face true n x = face false n y) :
    eval s (comp n x y he) = s.pt.comp n (eval s x) (eval s y) (composable_eval n he s) := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Cell, OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Cell.face, OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Cell.eval, OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Cell.comp, OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Cell.composable_eval
abbrev OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.category line 597
Source documentation
Every strict law is detected by the jointly injective cocone evaluations.
```
noncomputable abbrev category : StrictOmegaCategory.{0} where
…
```
def OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.evaluation line 659
Source documentation
Every model evaluation is an actual strict functor.
```
noncomputable def evaluation (s : Cocone F) : category F ⟶ s.pt where
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.category
def OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.generator line 679
Source documentation
The original diagram cells as quotient cells.
```
def generator (j : J) (x : F.obj j) : Cell F :=
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Cell
theorem OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.eval_generator line 682
def OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.leg line 686
Source documentation
Each original diagram object maps by an actual strict functor.
```
noncomputable def leg (j : J) : F.obj j ⟶ category F where
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.category
def OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.cocone line 703
Source documentation
All the original diagram relations hold in the quotient.
```
noncomputable def cocone : Cocone F where
…
```
theorem OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.evaluation_fac line 716
Source documentation
Evaluation extends the prescribed cocone on every original diagram object.
```
theorem evaluation_fac (s : Cocone F) (j : J) :
    leg F j ≫ evaluation F s = s.ι.app j := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.leg, OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.evaluation
theorem OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Cell.mk_face line 738
Source documentation
A face expression represents the face of the represented cell.
```
theorem mk_face (a : Bool) (n : ℕ) (x : Admitted F) :
    Quotient.mk _ (⟨.face a n x.val, .face a n x.property⟩ : Admitted F) =
      face a n (Quotient.mk _ x) := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Admitted, OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Cell.face
theorem OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Cell.mk_match line 746
Source documentation
Every admitted composition has matching boundaries in the quotient.
```
theorem mk_match (n : ℕ) (x y : Admitted F)
    (he : ∀ s : Cocone F, s.pt.target n (x.val.eval s) = s.pt.source n (y.val.eval s)) :
    face true n (Quotient.mk _ x) = face false n (Quotient.mk _ y) := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Admitted, OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Cell.face
theorem OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Cell.mk_comp line 754
Source documentation
A composition expression represents exactly the quotient composition.
```
theorem mk_comp (n : ℕ) (x y : Admitted F)
    (he : ∀ s : Cocone F, s.pt.target n (x.val.eval s) = s.pt.source n (y.val.eval s))
    (hq : face true n (Quotient.mk _ x) = face false n (Quotient.mk _ y)) :
    Quotient.mk _ (⟨.comp n x.val y.val, .comp n x.property y.property he⟩ : Admitted F) =
      comp n (Quotient.mk _ x) (Quotient.mk _ y) hq := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Admitted, OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Cell.face, OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Cell.comp
theorem OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.map_term line 770
Source documentation
Any strict map agreeing on the diagram generators agrees on all finite admitted cell expressions.
```
theorem map_term (s : Cocone F) (m : category F ⟶ s.pt)
    (hm : ∀ j, leg F j ≫ m = s.ι.app j) {t : Term F} (ht : Good F t) :
    m.toFun (Quotient.mk _ (⟨t, ht⟩ : Admitted F)) = t.eval s := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.category, OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.leg, OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Term, OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Good, OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.Admitted
theorem OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.hom_ext line 791
Source documentation
The original generator legs are jointly epimorphic among strict maps.
```
theorem hom_ext {D : StrictOmegaCategory.{0}} (f g : category F ⟶ D)
    (he : ∀ j, leg F j ≫ f = leg F j ≫ g) : f = g := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.category, OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.leg
def OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.isColimit line 804
Source documentation
The small semantic quotient is the colimit of the original diagram.
```
noncomputable def isColimit : IsColimit (cocone F) where
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.ColimitConstruction.cocone
inductive OAI.Thomason.Construction.StrictOmegaCategory.CompositeList line 827
theorem OAI.Thomason.Construction.StrictOmegaCategory.CompositeList.nonempty line 837
theorem OAI.Thomason.Construction.StrictOmegaCategory.CompositeList.map line 842
Source documentation
Strict functors carry every matching iterated composite to the corresponding iterated composite of its images.
```
theorem map (F : Hom C D) {xs : List C} {x : C} (h : CompositeList C r xs x) :
    CompositeList D r (xs.map F.toFun) (F.toFun x) := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Hom, OAI.Thomason.Construction.StrictOmegaCategory.CompositeList
theorem OAI.Thomason.Construction.StrictOmegaCategory.CompositeList.append line 854
Source documentation
Concatenating two matching strings gives their binary strict composite.
```
theorem append {xs ys : List C} {x y : C}
    (hx : CompositeList C r xs x) (hy : CompositeList C r ys y)
    (hxy : C.target r x = C.source r y) :
    CompositeList C r (xs ++ ys) (C.comp r x y hxy) := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.CompositeList

theorem OAI.Thomason.Construction.StrictOmegaCategory.CompositeList.split line 869

Source documentation

Every cut with two nonempty sides is a genuine binary factorization.

theorem split {xs ys : List C} {z : C}
    (h : CompositeList C r (xs ++ ys) z) (hxs : xs ≠ []) (hys : ys ≠ []) :
    ∃ (x y : C) (hxy : C.target r x = C.source r y),
      CompositeList C r xs x ∧ CompositeList C r ys y ∧ C.comp r x y hxy = z := by
…

Mentions: OAI.Thomason.Construction.StrictOmegaCategory.CompositeList

theorem OAI.Thomason.Construction.StrictOmegaCategory.CompositeList.total_unique line 912
theorem OAI.Thomason.Construction.StrictOmegaCategory.CompositeList.pair line 927
theorem OAI.Thomason.Construction.StrictOmegaCategory.CompositeList.replace_first_pair line 930