OAI/SetTheory/PartitionConsistency/Construction/CellCuts.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

CellCut

  1. theorem OAI.PartitionConsistency.MonoidPushout.IsPushout.change_left line 17

    Source documentation

    Replacing the upper-right corner by an isomorphic monoid does not change a presentation pushout.

    theorem change_left {f : A →* B} {g : A →* C} {i : B →* D} {j : C →* D}
    (h : IsPushout f g i j) (e : B ≃* E) :
    IsPushout (e.toMonoidHom.comp f) g (i.comp e.symm.toMonoidHom) j where
…

    Mentions: OAI.PartitionConsistency.MonoidPushout.IsPushout

  2. theorem OAI.PartitionConsistency.ConservativeMonoids.Cell.simulation_old line 52
  3. theorem OAI.PartitionConsistency.ConservativeMonoids.Cell.simulation_generator_range line 55
  4. def OAI.PartitionConsistency.ConservativeMonoids.CellTower.Closed line 66
  5. def OAI.PartitionConsistency.ConservativeMonoids.CellTower.selected line 68
  6. def OAI.PartitionConsistency.ConservativeMonoids.CellTower.restrict line 70
  7. theorem OAI.PartitionConsistency.ConservativeMonoids.CellTower.restrict_le line 73
  8. theorem OAI.PartitionConsistency.ConservativeMonoids.CellTower.restrict_mono line 76
  9. theorem OAI.PartitionConsistency.ConservativeMonoids.CellTower.restrict_omitted line 80
  10. theorem OAI.PartitionConsistency.ConservativeMonoids.CellTower.selected_countable line 86
  11. theorem OAI.PartitionConsistency.ConservativeMonoids.CellTower.selected_dependencies line 94

    Source documentation

    All the parameters and all the countably many generators are retained as soon as one new word of this cell is retained.

    theorem selected_dependencies (hS : D.Closed S) {i : J} (hi : D.selected S i) :
    ∃ h : (D.stage i).submonoid ≠ (D.stage (Order.succ i)).submonoid,
      (D.stepCell i h).parameters ⊆ S.submonoid ∧
        Set.range (D.stepCell i h).generator ⊆ S.submonoid := by
…
  12. theorem OAI.PartitionConsistency.ConservativeMonoids.CellTower.selected_word line 108

    Source documentation

    Every retained new word is still generated by retained old coefficients and the generators of this very same cell.

    theorem selected_word (hS : D.Closed S) {i : J}
    (h : (D.stage i).submonoid ≠ (D.stage (Order.succ i)).submonoid)
    {x : T} (hx : x ∈ S.submonoid) (hi : D.NewAt i x) :
    x ∈ Submonoid.closure ((D.restrict S i).submonoid ∪
      Set.range (D.stepCell i h).generator) := by
…
  13. theorem OAI.PartitionConsistency.ConservativeMonoids.CellTower.restrict_selected line 128

    Source documentation

    A selected successor really is the operation restricted to the retained base. Its inclusion into the original successor is the conservative cell simulation. This theorem includes the full presentation pushout.

    theorem restrict_selected (hS : D.Closed S) {i : J} (hi : D.selected S i) :
    Nonempty (Attachment (D.restrict S i) (D.restrict S (Order.succ i))) ∧
    IsPushout (Subobject.hom (D.restrict_mono S (Order.le_succ i))).toMonoidHom
      (Subobject.hom (D.restrict_le S i)).toMonoidHom
      (Subobject.hom (D.restrict_le S (Order.succ i))).toMonoidHom
      (Subobject.hom (D.mono (Order.le_succ i))).toMonoidHom := by
