OAI/SetTheory/PartitionConsistency/Construction/ConservativeHulls.lean

GitHub source file

67 declarations, 0 contain sorry, 0 declared as axioms

MonoidColimit

  1. def OAI.PartitionConsistency.MonoidConstruction.DirectedColimit.monoidLift line 22

    Source documentation

    Evaluation of a directed union in an arbitrary target monoid.

    def monoidLift (f : ∀ i, F.obj i →* N)
    (hf : ∀ i j h, (f j).comp (transition F i j h) = f i) : object F →* N where
…

    Mentions: OAI.PartitionConsistency.MonoidConstruction.DirectedColimit.transition, OAI.PartitionConsistency.MonoidConstruction.DirectedColimit.object

  2. theorem OAI.PartitionConsistency.MonoidConstruction.DirectedColimit.monoidLift_old line 38
  3. theorem OAI.PartitionConsistency.MonoidConstruction.DirectedColimit.monoidLift_comp_old line 42
  4. theorem OAI.PartitionConsistency.MonoidConstruction.DirectedColimit.monoidHom_ext line 48

    Source documentation

    Every element of the union belongs to a stage, so homomorphisms are uniquely determined on stages, without preservation assumptions on them.

    theorem monoidHom_ext {f g : object F →* N}
    (h : ∀ i, f.comp (old F i) = g.comp (old F i)) : f = g := by
…

    Mentions: OAI.PartitionConsistency.MonoidConstruction.DirectedColimit.object, OAI.PartitionConsistency.MonoidConstruction.DirectedColimit.old

  5. theorem OAI.PartitionConsistency.MonoidConstruction.DirectedColimit.monoidLift_unique line 54
  6. def OAI.PartitionConsistency.MonoidConstruction.DirectedColimit.fromBase line 64

    Source documentation

    A fixed coherent base maps to a directed union independently of the stage used to define the map.

    def fromBase {A : Type v} [Monoid A] (g : ∀ i, A →* F.obj i) : A →* object F :=
…

    Mentions: OAI.PartitionConsistency.MonoidConstruction.DirectedColimit.object

  7. theorem OAI.PartitionConsistency.MonoidConstruction.DirectedColimit.fromBase_eq line 67
  8. def OAI.PartitionConsistency.MonoidConstruction.DirectedColimit.monoidMap line 79

    Source documentation

    The literal map of direct limits induced by a coherent map of stages.

    def monoidMap (G : J ⥤ Object.{u}) (g : ∀ i, F.obj i →* G.obj i)
    (hg : ∀ i j h, (transition G i j h).comp (g i) = (g j).comp (transition F i j h)) :
    object F →* object G :=
…

    Mentions: OAI.PartitionConsistency.MonoidConstruction.DirectedColimit.transition, OAI.PartitionConsistency.MonoidConstruction.DirectedColimit.object

  9. theorem OAI.PartitionConsistency.MonoidConstruction.DirectedColimit.monoidMap_comp_old line 88
  10. theorem OAI.PartitionConsistency.MonoidConstruction.DirectedColimit.pushout_of_stage line 117

    Source documentation

    Pushout presentations commute with the actual directed unions in the construction. In particular, a limit stage of the selected subconstruction has the same presentation whether its cells were attached before or after the fixed base change f.

    theorem pushout_of_stage (h : ∀ i, IsPushout f (a i) (b i) (g i)) :
    IsPushout f (fromBase F a) (fromBase G b) (monoidMap F G g hg) where
