OAI/CategoryTheory/Thomason/Simplicial/SubdivisionUnions.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

Discharging the finite-poset unit input

This proves the needed specialization of Gagna's unit theorem from the constructed Gray contractions and the published full-sieve and simplicial gluing inputs. Neither the unit theorem, the Thomason transfer conclusion, nor a localization equivalence is used in the proof.

  1. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.unit_finite_poset line 37

    Source documentation

    The actual omega-categorification unit is weak on every finite poset.

    theorem unit_finite_poset
    (G : RightGrayInput h) (aw : SimplexComplex.AlexanderWhitneyInput h)
    (s : PublishedPosetSieveInput h)
    (g : PublishedSimplicialGluingInput) (kq : KanQuillenPublishedInput.{0})
    (P : Type) [PartialOrder P] [Finite P] :
    realizationWeakEquivalences (h.categorificationAdjunction.unit.app (nerve P)) := by
…

    Mentions: OAI.Thomason.Construction.RightGrayInput, OAI.Thomason.Construction.SimplexComplex.AlexanderWhitneyInput, OAI.Thomason.Construction.PublishedPosetSieveInput, OAI.Thomason.Construction.PublishedSimplicialGluingInput, OAI.Thomason.Construction.realizationWeakEquivalences

  2. theorem OAI.Thomason.Construction.FiniteReflectionInput.unit_finite_poset line 64

    Source documentation

    The same comparison is weak in every positive finite strict dimension.

    theorem unit_finite_poset
    (G : RightGrayInput h) (t : GrayTruncationInput G)
    (aw : SimplexComplex.AlexanderWhitneyInput h)
    (s : PublishedPosetSieveInput h)
    (g : PublishedSimplicialGluingInput) (kq : KanQuillenPublishedInput.{0})
    (P : Type) [PartialOrder P] [Finite P] :
    realizationWeakEquivalences ((r.categorificationAdjunction h).unit.app (nerve P)) := by
…

    Mentions: OAI.Thomason.Construction.RightGrayInput, OAI.Thomason.Construction.GrayTruncationInput, OAI.Thomason.Construction.SimplexComplex.AlexanderWhitneyInput, OAI.Thomason.Construction.PublishedPosetSieveInput, OAI.Thomason.Construction.PublishedSimplicialGluingInput, OAI.Thomason.Construction.realizationWeakEquivalences

  3. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.finitePosetUnitInput line 92

    Source documentation

    The finite-poset unit comparison follows from the specified simplicial and strict-category inputs.

    theorem finitePosetUnitInput
    (G : RightGrayInput h) (t : GrayTruncationInput G)
    (aw : SimplexComplex.AlexanderWhitneyInput h)
    (s : PublishedPosetSieveInput h)
    (g : PublishedSimplicialGluingInput) (kq : KanQuillenPublishedInput.{0}) :
    PublishedFinitePosetUnitInput h where
…

    Mentions: OAI.Thomason.Construction.RightGrayInput, OAI.Thomason.Construction.GrayTruncationInput, OAI.Thomason.Construction.SimplexComplex.AlexanderWhitneyInput, OAI.Thomason.Construction.PublishedPosetSieveInput, OAI.Thomason.Construction.PublishedSimplicialGluingInput, OAI.Thomason.Construction.PublishedFinitePosetUnitInput

  4. theorem OAI.Thomason.Construction.map_iff_of_unit_components line 122

    Source documentation

    The two unit components, rather than a global unit hypothesis, suffice to compare a map with its image under the endofunctor.

    theorem map_iff_of_unit_components {C : Type*} [Category* C]
    (W : MorphismProperty C) [W.HasTwoOutOfThreeProperty]
    {F : C ⥤ C} (η : 𝟭 C ⟶ F) {X Y : C} (f : X ⟶ Y)
    (hx : W (η.app X)) (hy : W (η.app Y)) : W (F.map f) ↔ W f := by
