OAI/SetTheory/PartitionConsistency/Models/OrbitAssignments.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PartitionConsistency.ProductForcing.ChainCode.corrected_stable line 30

   Source documentation

   A corrected assignment has the actual permanent ideal at its vertex.

   theorem corrected_stable {d : CohenForcing.Condition I κ} {w : Vertex q}
       {j : labelFiberSet v} {τ : LocalName hμ c w.diagram}
       (h : Corrected hμ c hcard hsize hmerger hj E hE C d w j τ.name) :
       StableAt hμ c hcard hsize hmerger E d w τ.name := by
   …

   Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.LocalName, OAI.PartitionConsistency.ProductForcing.ChainCode.Corrected, OAI.PartitionConsistency.ProductForcing.StableAt

2. theorem OAI.PartitionConsistency.ProductForcing.ChainCode.ordinalCount_mono line 45
3. theorem OAI.PartitionConsistency.ProductForcing.ChainCode.selected_exists line 53
4. theorem OAI.PartitionConsistency.ProductForcing.ChainCode.corrected_total line 61

   Source documentation

   Dense totality, with both the ordinal computations and the selector made at the actual moved condition.

   theorem corrected_total (d : CohenForcing.Condition I κ)
       (hsel : ∀ d : CohenForcing.Condition I κ, ∃ e, e ≤ d ∧ (C.tailData hj).Good e)
       (hcount : ∀ g : G, OrdinalCount hμ c hcard hsize hmerger hj E hE C (g⁻¹ • d))
       (w : Vertex q) (hw : Vertex.Common v w) (j : labelFiberSet v) :
       ∃ e, e ≤ d ∧ ∃ τ : LocalName hμ c w.diagram,
         Corrected hμ c hcard hsize hmerger hj E hE C e w j τ.name := by
   …

   Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.ChainCode.OrdinalCount, OAI.PartitionConsistency.ProductForcing.LocalName, OAI.PartitionConsistency.ProductForcing.ChainCode.Corrected

5. theorem OAI.PartitionConsistency.ProductForcing.ChainCode.corrected_onto line 88

   Source documentation

   Dense surjectivity onto every actual, permanently available local class.

   theorem corrected_onto (d : CohenForcing.Condition I κ)
       (hsel : ∀ d : CohenForcing.Condition I κ, ∃ e, e ≤ d ∧ (C.tailData hj).Good e)
       (hcount : ∀ g : G, OrdinalCount hμ c hcard hsize hmerger hj E hE C (g⁻¹ • d))
       (w : Vertex q) (hw : Vertex.Common v w) (τ : (S).Name)
       (hs : StableAt hμ c hcard hsize hmerger E d w τ) :
       ∃ e, e ≤ d ∧ ∃ j : labelFiberSet v,
         Corrected hμ c hcard hsize hmerger hj E hE C e w j τ := by
   …

   Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.ChainCode.OrdinalCount, OAI.PartitionConsistency.ProductForcing.StableAt, OAI.PartitionConsistency.ProductForcing.ChainCode.Corrected

