CellReorder.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

CellUnion

def OAI.PartitionConsistency.ConservativeMonoids.Subobject.directedSup line 18
Source documentation
Directed unions do not add factors or conditional joins.
```
def directedSup {K : Type u} [Nonempty K] (F : K → Subobject T)
    (hF : Directed (· ≤ ·) (fun k => (F k).submonoid)) : Subobject T where
…
```
Mentions: OAI.PartitionConsistency.ConservativeMonoids.Subobject
def OAI.PartitionConsistency.ConservativeMonoids.Subobject.unionValue line 42
theorem OAI.PartitionConsistency.ConservativeMonoids.Subobject.unionValue_at line 48
def OAI.PartitionConsistency.ConservativeMonoids.Subobject.unionLift line 59
Source documentation
A compatible family of arbitrary monoid homomorphisms glues over an actual directed union.
```
def unionLift : U.object →* N where
…
```
theorem OAI.PartitionConsistency.ConservativeMonoids.Subobject.unionLift_comp line 78
theorem OAI.PartitionConsistency.ConservativeMonoids.Subobject.Square.identity line 88
theorem OAI.PartitionConsistency.ConservativeMonoids.Subobject.Square.paste line 91
theorem OAI.PartitionConsistency.ConservativeMonoids.Subobject.Square.cancel_left line 94

theorem OAI.PartitionConsistency.ConservativeMonoids.Subobject.Square.union line 101

Source documentation

The pushout of a fixed base change with a directed union is the union of the actual pushout stages.

theorem union {K : Type u} [Preorder K] [IsDirectedOrder K] [Nonempty K]
    {A C Bup Dup : Subobject T} (B D : K → Subobject T)
    (hB : Monotone (fun k => (B k).submonoid))
    (hD : Monotone (fun k => (D k).submonoid))
    (hBL : ∀ k, (B k).submonoid ≤ Bup.submonoid)
    (hDL : ∀ k, (D k).submonoid ≤ Dup.submonoid)
    (hBU : ∀ x ∈ Bup.submonoid, ∃ k, x ∈ (B k).submonoid)
    (hDU : ∀ x ∈ Dup.submonoid, ∃ k, x ∈ (D k).submonoid)
    (h : ∀ k, Square A (B k) C (D k)) : Square A Bup C Dup := by
…

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

theorem OAI.PartitionConsistency.ConservativeMonoids.CellTower.future_cut line 182
Source documentation
Simulate the selected future cells over any original earlier cut. The result has exactly the union presentation, not a further conservative hull.
```
theorem future_cut (hS : D.Closed S) (a b : J) (hab : a ≤ b) :
    ∃ R : Subobject T, R.submonoid = (D.stage a).submonoid ⊔ (D.restrict S b).submonoid ∧
      Square (D.restrict S a) (D.restrict S b) (D.stage a) R := by
…
```
Mentions: OAI.PartitionConsistency.ConservativeMonoids.Subobject
def OAI.PartitionConsistency.ConservativeMonoids.CellTower.future line 254
Source documentation
The original cut, followed by all its selected future cells.
```
def future (hS : D.Closed S) (a : J) : Subobject T :=
…
```
Mentions: OAI.PartitionConsistency.ConservativeMonoids.Subobject
theorem OAI.PartitionConsistency.ConservativeMonoids.CellTower.future_eq line 257
theorem OAI.PartitionConsistency.ConservativeMonoids.CellTower.future_square line 264
theorem OAI.PartitionConsistency.ConservativeMonoids.CellTower.future_mono line 272
theorem OAI.PartitionConsistency.ConservativeMonoids.CellTower.future_selected line 278
theorem OAI.PartitionConsistency.ConservativeMonoids.CellTower.future_omitted_square line 292
def OAI.PartitionConsistency.ConservativeMonoids.CellTower.reordered line 305
Source documentation
The reordered tower, inside the same T. Its initial submonoid is S whenever S contains the original initial stage.
```
def reordered (hS : D.Closed S) : CellTower T J where
…
```
Mentions: OAI.PartitionConsistency.ConservativeMonoids.CellTower
theorem OAI.PartitionConsistency.ConservativeMonoids.CellTower.reordered_bottom line 339
theorem OAI.PartitionConsistency.ConservativeMonoids.CellTower.countable_reordering line 346
Source documentation
Every countable set is contained in a countable initial base for a reordering by the original two kinds of cells.
```
theorem countable_reordering (hbot : ((D.stage ⊥).submonoid : Set T).Countable)
    (s : Set T) (hs : s.Countable) :
    ∃ E : CellTower T J, ((E.stage ⊥).submonoid : Set T).Countable ∧
      s ⊆ (E.stage ⊥).submonoid := by
…
```
Mentions: OAI.PartitionConsistency.ConservativeMonoids.CellTower