…
  5. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.finite_poset_map_weakEquivalence_iff line 143

    Source documentation

    Categorification preserves and reflects the actual weak-equivalence property on arbitrary simplicial maps between finite-poset nerves.

    theorem finite_poset_map_weakEquivalence_iff
    (G : RightGrayInput h) (aw : SimplexComplex.AlexanderWhitneyInput h)
    (s : PublishedPosetSieveInput h)
    (g : PublishedSimplicialGluingInput) (kq : KanQuillenPublishedInput.{0})
    {P Q : Type} [PartialOrder P] [PartialOrder Q] [Finite P] [Finite Q]
    (f : nerve P ⟶ nerve Q) :
    h.streetWeakEquivalences (h.categorification.map f) ↔ realizationWeakEquivalences f := by
…

    Mentions: OAI.Thomason.Construction.RightGrayInput, OAI.Thomason.Construction.SimplexComplex.AlexanderWhitneyInput, OAI.Thomason.Construction.PublishedPosetSieveInput, OAI.Thomason.Construction.PublishedSimplicialGluingInput, OAI.Thomason.Construction.realizationWeakEquivalences

  6. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.finite_poset_map_extended_weakEquivalence_iff line 156

    Source documentation

    The same equivalences are detected by the actual Thomason right adjoint Ex²N.

    theorem finite_poset_map_extended_weakEquivalence_iff
    (G : RightGrayInput h) (aw : SimplexComplex.AlexanderWhitneyInput h)
    (s : PublishedPosetSieveInput h)
    (g : PublishedSimplicialGluingInput) (kq : KanQuillenPublishedInput.{0})
    (hj : ∀ X : SSet.{0}, realizationWeakEquivalences (canonicalExtension.app X))
    {P Q : Type} [PartialOrder P] [PartialOrder Q] [Finite P] [Finite Q]
    (f : nerve P ⟶ nerve Q) :
    realizationWeakEquivalences (h.thomasonRight.map (h.categorification.map f)) ↔
      realizationWeakEquivalences f := by
…

    Mentions: OAI.Thomason.Construction.RightGrayInput, OAI.Thomason.Construction.SimplexComplex.AlexanderWhitneyInput, OAI.Thomason.Construction.PublishedPosetSieveInput, OAI.Thomason.Construction.PublishedSimplicialGluingInput, OAI.Thomason.Construction.realizationWeakEquivalences

  7. theorem OAI.Thomason.Construction.FiniteReflectionInput.finite_poset_map_weakEquivalence_iff line 177

    Source documentation

    Finite reflection preserves and reflects these equivalences as well.

    theorem finite_poset_map_weakEquivalence_iff
    (G : RightGrayInput h) (t : GrayTruncationInput G)
    (aw : SimplexComplex.AlexanderWhitneyInput h)
    (s : PublishedPosetSieveInput h)
    (g : PublishedSimplicialGluingInput) (kq : KanQuillenPublishedInput.{0})
    {P Q : Type} [PartialOrder P] [PartialOrder Q] [Finite P] [Finite Q]
    (f : nerve P ⟶ nerve Q) :
    realizationWeakEquivalences ((h.finiteStreetNerve (n + 1)).map
      ((r.categorification h).map f)) ↔ realizationWeakEquivalences f := by
…

    Mentions: OAI.Thomason.Construction.RightGrayInput, OAI.Thomason.Construction.GrayTruncationInput, OAI.Thomason.Construction.SimplexComplex.AlexanderWhitneyInput, OAI.Thomason.Construction.PublishedPosetSieveInput, OAI.Thomason.Construction.PublishedSimplicialGluingInput, OAI.Thomason.Construction.realizationWeakEquivalences

  8. theorem OAI.Thomason.Construction.FiniteReflectionInput.finite_poset_map_extended_weakEquivalence_iff line 192

    Source documentation

    Ex² of the finite Street nerve gives the same test on these maps.

    theorem finite_poset_map_extended_weakEquivalence_iff
    (G : RightGrayInput h) (t : GrayTruncationInput G)
    (aw : SimplexComplex.AlexanderWhitneyInput h)
    (s : PublishedPosetSieveInput h)
    (g : PublishedSimplicialGluingInput) (kq : KanQuillenPublishedInput.{0})
    (hj : ∀ X : SSet.{0}, realizationWeakEquivalences (canonicalExtension.app X))
    {P Q : Type} [PartialOrder P] [PartialOrder Q] [Finite P] [Finite Q]
    (f : nerve P ⟶ nerve Q) :
    realizationWeakEquivalences ((h.finiteStreetNerve (n + 1) ⋙ SSet.ex ⋙ SSet.ex).map
      ((r.categorification h).map f)) ↔ realizationWeakEquivalences f := by
