OAI/SetTheory/PartitionConsistency/Construction/MonoidRounds.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

Schedule

  1. def OAI.PartitionConsistency.MonoidConstruction.ProbeData.map line 17

    Source documentation

    Transport parameters, not profile conclusions, from the starting stage.

    def map (d : ProbeData M) (f : M ⟶ N) : ProbeData N where
…

    Mentions: OAI.PartitionConsistency.MonoidConstruction.ProbeData

  2. theorem OAI.PartitionConsistency.MonoidConstruction.ProbeData.map_a line 23
  3. theorem OAI.PartitionConsistency.MonoidConstruction.ProbeData.map_b line 24
  4. theorem OAI.PartitionConsistency.MonoidConstruction.ProbeData.map_node line 25
  5. def OAI.PartitionConsistency.MonoidConstruction.MergerData.map line 31
  6. abbrev OAI.PartitionConsistency.MonoidConstruction.Request line 39

    Source documentation

    The two actual operations to execute in a round.

    abbrev Request (M : Object.{u}) := ProbeData M ⊕ MergerData M
…

    Mentions: OAI.PartitionConsistency.MonoidConstruction.ProbeData, OAI.PartitionConsistency.MonoidConstruction.MergerData

  7. def OAI.PartitionConsistency.MonoidConstruction.Request.map line 43
  8. def OAI.PartitionConsistency.MonoidConstruction.Request.target line 47
  9. def OAI.PartitionConsistency.MonoidConstruction.Request.inclusion line 51
  10. theorem OAI.PartitionConsistency.MonoidConstruction.Request.cardinal_le line 55
  11. theorem OAI.PartitionConsistency.MonoidConstruction.Request.gates line 61
  12. theorem OAI.PartitionConsistency.MonoidConstruction.Request.preserves_profile line 66
  13. instance OAI.PartitionConsistency.MonoidConstruction.(instance at line 73) line 73
  14. instance OAI.PartitionConsistency.MonoidConstruction.(instance at line 81) line 81
  15. def OAI.PartitionConsistency.MonoidConstruction.Round.step line 93
  16. abbrev OAI.PartitionConsistency.MonoidConstruction.Round.underFunctor line 97
  17. abbrev OAI.PartitionConsistency.MonoidConstruction.Round.functor line 100
  18. def OAI.PartitionConsistency.MonoidConstruction.Round.fromBase line 103

    Source documentation

    Each stage has the same specified conservative map from the round's base.

    def fromBase (j : J) : M ⟶ (functor M schedule).obj j := (underFunctor M schedule).obj j |>.hom

    Mentions: OAI.PartitionConsistency.MonoidConstruction.Round.functor, OAI.PartitionConsistency.MonoidConstruction.Round.underFunctor

  19. theorem OAI.PartitionConsistency.MonoidConstruction.Round.fromBase_naturality line 105
  20. def OAI.PartitionConsistency.MonoidConstruction.Round.botIso line 109
  21. def OAI.PartitionConsistency.MonoidConstruction.Round.succIso line 112
  22. theorem OAI.PartitionConsistency.MonoidConstruction.Round.map_succ line 118
  23. theorem OAI.PartitionConsistency.MonoidConstruction.comp_apply line 136
  24. theorem OAI.PartitionConsistency.MonoidConstruction.identity_apply line 138
  25. def OAI.PartitionConsistency.MonoidConstruction.isoEquiv line 141

    Source documentation

    The underlying equivalence of stages of a construction isomorphism.

    def isoEquiv {M N : Object.{u}} (e : M ≅ N) : M ≃ N where
…
  26. def OAI.PartitionConsistency.MonoidConstruction.PreservesProfiles line 148

    Source documentation

    A genuine property of a transition, not a field assumed at arbitrary limits.

    def PreservesProfiles {M N : Object.{u}} (f : M ⟶ N) : Prop :=
…
  27. theorem OAI.PartitionConsistency.MonoidConstruction.PreservesProfiles.id line 154
  28. theorem OAI.PartitionConsistency.MonoidConstruction.PreservesProfiles.comp line 156
  29. theorem OAI.PartitionConsistency.MonoidConstruction.PreservesProfiles.of_surjective line 161
  30. theorem OAI.PartitionConsistency.MonoidConstruction.PreservesProfiles.of_iso line 165
  31. theorem OAI.PartitionConsistency.MonoidConstruction.PreservesProfiles.operation line 168
  32. theorem OAI.PartitionConsistency.MonoidConstruction.DirectedColimit.exists_rep line 180

    Source documentation

    Any colimit in the stage category is a union of its stages as a monoid.

    theorem exists_rep (y : C.pt) : ∃ i : J, ∃ x : F.obj i, C.ι.app i x = y := by
…
  33. theorem OAI.PartitionConsistency.MonoidConstruction.DirectedColimit.cardinal_le line 191
  34. theorem OAI.PartitionConsistency.MonoidConstruction.DirectedColimit.profile line 197
  35. theorem OAI.PartitionConsistency.MonoidConstruction.ContinuousTower.exists_rep line 221

    Source documentation

    Every tested element at a limit is already present at a strict earlier cut.

    theorem exists_rep {j : J} (hj : Order.IsSuccLimit j) (x : F.obj j) :
    ∃ i : J, ∃ hij : i < j, ∃ a : F.obj i, F.map (homOfLE hij.le) a = x := by