6. def OAI.PartitionConsistency.LocalDiagramSystem.Vertex.OrbitRel line 136
7. theorem OAI.PartitionConsistency.LocalDiagramSystem.Vertex.OrbitRel.refl line 140
8. theorem OAI.PartitionConsistency.LocalDiagramSystem.Vertex.OrbitRel.symm line 141
9. theorem OAI.PartitionConsistency.LocalDiagramSystem.Vertex.OrbitRel.trans line 144
10. def OAI.PartitionConsistency.LocalDiagramSystem.Vertex.orbitSetoid line 151
11. abbrev OAI.PartitionConsistency.LocalDiagramSystem.Vertex.ComponentOrbit line 155
12. def OAI.PartitionConsistency.LocalDiagramSystem.Vertex.orbit line 157
13. def OAI.PartitionConsistency.LocalDiagramSystem.Vertex.orbitRep line 159
14. theorem OAI.PartitionConsistency.LocalDiagramSystem.Vertex.orbit_rep line 161
15. theorem OAI.PartitionConsistency.LocalDiagramSystem.Vertex.orbit_eq line 164
16. theorem OAI.PartitionConsistency.LocalDiagramSystem.Vertex.orbit_common line 167
17. theorem OAI.PartitionConsistency.LocalDiagramSystem.Vertex.orbit_move line 170
18. def OAI.PartitionConsistency.LocalDiagramSystem.Vertex.orbitChain line 173
19. def OAI.PartitionConsistency.ProductForcing.ChainCode.OrbitAssignment line 202
20. theorem OAI.PartitionConsistency.ProductForcing.ChainCode.orbitAssignment_orbit line 208
21. theorem OAI.PartitionConsistency.ProductForcing.ChainCode.orbitAssignment_label line 214
22. theorem OAI.PartitionConsistency.ProductForcing.ChainCode.orbitAssignment_mono line 224
23. theorem OAI.PartitionConsistency.ProductForcing.ChainCode.orbitAssignment_permute line 232
24. theorem OAI.PartitionConsistency.ProductForcing.ChainCode.orbitAssignment_congr line 240
25. theorem OAI.PartitionConsistency.ProductForcing.ChainCode.orbitAssignment_restrict line 247
26. theorem OAI.PartitionConsistency.ProductForcing.ChainCode.orbitAssignment_descend line 254
27. theorem OAI.PartitionConsistency.ProductForcing.ChainCode.orbitAssignment_stable line 262
28. theorem OAI.PartitionConsistency.ProductForcing.ChainCode.component_difference line 273

    Source documentation

    Two transports to the same component differ by the full stabilizer.

    theorem component_difference (g s : G) (w : Vertex q)
        (hg : Vertex.Common v (g⁻¹ • w)) (hs : Vertex.Common v (s⁻¹ • w)) :
        g⁻¹*s ∈ Vertex.componentStabilizer hj v := by
    …