…

    Mentions: OAI.Thomason.Construction.RightGrayInput, OAI.Thomason.Construction.GrayTruncationInput, OAI.Thomason.Construction.SimplexComplex.AlexanderWhitneyInput, OAI.Thomason.Construction.PublishedPosetSieveInput, OAI.Thomason.Construction.PublishedSimplicialGluingInput, OAI.Thomason.Construction.realizationWeakEquivalences

  9. theorem OAI.Thomason.Construction.SieveMap.fiberMap_weak_iff line 234

    Source documentation

    The actual fibre map and the categorified restricted map have the same Street weak-equivalence property.

    theorem fiberMap_weak_iff :
    h.streetWeakEquivalences (fiberMap A B f hf h hA hB) ↔
      h.streetWeakEquivalences (h.posetMap (restriction A B f hf)) := by
…

    Mentions: OAI.Thomason.Construction.SieveMap.fiberMap, OAI.Thomason.Construction.SieveMap.restriction

  10. theorem OAI.Thomason.Construction.SieveMap.fiberMap_weak_iff_nerve line 256

    Source documentation

    For finite posets the full-fibre map is weak exactly when the ordinary restricted poset nerve is a Kan–Quillen weak equivalence.

    theorem fiberMap_weak_iff_nerve [Finite P] [Finite Q]
    (G : RightGrayInput h) (aw : SimplexComplex.AlexanderWhitneyInput h)
    (kq : KanQuillenPublishedInput.{0}) :
    h.streetWeakEquivalences (fiberMap A B f hf h hA hB) ↔
      realizationWeakEquivalences (nerveMap (restriction A B f hf).monotone.functor) :=
…

    Mentions: OAI.Thomason.Construction.RightGrayInput, OAI.Thomason.Construction.SimplexComplex.AlexanderWhitneyInput, OAI.Thomason.Construction.SieveMap.fiberMap, OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.SieveMap.restriction

  11. theorem OAI.Thomason.Construction.RealizedCube.singular_fibration_boundary_lifting line 282

    Source documentation

    A singular Kan fibration which is an actual weak equivalence lifts arbitrary cubical boundary squares in every positive dimension.

    theorem singular_fibration_boundary_lifting (n : ℕ) {X Y : TopCat.{0}}
    (p : X ⟶ Y) [HomotopicalAlgebra.Fibration (TopCat.toSSet.map p)]
    (hp : IsWeakHomotopyEquivalence p.hom) :
    HasLiftingProperty (boundaryInclusion n) p := by
…

    Mentions: OAI.Thomason.Construction.IsWeakHomotopyEquivalence, OAI.Thomason.Construction.RealizedCube.boundaryInclusion

  12. theorem OAI.Thomason.Construction.RealizedCube.singular_acyclic_boundary_lifting line 338

    Source documentation

    The full cubical lifting conclusion under the original singular-realization weak-equivalence hypothesis, with no constant-boundary restriction.

    theorem singular_acyclic_boundary_lifting (n : ℕ) {X Y : TopCat.{0}}
    (p : X ⟶ Y) [HomotopicalAlgebra.Fibration (TopCat.toSSet.map p)]
    (hp : realizationWeakEquivalences (TopCat.toSSet.map p)) :
    HasLiftingProperty (boundaryInclusion n) p :=
