OAI/SetTheory/PartitionConsistency/Construction/ConservativeCells.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

ConservativeIntersections

  1. theorem OAI.PartitionConsistency.DiagramOrder.Conservative.map_factor line 21
  2. theorem OAI.PartitionConsistency.DiagramOrder.Conservative.map_join line 31

    Source documentation

    The selected conditional join (or the identity for disjoint cones) is preserved literally by every conservative map of conditional-join monoids.

    theorem map_join (hA : HasConditionalJoins (LeftDivOrder A))
    (hB : HasConditionalJoins (LeftDivOrder B)) (x y : A) :
    f (join x y) = join (f x) (f y) := by
…

    Mentions: OAI.PartitionConsistency.DiagramOrder.HasConditionalJoins, OAI.PartitionConsistency.DiagramOrder.LeftDivOrder

  3. theorem OAI.PartitionConsistency.DiagramOrder.Conservative.of_comp line 49

    Source documentation

    Conservation reflects through a conservative final embedding.

    theorem of_comp {g : B →* C} (hg : Conservative g) (hgf : Conservative (g.comp f)) :
    Conservative f where
…

    Mentions: OAI.PartitionConsistency.DiagramOrder.Conservative

  4. theorem OAI.PartitionConsistency.DiagramOrder.ConservativeHull.conditionalJoins line 78

    Source documentation

    A submonoid closed under the uniquely determined factors and joins has conditional joins of its own.

    theorem conditionalJoins : HasConditionalJoins (LeftDivOrder S) := by
…

    Mentions: OAI.PartitionConsistency.DiagramOrder.HasConditionalJoins, OAI.PartitionConsistency.DiagramOrder.LeftDivOrder

  5. def OAI.PartitionConsistency.ConservativeMonoids.closedObject line 103

    Source documentation

    Closure under factors and ambient joins supplies a genuine object.

    def closedObject (S : Submonoid M)
    (hf : ∀ x ∈ S, ∀ y ∈ S, factor x y ∈ S)
    (hc : ∀ x ∈ S, ∀ y ∈ S, join x y ∈ S) : Object.{u} :=
…
  6. def OAI.PartitionConsistency.ConservativeMonoids.closedInclusion line 108
  7. structure OAI.PartitionConsistency.ConservativeMonoids.Subobject line 115

    Source documentation

    A conservative subobject can equivalently be specified by its carrier submonoid and its two countably-ary closure requirements.

    structure Subobject (M : Object.{u}) where
…
  8. def OAI.PartitionConsistency.ConservativeMonoids.Subobject.object line 122
  9. def OAI.PartitionConsistency.ConservativeMonoids.Subobject.inclusion line 124
  10. def OAI.PartitionConsistency.ConservativeMonoids.Subobject.inf line 128

    Source documentation

    Conservative intersections exist at every original tower cut.

    def inf (S R : Subobject M) : Subobject M where
…

    Mentions: OAI.PartitionConsistency.ConservativeMonoids.Subobject

  11. def OAI.PartitionConsistency.ConservativeMonoids.Subobject.comap line 135

    Source documentation

    Pulling a retained submonoid back to an original stage also preserves all the conservation requirements.

    def comap {N : Object.{u}} (S : Subobject N) (f : M ⟶ N) : Subobject M where
…

    Mentions: OAI.PartitionConsistency.ConservativeMonoids.Subobject

  12. def OAI.PartitionConsistency.ConservativeMonoids.Subobject.range line 147

    Source documentation

    Images of actual conservative maps are conservative subobjects.

    def range {N : Object.{u}} (f : M ⟶ N) : Subobject N where
…

    Mentions: OAI.PartitionConsistency.ConservativeMonoids.Subobject

  13. structure OAI.PartitionConsistency.ConservativeMonoids.Probe line 171
  14. def OAI.PartitionConsistency.ConservativeMonoids.Probe.extension line 182
  15. def OAI.PartitionConsistency.ConservativeMonoids.Probe.inclusion line 188
  16. def OAI.PartitionConsistency.ConservativeMonoids.Probe.generator line 192
  17. def OAI.PartitionConsistency.ConservativeMonoids.Probe.map line 194
  18. def OAI.PartitionConsistency.ConservativeMonoids.Probe.simulation line 198
  19. theorem OAI.PartitionConsistency.ConservativeMonoids.Probe.simulation_inclusion line 202
  20. theorem OAI.PartitionConsistency.ConservativeMonoids.Probe.simulation_generator line 205
  21. theorem OAI.PartitionConsistency.ConservativeMonoids.Probe.pushout line 209
  22. theorem OAI.PartitionConsistency.ConservativeMonoids.Probe.gates line 214
  23. theorem OAI.PartitionConsistency.ConservativeMonoids.Probe.generated line 219

    Source documentation

    An extension is generated by the whole old monoid and its countably many displayed generators. This is proved from the literal presentation.

    theorem generated (S : Submonoid d.extension)
    (ho : ∀ x : M, d.inclusion x ∈ S) (hn : ∀ i, d.generator i ∈ S) : S = ⊤ := by