29. theorem OAI.PartitionConsistency.ProductForcing.ChainCode.orbitAssignment_eq_iff line 282

    Source documentation

    The transport is unambiguous even when its two witnesses use unrelated coordinate permutations. Both injectivity and single-valuedness are retained.

    theorem orbitAssignment_eq_iff {d : CohenForcing.Condition I κ} {w : Vertex q} {j j' : I} {τ σ : (S).Name}
        (h : OrbitAssignment hμ c hcard hsize hmerger hj E hE C d w j τ)
        (h' : OrbitAssignment hμ c hcard hsize hmerger hj E hE C d w j' σ) :
        (S).atomic.EqF ((d,w.diagram) : Poset M I κ) τ σ ↔ j = j' := by
    …

    Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.ChainCode.OrbitAssignment, OAI.PartitionConsistency.ProductForcing.Poset

30. theorem OAI.PartitionConsistency.ProductForcing.ChainCode.orbitAssignment_total_at line 333

    Source documentation

    Totality after transporting to any component in the orbit.

    theorem orbitAssignment_total_at (d : CohenForcing.Condition I κ) (w : Vertex q) (g : G)
        (hw : Vertex.Common v (g⁻¹ • w))
        (hsel : ∀ e : CohenForcing.Condition I κ, ∃ f, f ≤ e ∧ (C.tailData hj).Good f)
        (hcount : ∀ a : Vertex.componentStabilizer hj v,
          OrdinalCount hμ c hcard hsize hmerger hj E hE C (a⁻¹ • (g⁻¹ • d)))
        (j : I) (hjw : j ∈ labelFiberSet w) :
        ∃ e, e ≤ d ∧ ∃ τ : LocalName hμ c w.diagram,
          OrbitAssignment hμ c hcard hsize hmerger hj E hE C e w j τ.name := by
    …

    Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.ChainCode.OrdinalCount, OAI.PartitionConsistency.ProductForcing.LocalName, OAI.PartitionConsistency.ProductForcing.ChainCode.OrbitAssignment

31. theorem OAI.PartitionConsistency.ProductForcing.ChainCode.orbitAssignment_onto_at line 362

    Source documentation

    Surjectivity after orbital transport, still only onto an actual local class with its permanent availability ideal.

    theorem orbitAssignment_onto_at (d : CohenForcing.Condition I κ) (w : Vertex q) (g : G)
        (hw : Vertex.Common v (g⁻¹ • w))
        (hsel : ∀ e : CohenForcing.Condition I κ, ∃ f, f ≤ e ∧ (C.tailData hj).Good f)
        (hcount : ∀ a : Vertex.componentStabilizer hj v,
          OrdinalCount hμ c hcard hsize hmerger hj E hE C (a⁻¹ • (g⁻¹ • d)))
        (τ : (S).Name) (hs : StableAt hμ c hcard hsize hmerger E d w τ) :
        ∃ e, e ≤ d ∧ ∃ j : I,
          OrbitAssignment hμ c hcard hsize hmerger hj E hE C e w j τ := by
    …

    Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.ChainCode.OrdinalCount, OAI.PartitionConsistency.ProductForcing.StableAt, OAI.PartitionConsistency.ProductForcing.ChainCode.OrbitAssignment

32. def OAI.PartitionConsistency.ProductForcing.ChainCode.Assigned line 403

    Source documentation

    The assignment on all vertices, choosing a single chain per orbit of actual components. Its witnesses are local names and literal label indices.

    def Assigned (d : CohenForcing.Condition I κ) (w : Vertex q) (j : I) (τ : (S).Name) : Prop :=
    …

    Mentions: OAI.PartitionConsistency.CohenForcing.Condition

33. theorem OAI.PartitionConsistency.ProductForcing.ChainCode.assigned_label line 409
34. theorem OAI.PartitionConsistency.ProductForcing.ChainCode.assigned_mono line 414
35. theorem OAI.PartitionConsistency.ProductForcing.ChainCode.assigned_permute line 422
36. theorem OAI.PartitionConsistency.ProductForcing.ChainCode.assigned_congr line 429
37. theorem OAI.PartitionConsistency.ProductForcing.ChainCode.assigned_restrict line 436
38. theorem OAI.PartitionConsistency.ProductForcing.ChainCode.assigned_stable line 443
39. theorem OAI.PartitionConsistency.ProductForcing.ChainCode.orbitAssignment_index line 450
40. theorem OAI.PartitionConsistency.ProductForcing.ChainCode.assigned_eq_iff line 457
41. theorem OAI.PartitionConsistency.ProductForcing.ChainCode.assigned_total line 471

    Source documentation

    Uniform count and selector hypotheses give totality on every vertex; there is no orbit omitted from the chosen graph.

    theorem assigned_total (d : CohenForcing.Condition I κ)
        (hsel : ∀ a : Vertex.ComponentOrbit (q := q) hj, ∀ e : CohenForcing.Condition I κ,
    …

    Mentions: OAI.PartitionConsistency.CohenForcing.Condition

42. theorem OAI.PartitionConsistency.ProductForcing.ChainCode.assigned_onto line 491
43. def OAI.PartitionConsistency.LocalDiagramSystem.labelVertex line 523

    Source documentation

    The vertex associated to a literal available label at an extension of q.

    def labelVertex {q : Diagram M I} (r : Diagram M I) (a : M) (ha : r.sub a = q)
        (j : I) (hj : j ∈ r.range) : Vertex q :=
    …

    Mentions: OAI.PartitionConsistency.LocalDiagramSystem.Vertex

44. theorem OAI.PartitionConsistency.LocalDiagramSystem.labelVertex_mem line 527
45. theorem OAI.PartitionConsistency.LocalDiagramSystem.labelVertex_arrow line 533

    Source documentation

    Enlarging a diagram induces the unique contraction carrying the exact label fiber back to its original vertex.

    theorem labelVertex_arrow {q : Diagram M I} (r : Diagram M I) (a : M) (ha : r.sub a = q)
        (w : Vertex q) (hrw : r ≤ w.diagram) (j : I) (hj : j ∈ labelFiberSet w) :
        Nonempty ((labelVertex r a ha j (Diagram.range_antitone hrw (labelFiberSet_subset w hj))).Arrow w) := by
    …

    Mentions: OAI.PartitionConsistency.LocalDiagramSystem.Vertex, OAI.PartitionConsistency.LocalDiagramSystem.labelFiberSet, OAI.PartitionConsistency.LocalDiagramSystem.labelVertex, OAI.PartitionConsistency.LocalDiagramSystem.labelFiberSet_subset

46. theorem OAI.PartitionConsistency.ProductForcing.ChainCode.assigned_ideal line 574
47. theorem OAI.PartitionConsistency.ProductForcing.ChainCode.assigned_at_extension line 585

    Source documentation

    Passing to a stronger diagram uses the actual label availability ideal, so no arbitrary identification between enlarged fibers is made.

    theorem assigned_at_extension {d e : CohenForcing.Condition I κ} {w : Vertex q}
        {j : I} {τ : LocalName hμ c w.diagram}
        (h : Assigned hμ c hcard hsize hmerger hj H E hE d w j τ.name)
        (he : e ≤ d) (r : Diagram M I) (a : M) (ha : r.sub a = q) (hrw : r ≤ w.diagram) :
        Assigned hμ c hcard hsize hmerger hj H E hE e
          (labelVertex r a ha j (Diagram.range_antitone hrw (labelFiberSet_subset w (assigned_label h))))
          j (τ.restrict hrw).name := by
    …

    Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.LocalName, OAI.PartitionConsistency.ProductForcing.ChainCode.Assigned, OAI.PartitionConsistency.ProductForcing.ChainCode.assigned_label

48. theorem OAI.PartitionConsistency.ProductForcing.ChainCode.assigned_compatible_one line 597

    Source documentation

    Compatible graph entries with the same literal label always have the same value, even if they were computed at different diagrams and components.

    theorem assigned_compatible_one {d e f : CohenForcing.Condition I κ} {w z : Vertex q}
        {j : I} {τ : LocalName hμ c w.diagram} {σ : LocalName hμ c z.diagram}
        (h : Assigned hμ c hcard hsize hmerger hj H E hE d w j τ.name)
        (h' : Assigned hμ c hcard hsize hmerger hj H E hE e z j σ.name)
        (hfd : f ≤ d) (hfe : f ≤ e) (r : Diagram M I) (hrw : r ≤ w.diagram) (hrz : r ≤ z.diagram) :
        (S).atomic.EqF ((f,r) : Poset M I κ) τ.name σ.name := by
    …

    Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.LocalName, OAI.PartitionConsistency.ProductForcing.ChainCode.Assigned, OAI.PartitionConsistency.ProductForcing.Poset

49. theorem OAI.PartitionConsistency.ProductForcing.ChainCode.assigned_compatible_inj line 610

    Source documentation

    Equal values at a common extension have equal permanent availability ideals, hence lie in one and the same fiber and have equal labels.

    theorem assigned_compatible_inj {d e f : CohenForcing.Condition I κ} {w z : Vertex q}
        {j k : I} {τ : LocalName hμ c w.diagram} {σ : LocalName hμ c z.diagram}
        (h : Assigned hμ c hcard hsize hmerger hj H E hE d w j τ.name)
        (h' : Assigned hμ c hcard hsize hmerger hj H E hE e z k σ.name)
        (hfd : f ≤ d) (hfe : f ≤ e) (r : Diagram M I) (hrw : r ≤ w.diagram) (hrz : r ≤ z.diagram)
        (heq : (S).atomic.EqF ((f,r) : Poset M I κ) τ.name σ.name) : j = k := by
    …

    Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.LocalName, OAI.PartitionConsistency.ProductForcing.ChainCode.Assigned, OAI.PartitionConsistency.ProductForcing.Poset