…

    Mentions: OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.RealizedCube.boundaryInclusion

  13. def OAI.Thomason.Construction.SimplexPolytopes.cube line 360
  14. def OAI.Thomason.Construction.SimplexPolytopes.simplex line 363
  15. def OAI.Thomason.Construction.SimplexPolytopes.sumMap line 366
  16. theorem OAI.Thomason.Construction.SimplexPolytopes.sumMap_surjective line 371
  17. theorem OAI.Thomason.Construction.SimplexPolytopes.cube_convex line 376
  18. theorem OAI.Thomason.Construction.SimplexPolytopes.simplex_convex line 379
  19. theorem OAI.Thomason.Construction.SimplexPolytopes.cube_closed line 383
  20. theorem OAI.Thomason.Construction.SimplexPolytopes.simplex_closed line 386
  21. theorem OAI.Thomason.Construction.SimplexPolytopes.cube_compact line 389
  22. theorem OAI.Thomason.Construction.SimplexPolytopes.simplex_subset_cube line 392
  23. theorem OAI.Thomason.Construction.SimplexPolytopes.simplex_compact line 397
  24. theorem OAI.Thomason.Construction.SimplexPolytopes.cube_interior line 400
  25. theorem OAI.Thomason.Construction.SimplexPolytopes.simplex_interior line 405
  26. theorem OAI.Thomason.Construction.SimplexPolytopes.cube_interior_nonempty line 417
  27. theorem OAI.Thomason.Construction.SimplexPolytopes.simplex_interior_nonempty line 421
  28. theorem OAI.Thomason.Construction.SimplexPolytopes.exists_pair_homeomorph line 434

    Source documentation

    The ambient radial comparison carries both bodies and their boundaries.

    theorem exists_pair_homeomorph (n : ℕ) :
    ∃ e : (Fin (n+1) → ℝ) ≃ₜ (Fin (n+1) → ℝ),
      e '' simplex n = cube n ∧ e '' frontier (simplex n) = frontier (cube n) := by
…

    Mentions: OAI.Thomason.Construction.SimplexPolytopes.simplex, OAI.Thomason.Construction.SimplexPolytopes.cube

  29. def OAI.Thomason.Construction.SimplexPolytopes.simplexCoordinates line 460

    Source documentation

    Omit the first barycentric coordinate. Its value is recovered by the sum.

    def simplexCoordinates (n : ℕ) : StdSimplex ℝ (Fin (n+2)) ≃ₜ simplex n where
…

    Mentions: OAI.Thomason.Construction.SimplexPolytopes.simplex

  30. def OAI.Thomason.Construction.SimplexPolytopes.cubeCoordinates line 503

    Source documentation

    The product of closed unit intervals is exactly the coordinate box.

    def cubeCoordinates (n : ℕ) : (Fin (n+1) → unitInterval) ≃ₜ cube n where
…

    Mentions: OAI.Thomason.Construction.SimplexPolytopes.cube

  31. theorem OAI.Thomason.Construction.SimplexPolytopes.simplexCoordinates_boundary line 515

    Source documentation

    Barycentric zeros are exactly the topological frontier of the solid simplex.

    theorem simplexCoordinates_boundary (n : ℕ) (s : StdSimplex ℝ (Fin (n+2))) :
    s ∈ RealizationPrism.boundaryLocus (n+1) ↔
      (simplexCoordinates n s).val ∈ frontier (simplex n) := by
…

    Mentions: OAI.Thomason.Construction.RealizationPrism.boundaryLocus, OAI.Thomason.Construction.SimplexPolytopes.simplexCoordinates, OAI.Thomason.Construction.SimplexPolytopes.simplex

  32. theorem OAI.Thomason.Construction.SimplexPolytopes.cubeCoordinates_boundary line 544

    Source documentation

    Endpoint coordinates are exactly the topological frontier of the box.

    theorem cubeCoordinates_boundary (n : ℕ) (u : Fin (n+1) → unitInterval) :
    u ∈ Cube.boundary (Fin (n+1)) ↔
      (cubeCoordinates n u).val ∈ frontier (cube n) := by
…

    Mentions: OAI.Thomason.Construction.SimplexPolytopes.cubeCoordinates, OAI.Thomason.Construction.SimplexPolytopes.cube

  33. def OAI.Thomason.Construction.SimplexPolytopes.ambientHomeomorph line 586
  34. theorem OAI.Thomason.Construction.SimplexPolytopes.ambientHomeomorph_body line 589
  35. theorem OAI.Thomason.Construction.SimplexPolytopes.ambientHomeomorph_boundary line 593
  36. def OAI.Thomason.Construction.SimplexPolytopes.bodyHomeomorph line 597
  37. def OAI.Thomason.Construction.SimplexPolytopes.simplexCubeHomeomorph line 601
  38. theorem OAI.Thomason.Construction.SimplexPolytopes.simplexCubeHomeomorph_boundary line 605
  39. def OAI.Thomason.Construction.SimplexPolytopes.boundaryArrowIso line 621

    Source documentation

    Transport of lifting problems retains the entire boundary on both sides.

    def boundaryArrowIso (n : ℕ) :
    Arrow.mk (RealizationPrism.boundaryInclusion (n+1)) ≅
      Arrow.mk (RealizedCube.boundaryInclusion n) :=