…
  36. theorem OAI.PartitionConsistency.MonoidConstruction.ContinuousTower.preservesProfiles line 229

    Source documentation

    Successor persistence together with continuity proves persistence through arbitrary limits, without supposing that the path belongs to every stage.

    theorem preservesProfiles
    (hsucc : ∀ j, ¬ IsMax j → PreservesProfiles (F.map (homOfLE (Order.le_succ j)))) :
    ∀ (i j : J) (hij : i ≤ j), PreservesProfiles (F.map (homOfLE hij)) := by
…

    Mentions: OAI.PartitionConsistency.MonoidConstruction.PreservesProfiles

  37. theorem OAI.PartitionConsistency.MonoidConstruction.ContinuousTower.cardinal_le line 261

    Source documentation

    Size is bounded by the size of the stage index and the existing operation bounds. The colimit bound is a consequence, not an extra construction input.

    theorem cardinal_le {μ : Cardinal.{u}} (hω : Cardinal.aleph0 ≤ μ) (hJ : Cardinal.mk J ≤ μ)
    (h₀ : Cardinal.mk (F.obj ⊥) ≤ μ)
    (hsucc : ∀ j, ¬ IsMax j → Cardinal.mk (F.obj j) ≤ μ →
      Cardinal.mk (F.obj (Order.succ j)) ≤ μ) (j : J) : Cardinal.mk (F.obj j) ≤ μ := by
…
  38. theorem OAI.PartitionConsistency.MonoidConstruction.ProbeData.probe_gate line 292
  39. theorem OAI.PartitionConsistency.MonoidConstruction.ProbeData.independent line 304

    Source documentation

    A previously inserted probe, not dividing a, meets the next probe in exactly ae. This is why repeated requests give independent cones.

    theorem independent (x : M) (hx : x ∣ d.a * M.e) (hxa : ¬ x ∣ d.a)
    (z : d.extension) : d.inclusion x ∣ z ∧ d.probe ∣ z ↔ d.inclusion (d.a * M.e) ∣ z := by
…
  40. theorem OAI.PartitionConsistency.MonoidConstruction.Request.inclusion_eq_transport line 321
  41. theorem OAI.PartitionConsistency.MonoidConstruction.Round.bot_inv line 331
  42. theorem OAI.PartitionConsistency.MonoidConstruction.Round.preservesProfiles line 336
  43. theorem OAI.PartitionConsistency.MonoidConstruction.Round.fromBase_preservesProfiles line 343
  44. theorem OAI.PartitionConsistency.MonoidConstruction.Round.cardinal_le line 348
  45. theorem OAI.PartitionConsistency.MonoidConstruction.Round.creates_probe line 359

    Source documentation

    Executing a scheduled probe provides a full profile, and a genuinely new element, at every subsequent cut of the round.

    theorem creates_probe (j : J) (hj : ¬ IsMax j) (d : ProbeData M)
    (hd : schedule j = .inl d) (k : J) (hjk : Order.succ j ≤ k) :
    ∃ m : (functor M schedule).obj k,
      ProbeProfile (fromBase M schedule k d.a) (fromBase M schedule k d.b)
        ((functor M schedule).obj k).e m (fun i => fromBase M schedule k (d.path.node i)) ∧
      ¬ ∃ x : (functor M schedule).obj j,
        (functor M schedule).map (homOfLE ((Order.le_succ j).trans hjk)) x = m := by
…

    Mentions: OAI.PartitionConsistency.MonoidConstruction.ProbeData, OAI.PartitionConsistency.MonoidConstruction.Round.functor, OAI.PartitionConsistency.MonoidConstruction.Round.fromBase

  46. def OAI.PartitionConsistency.MonoidConstruction.WellOrdered line 410

    Source documentation

    A chosen well-order on a type of requests; nothing is quotiented or omitted.

    def WellOrdered (A : Type u) := A
…
  47. instance OAI.PartitionConsistency.MonoidConstruction.WellOrdered.(instance at line 413) line 413
  48. instance OAI.PartitionConsistency.MonoidConstruction.WellOrdered.(instance at line 414) line 414
  49. instance OAI.PartitionConsistency.MonoidConstruction.WellOrdered.(instance at line 415) line 415
  50. instance OAI.PartitionConsistency.MonoidConstruction.WellOrdered.(instance at line 416) line 416
  51. instance OAI.PartitionConsistency.MonoidConstruction.WellOrdered.(instance at line 417) line 417
  52. abbrev OAI.PartitionConsistency.MonoidConstruction.ScheduleIndex line 421
  53. instance OAI.PartitionConsistency.MonoidConstruction.(instance at line 422) line 422
  54. instance OAI.PartitionConsistency.MonoidConstruction.(instance at line 423) line 423
  55. def OAI.PartitionConsistency.MonoidConstruction.Request.defaultProbe line 427
  56. instance OAI.PartitionConsistency.MonoidConstruction.Request.(instance at line 432) line 432