…

    Mentions: OAI.PartitionConsistency.ConservativeMonoids.Attachment, OAI.PartitionConsistency.ConservativeMonoids.Subobject.hom

  14. def OAI.PartitionConsistency.ConservativeMonoids.Cell.naturalGenerator line 236
  15. theorem OAI.PartitionConsistency.ConservativeMonoids.Cell.hom_ext line 240
  16. theorem OAI.PartitionConsistency.ConservativeMonoids.Cell.simulation_naturalGenerator line 253
  17. def OAI.PartitionConsistency.ConservativeMonoids.Cell.cast line 265
  18. theorem OAI.PartitionConsistency.ConservativeMonoids.Cell.cast_old line 267
  19. theorem OAI.PartitionConsistency.ConservativeMonoids.Cell.cast_naturalGenerator line 270
  20. theorem OAI.PartitionConsistency.ConservativeMonoids.Cell.map_comp line 273
  21. theorem OAI.PartitionConsistency.ConservativeMonoids.Cell.simulation_comp line 294

    Source documentation

    Simulating along two conservative maps is the literal simulation along the composite, after the presentation-theoretic identification.

    theorem simulation_comp (d : Cell M) (f : M ⟶ N) (g : N ⟶ P) :
    (cast (d.map_comp f g)).toMonoidHom.comp
      (((d.map f).simulation g).toMonoidHom.comp (d.simulation f).toMonoidHom) =
      (d.simulation (g.comp f)).toMonoidHom := by
…

    Mentions: OAI.PartitionConsistency.ConservativeMonoids.Cell, OAI.PartitionConsistency.ConservativeMonoids.Cell.cast, OAI.PartitionConsistency.ConservativeMonoids.Cell.simulation

  22. theorem OAI.PartitionConsistency.MonoidPushout.IsPushout.generated line 323
  23. structure OAI.PartitionConsistency.ConservativeMonoids.Subobject.Square line 359

    Source documentation

    A commutative square of actual inclusions which is a pushout among all monoids, not merely among conservative maps.

    structure Square (A B C D : Subobject T) : Prop where
…

    Mentions: OAI.PartitionConsistency.ConservativeMonoids.Subobject

  24. theorem OAI.PartitionConsistency.ConservativeMonoids.Subobject.Square.apex_eq_sup line 371
  25. theorem OAI.PartitionConsistency.ConservativeMonoids.Subobject.Square.flip line 381
  26. theorem OAI.PartitionConsistency.ConservativeMonoids.Subobject.Square.presentationPushout line 383
  27. def OAI.PartitionConsistency.ConservativeMonoids.Subobject.Square.realization line 398

    Source documentation

    The canonical cell base-change is identified with the given apex by its universal property.

    def realization (d : Attachment A B) :
    (d.cell.map (hom h.ac)).extension ≃* D.object :=
…

    Mentions: OAI.PartitionConsistency.ConservativeMonoids.Attachment, OAI.PartitionConsistency.ConservativeMonoids.Subobject.hom

  28. theorem OAI.PartitionConsistency.ConservativeMonoids.Subobject.Square.realization_old line 402
  29. theorem OAI.PartitionConsistency.ConservativeMonoids.Subobject.Square.realization_new line 407
  30. def OAI.PartitionConsistency.ConservativeMonoids.Subobject.Square.attachment line 412
  31. def OAI.PartitionConsistency.ConservativeMonoids.Hom.rangeEquiv line 422

    Source documentation

    A conservative embedding identifies its domain with its actual range.

    def rangeEquiv : M ≃* (Subobject.range f).object := by
…

    Mentions: OAI.PartitionConsistency.ConservativeMonoids.Subobject.range

  32. theorem OAI.PartitionConsistency.ConservativeMonoids.Hom.rangeEquiv_val line 432
  33. theorem OAI.PartitionConsistency.ConservativeMonoids.Subobject.Square.intermediate line 441

    Source documentation

    Intermediate base change stays inside the original successor. Its carrier is exactly the submonoid generated by the intermediate base and the retained successor, not an enlarged conservative hull.

    theorem intermediate (h : Square A B C D) (d : Attachment A B)
    (ha : A.submonoid ≤ E.submonoid) (hc : E.submonoid ≤ C.submonoid) :
    ∃ F : Subobject T, F.submonoid = B.submonoid ⊔ E.submonoid ∧
      F.submonoid ≤ D.submonoid ∧ Nonempty (Attachment E F) ∧ Square A B E F := by
…

    Mentions: OAI.PartitionConsistency.ConservativeMonoids.Subobject.Square, OAI.PartitionConsistency.ConservativeMonoids.Attachment, OAI.PartitionConsistency.ConservativeMonoids.Subobject