…

    Mentions: OAI.Thomason.Construction.RealizationPrism.boundaryInclusion, OAI.Thomason.Construction.RealizedCube.boundaryInclusion

  40. theorem OAI.Thomason.Construction.singular_fibration_boundary_lifting line 647

    Source documentation

    The full boundary lift from the actual topological weak-equivalence test.

    theorem singular_fibration_boundary_lifting {X Y : TopCat.{0}} (p : X ⟶ Y)
    [HomotopicalAlgebra.Fibration (TopCat.toSSet.map p)]
    (hp : IsWeakHomotopyEquivalence p.hom) (n : ℕ) :
    HasLiftingProperty (SSet.boundary n).ι (TopCat.toSSet.map p) := by
…

    Mentions: OAI.Thomason.Construction.IsWeakHomotopyEquivalence

  41. theorem OAI.Thomason.Construction.singular_fibration_boundary_rlp line 662

    Source documentation

    Actual weak equivalences with singular Kan lifting have the boundary rlp.

    theorem singular_fibration_boundary_rlp {X Y : TopCat.{0}} (p : X ⟶ Y)
    [HomotopicalAlgebra.Fibration (TopCat.toSSet.map p)]
    (hp : IsWeakHomotopyEquivalence p.hom) :
    SSet.modelCategoryQuillen.I.rlp (TopCat.toSSet.map p) := by
…

    Mentions: OAI.Thomason.Construction.IsWeakHomotopyEquivalence

  42. theorem OAI.Thomason.Construction.singular_acyclic_boundary_lifting line 671

    Source documentation

    The actual singular Kan fibration associated to a realization-weak map has the full boundary right lifting property in every simplicial degree.

    theorem singular_acyclic_boundary_lifting {X Y : TopCat.{0}} (p : X ⟶ Y)
    [HomotopicalAlgebra.Fibration (TopCat.toSSet.map p)]
    (hp : realizationWeakEquivalences (TopCat.toSSet.map p)) (n : ℕ) :
    HasLiftingProperty (SSet.boundary n).ι (TopCat.toSSet.map p) := by
…

    Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

  43. theorem OAI.Thomason.Construction.singular_acyclic_boundary_rlp line 685

    Source documentation

    The singular specialization of the acyclic Kan implication, stated for its actual generating boundary class. General simplicial maps remain separate.

    theorem singular_acyclic_boundary_rlp {X Y : TopCat.{0}} (p : X ⟶ Y)
    [HomotopicalAlgebra.Fibration (TopCat.toSSet.map p)]
    (hp : realizationWeakEquivalences (TopCat.toSSet.map p)) :
    SSet.modelCategoryQuillen.I.rlp (TopCat.toSSet.map p) := by
…

    Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

  44. theorem OAI.Thomason.Construction.singular_fibration_weak_iff line 694

    Source documentation

    On actual singular Kan fibrations, singular realization preserves and reflects the topological weak-equivalence test. No counit-W input is used.

    theorem singular_fibration_weak_iff {X Y : TopCat.{0}} (p : X ⟶ Y)
    [HomotopicalAlgebra.Fibration (TopCat.toSSet.map p)] :
    realizationWeakEquivalences (TopCat.toSSet.map p) ↔
      IsWeakHomotopyEquivalence p.hom := by
…

    Mentions: OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.IsWeakHomotopyEquivalence

  45. theorem OAI.Thomason.Construction.singular_fibration_realization_mono_lifting line 705

    Source documentation

    Acyclic singular fibrations lift against every actual realized simplicial monomorphism, keeping the whole prescribed subcomplex map exactly fixed.

    theorem singular_fibration_realization_mono_lifting {X Y : TopCat.{0}} (p : X ⟶ Y)
    [HomotopicalAlgebra.Fibration (TopCat.toSSet.map p)]
    (hp : IsWeakHomotopyEquivalence p.hom) {K L : SSet.{0}} (i : K ⟶ L) [Mono i] :
    HasLiftingProperty (SSet.toTop.map i) p := by