…

    Mentions: OAI.PartitionConsistency.MonoidConstruction.DirectedColimit.fromBase, OAI.PartitionConsistency.MonoidConstruction.DirectedColimit.monoidMap

  11. def OAI.PartitionConsistency.CountableHull.stage line 177
  12. def OAI.PartitionConsistency.CountableHull.carrier line 181
  13. theorem OAI.PartitionConsistency.CountableHull.stage_mono line 183
  14. theorem OAI.PartitionConsistency.CountableHull.subset_carrier line 186
  15. theorem OAI.PartitionConsistency.CountableHull.countable line 188
  16. theorem OAI.PartitionConsistency.CountableHull.closed line 197
  17. instance OAI.PartitionConsistency.DiagramOrder.(instance at line 216) line 216
  18. def OAI.PartitionConsistency.DiagramOrder.ConservativeHull.factor line 225

    Source documentation

    The unique right factor when it exists, and 1 otherwise.

    def factor (x y : M) : M := if h : x ∣ y then h.choose else 1
…
  19. theorem OAI.PartitionConsistency.DiagramOrder.ConservativeHull.factor_eq line 228
  20. def OAI.PartitionConsistency.DiagramOrder.ConservativeHull.join line 235

    Source documentation

    The conditional join when it exists, and 1 for a pair with disjoint right cones. There is no completion added to the monoid.

    def join (x y : M) : M :=
…
  21. theorem OAI.PartitionConsistency.DiagramOrder.ConservativeHull.join_spec line 238
  22. theorem OAI.PartitionConsistency.DiagramOrder.ConservativeHull.conservative line 249

    Source documentation

    Closing under right factors and the actual ambient conditional joins is sufficient for all four conservation clauses.

    theorem conservative (hj : HasConditionalJoins (LeftDivOrder M)) (S : Submonoid M)
    (hf : ∀ x ∈ S, ∀ y ∈ S, factor x y ∈ S)
    (hjS : ∀ x ∈ S, ∀ y ∈ S, join x y ∈ S) : Conservative S.subtype where
…

    Mentions: OAI.PartitionConsistency.DiagramOrder.HasConditionalJoins, OAI.PartitionConsistency.DiagramOrder.LeftDivOrder, OAI.PartitionConsistency.DiagramOrder.ConservativeHull.factor, OAI.PartitionConsistency.DiagramOrder.ConservativeHull.join, OAI.PartitionConsistency.DiagramOrder.Conservative

  23. def OAI.PartitionConsistency.DiagramOrder.ConservativeHull.operations line 293
  24. def OAI.PartitionConsistency.DiagramOrder.ConservativeHull.seed line 295
  25. def OAI.PartitionConsistency.DiagramOrder.ConservativeHull.submonoid line 297
  26. theorem OAI.PartitionConsistency.DiagramOrder.ConservativeHull.contains line 303
  27. theorem OAI.PartitionConsistency.DiagramOrder.ConservativeHull.countable line 307
  28. theorem OAI.PartitionConsistency.DiagramOrder.ConservativeHull.closed_deps line 314
  29. theorem OAI.PartitionConsistency.DiagramOrder.ConservativeHull.inclusion_conservative line 320
  30. theorem OAI.PartitionConsistency.DiagramOrder.ConservativeHull.exists_countable_conservative line 332

    Source documentation

    Countable conservative hulls exist inside the same monoid and can be required to contain the countably many dependencies of each retained element. This is not yet the reordering of the original generator/relator schedule.

    theorem exists_countable_conservative (hs : s.Countable) (hd : ∀ x, (deps x).Countable) :
    ∃ S : Submonoid M, (S : Set M).Countable ∧ s ⊆ S ∧
      Conservative S.subtype ∧ ∀ x ∈ S, deps x ⊆ S :=