…
  24. def OAI.PartitionConsistency.ConservativeMonoids.Probe.parameters line 250

    Source documentation

    Only these countably many old elements are needed to specify a probe cell; factors along the path belong to every conservative subobject that contains the displayed endpoints.

    def parameters : Set M := {d.a,d.b,d.e} ∪ Set.range d.path.node
  25. theorem OAI.PartitionConsistency.ConservativeMonoids.Probe.parameters_countable line 252
  26. structure OAI.PartitionConsistency.ConservativeMonoids.Merger line 257
  27. def OAI.PartitionConsistency.ConservativeMonoids.Merger.extension line 265
  28. def OAI.PartitionConsistency.ConservativeMonoids.Merger.inclusion line 271
  29. def OAI.PartitionConsistency.ConservativeMonoids.Merger.generator line 274
  30. def OAI.PartitionConsistency.ConservativeMonoids.Merger.map line 276
  31. def OAI.PartitionConsistency.ConservativeMonoids.Merger.simulation line 279
  32. theorem OAI.PartitionConsistency.ConservativeMonoids.Merger.simulation_inclusion line 283
  33. theorem OAI.PartitionConsistency.ConservativeMonoids.Merger.simulation_generator line 286
  34. theorem OAI.PartitionConsistency.ConservativeMonoids.Merger.pushout line 290
  35. theorem OAI.PartitionConsistency.ConservativeMonoids.Merger.gates line 295
  36. theorem OAI.PartitionConsistency.ConservativeMonoids.Merger.generated line 297
  37. def OAI.PartitionConsistency.ConservativeMonoids.Merger.parameters line 321
  38. theorem OAI.PartitionConsistency.ConservativeMonoids.Merger.parameters_countable line 324
  39. abbrev OAI.PartitionConsistency.ConservativeMonoids.Cell line 337
  40. def OAI.PartitionConsistency.ConservativeMonoids.Cell.extension line 342
  41. def OAI.PartitionConsistency.ConservativeMonoids.Cell.inclusion line 346
  42. def OAI.PartitionConsistency.ConservativeMonoids.Cell.Generators line 350
  43. instance OAI.PartitionConsistency.ConservativeMonoids.Cell.(instance at line 354) line 354
  44. def OAI.PartitionConsistency.ConservativeMonoids.Cell.generator line 356
  45. def OAI.PartitionConsistency.ConservativeMonoids.Cell.parameters line 360
  46. theorem OAI.PartitionConsistency.ConservativeMonoids.Cell.parameters_countable line 364
  47. def OAI.PartitionConsistency.ConservativeMonoids.Cell.map line 369
  48. def OAI.PartitionConsistency.ConservativeMonoids.Cell.simulation line 373
  49. theorem OAI.PartitionConsistency.ConservativeMonoids.Cell.pushout line 377
  50. theorem OAI.PartitionConsistency.ConservativeMonoids.Cell.gates line 384
  51. theorem OAI.PartitionConsistency.ConservativeMonoids.Cell.generated line 389
  52. theorem OAI.PartitionConsistency.ConservativeMonoids.Cell.mem_closure line 395
  53. theorem OAI.PartitionConsistency.ConservativeMonoids.Cell.finite_coefficients line 404

    Source documentation

    The countable list of new generators remains whole, but each particular word uses just finitely many old coefficients. No finite support is claimed for the countable path which specifies the cell.

    theorem finite_coefficients (d : Cell M) (x : d.extension) :
    ∃ s : Finset M, x ∈ Submonoid.closure (d.inclusion '' (s : Set M) ∪ Set.range d.generator) := by
…

    Mentions: OAI.PartitionConsistency.ConservativeMonoids.Cell

  54. def OAI.PartitionConsistency.ConservativeMonoids.RequestCell line 427

    Source documentation

    Forgetting heights takes each executed request to precisely one of the cells above, not to an object merely satisfying the same axioms.

    def RequestCell {M : MonoidConstruction.Object.{u}} :
    MonoidConstruction.Request M → Cell (forgetMargins.obj M)
  | .inl d => .inl ⟨d.a,d.b,M.e,d.b_ne_one,M.e_ne_one,d.path⟩
  | .inr d => .inr ⟨d.n,d.prescription,d.valid⟩

end
end PartitionConsistency.ConservativeMonoids

end OAI

    Mentions: OAI.PartitionConsistency.MonoidConstruction.Request, OAI.PartitionConsistency.ConservativeMonoids.Cell