…

    Mentions: OAI.Thomason.Construction.IsWeakHomotopyEquivalence

  46. theorem OAI.Thomason.Construction.singular_fibration_fiber_extension line 733

    Source documentation

    Any map from a realized simplicial subobject to a point fibre of an acyclic singular fibration extends inside that same actual point fibre.

    theorem singular_fibration_fiber_extension {X Y : TopCat.{0}} (p : X ⟶ Y)
    [HomotopicalAlgebra.Fibration (TopCat.toSSet.map p)]
    (hp : IsWeakHomotopyEquivalence p.hom) (y : Y)
    {K L : SSet.{0}} (i : K ⟶ L) [Mono i]
    (a : SSet.toTop.obj K ⟶ TopCat.of {x : X // p.hom x = y}) :
    ∃ g : SSet.toTop.obj L ⟶ TopCat.of {x : X // p.hom x = y},
      SSet.toTop.map i ≫ g = a := by
…

    Mentions: OAI.Thomason.Construction.IsWeakHomotopyEquivalence

  47. def OAI.Thomason.Construction.subdivisionInclusion line 780

    Source documentation

    The subdivision of a subcomplex, mapped to the standard finite-chain nerve.

    def subdivisionInclusion {n : ℕ} (A : (Δ[n] : SSet.{0}).Subcomplex) :
    SSet.sd.obj (A : SSet) ⟶ SimplexCategory.sd.obj ⦋n⦌ :=
…
  48. theorem OAI.Thomason.Construction.subdivisionInclusion_fac line 784
  49. theorem OAI.Thomason.Construction.subdivision_union_mono_range line 793

    Source documentation

    Subdivision assembles a union injectively when its two images meet in the already constructed subdivision of their intersection.

    theorem subdivision_union_mono_range {n : ℕ}
    (A B : (Δ[n] : SSet.{0}).Subcomplex)
    (ha : Mono (subdivisionInclusion A)) (hb : Mono (subdivisionInclusion B))
    (hi : Mono (subdivisionInclusion (A ⊓ B)))
    (he : SSet.Subcomplex.range (subdivisionInclusion (A ⊓ B)) =
      SSet.Subcomplex.range (subdivisionInclusion A) ⊓
        SSet.Subcomplex.range (subdivisionInclusion B)) :
    Mono (subdivisionInclusion (A ⊔ B)) ∧
      SSet.Subcomplex.range (subdivisionInclusion (A ⊔ B)) =
        SSet.Subcomplex.range (subdivisionInclusion A) ⊔
          SSet.Subcomplex.range (subdivisionInclusion B) := by
…

    Mentions: OAI.Thomason.Construction.subdivisionInclusion

  50. def OAI.Thomason.Construction.faceUnion line 817
  51. def OAI.Thomason.Construction.subdividedFaceUnion line 820
  52. theorem OAI.Thomason.Construction.subcomplex_finsetSup_inf line 824
  53. theorem OAI.Thomason.Construction.faceUnion_inter_face line 837
  54. theorem OAI.Thomason.Construction.subdividedFaceUnion_inter_face line 850
  55. theorem OAI.Thomason.Construction.finiteFaceUnion_mono_range_aux line 864
  56. theorem OAI.Thomason.Construction.finiteFaceUnion_mono_range line 916

    Source documentation

    Every finite union of original faces subdivides as the literal union of its finite-chain faces, with an injective comparison to the ambient simplex.

    theorem finiteFaceUnion_mono_range {n : ℕ} (F : Finset (Finset (Fin (n+1)))) :
    Mono (subdivisionInclusion (faceUnion F)) ∧
      SSet.Subcomplex.range (subdivisionInclusion (faceUnion F)) = subdividedFaceUnion F :=
…

    Mentions: OAI.Thomason.Construction.subdivisionInclusion, OAI.Thomason.Construction.faceUnion, OAI.Thomason.Construction.subdividedFaceUnion