…

    Mentions: OAI.PartitionConsistency.DiagramOrder.Conservative

  31. instance OAI.PartitionConsistency.DiagramOrder.(instance at line 350) line 350
  32. structure OAI.PartitionConsistency.ConservativeMonoids.Object line 360
  33. instance OAI.PartitionConsistency.ConservativeMonoids.(instance at line 366) line 366
  34. structure OAI.PartitionConsistency.ConservativeMonoids.Hom line 369
  35. instance OAI.PartitionConsistency.ConservativeMonoids.(instance at line 372) line 372
  36. theorem OAI.PartitionConsistency.ConservativeMonoids.Hom.ext line 377
  37. def OAI.PartitionConsistency.ConservativeMonoids.Hom.id line 382
  38. def OAI.PartitionConsistency.ConservativeMonoids.Hom.comp line 383
  39. theorem OAI.PartitionConsistency.ConservativeMonoids.Hom.id_apply line 386
  40. theorem OAI.PartitionConsistency.ConservativeMonoids.Hom.comp_apply line 387
  41. theorem OAI.PartitionConsistency.ConservativeMonoids.Hom.id_comp line 389
  42. theorem OAI.PartitionConsistency.ConservativeMonoids.Hom.comp_id line 390
  43. theorem OAI.PartitionConsistency.ConservativeMonoids.Hom.injective line 392
  44. instance OAI.PartitionConsistency.ConservativeMonoids.(instance at line 395) line 395
  45. instance OAI.PartitionConsistency.ConservativeMonoids.(instance at line 403) line 403
  46. def OAI.PartitionConsistency.ConservativeMonoids.forgetMargins line 405
  47. abbrev OAI.PartitionConsistency.ConservativeMonoids.DirectedColimit.Carrier line 413
  48. def OAI.PartitionConsistency.ConservativeMonoids.DirectedColimit.transition line 415
  49. instance OAI.PartitionConsistency.ConservativeMonoids.DirectedColimit.(instance at line 418) line 418
  50. theorem OAI.PartitionConsistency.ConservativeMonoids.DirectedColimit.conservative line 426
  51. abbrev OAI.PartitionConsistency.ConservativeMonoids.DirectedColimit.Limit line 429
  52. def OAI.PartitionConsistency.ConservativeMonoids.DirectedColimit.old line 431
  53. theorem OAI.PartitionConsistency.ConservativeMonoids.DirectedColimit.old_map line 433
  54. def OAI.PartitionConsistency.ConservativeMonoids.DirectedColimit.object line 437
  55. def OAI.PartitionConsistency.ConservativeMonoids.DirectedColimit.inclusion line 443
  56. def OAI.PartitionConsistency.ConservativeMonoids.DirectedColimit.cocone line 446
  57. def OAI.PartitionConsistency.ConservativeMonoids.DirectedColimit.liftFun line 458
  58. theorem OAI.PartitionConsistency.ConservativeMonoids.DirectedColimit.lift_old line 463
  59. def OAI.PartitionConsistency.ConservativeMonoids.DirectedColimit.liftMonoidHom line 465
  60. theorem OAI.PartitionConsistency.ConservativeMonoids.DirectedColimit.lift_conservative line 480
  61. def OAI.PartitionConsistency.ConservativeMonoids.DirectedColimit.lift line 508
  62. def OAI.PartitionConsistency.ConservativeMonoids.DirectedColimit.isColimit line 510
  63. def OAI.PartitionConsistency.ConservativeMonoids.DirectedColimit.monoidLift line 522

    Source documentation

    The same direct limit has its universal property for all monoid maps, not only maps which preserve divisions and joins.

    def monoidLift (f : ∀ i, F.obj i →* N)
    (hf : ∀ i j h, (f j).comp (transition F i j h) = f i) : object F →* N where
…

    Mentions: OAI.PartitionConsistency.ConservativeMonoids.DirectedColimit.transition, OAI.PartitionConsistency.ConservativeMonoids.DirectedColimit.object

  64. theorem OAI.PartitionConsistency.ConservativeMonoids.DirectedColimit.monoidLift_comp_old line 537
  65. theorem OAI.PartitionConsistency.ConservativeMonoids.DirectedColimit.monoidHom_ext line 541
  66. instance OAI.PartitionConsistency.ConservativeMonoids.(instance at line 549) line 549
  67. instance OAI.PartitionConsistency.ConservativeMonoids.(instance at line 553) line 553