OAI/SetTheory/PartitionConsistency/Forcing/Diagrams.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.PartitionConsistency.DiagramForcing.Diagram line 14

   Source documentation

   An actual injective diagram on all of the monoid, with no finite or rank cutoff. Stronger diagrams are the larger diagrams in the translation order.

   structure Diagram (M I : Type u) where
   …

2. instance OAI.PartitionConsistency.DiagramForcing.Diagram.(instance at line 18) line 18
3. theorem OAI.PartitionConsistency.DiagramForcing.Diagram.ext line 19
4. theorem OAI.PartitionConsistency.DiagramForcing.Diagram.injective line 22
5. def OAI.PartitionConsistency.DiagramForcing.Diagram.sub line 26
6. theorem OAI.PartitionConsistency.DiagramForcing.Diagram.sub_apply line 29
7. theorem OAI.PartitionConsistency.DiagramForcing.Diagram.sub_one line 30
8. theorem OAI.PartitionConsistency.DiagramForcing.Diagram.sub_sub line 31
9. theorem OAI.PartitionConsistency.DiagramForcing.Diagram.index_unique line 35
10. def OAI.PartitionConsistency.DiagramForcing.Diagram.range line 39
11. theorem OAI.PartitionConsistency.DiagramForcing.Diagram.range_sub_subset line 41
12. instance OAI.PartitionConsistency.DiagramForcing.Diagram.(instance at line 45) line 45
13. theorem OAI.PartitionConsistency.DiagramForcing.Diagram.le_iff line 59
14. theorem OAI.PartitionConsistency.DiagramForcing.Diagram.range_antitone line 62
15. def OAI.PartitionConsistency.DiagramForcing.Diagram.permute line 68

    Source documentation

    Label permutations act on the entire diagram, not on its monoid positions.

    def permute (π : Equiv.Perm I) (r : Diagram M I) : Diagram M I :=
    …

    Mentions: OAI.PartitionConsistency.DiagramForcing.Diagram

16. theorem OAI.PartitionConsistency.DiagramForcing.Diagram.permute_apply line 72
17. theorem OAI.PartitionConsistency.DiagramForcing.Diagram.permute_one line 75
18. theorem OAI.PartitionConsistency.DiagramForcing.Diagram.permute_mul line 77
19. theorem OAI.PartitionConsistency.DiagramForcing.Diagram.permute_sub line 79
20. theorem OAI.PartitionConsistency.DiagramForcing.Diagram.permute_inv_permute line 83
21. theorem OAI.PartitionConsistency.DiagramForcing.Diagram.permute_permute_inv line 86
22. def OAI.PartitionConsistency.DiagramForcing.Diagram.permuteOrderIso line 90

    Source documentation

    The label action preserves and reflects the forcing order.

    def permuteOrderIso [DiagramOrder.IsConical M] (π : Equiv.Perm I) :
        Diagram M I ≃o Diagram M I where
    …

    Mentions: OAI.PartitionConsistency.DiagramOrder.IsConical, OAI.PartitionConsistency.DiagramForcing.Diagram

23. theorem OAI.PartitionConsistency.DiagramForcing.Diagram.extend_through line 109

    Source documentation

    The distinguished-probe complement bound is exactly what is needed to extend a diagram through e while covering any prescribed μ labels. Source lem:diagram-amalgamation, first part.

    theorem extend_through [Infinite I] (hsize : Cardinal.mk M < Cardinal.mk I) (e : M)
        (he : Cardinal.mk ((Set.range (fun x : M => e * x))ᶜ : Set M) = Cardinal.mk M)
        (p : Diagram M I) {J : Set I} (hJ : Cardinal.mk J ≤ Cardinal.mk M) :
        ∃ r : Diagram M I, sub r e = p ∧ J ⊆ r.range := by
    …

    Mentions: OAI.PartitionConsistency.DiagramForcing.Diagram, OAI.PartitionConsistency.DiagramForcing.Diagram.sub

24. structure OAI.PartitionConsistency.DiagramForcing.OverlapPrescription line 127

    Source documentation

    A finite overlap prescription, before transitive closure. none specifies no overlap; some (a,b) identifies (i,a*x) with (j,b*x) for each x.

    structure OverlapPrescription (M : Type u) (n : ℕ) where
    …

25. def OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.Rel line 133
26. def OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.Valid line 142

    Source documentation

    The indicated pair identifications must already be an equivalence, without adding further overlaps by transitive closure. Equality within a copy is built into Rel.

    def Valid (P : OverlapPrescription M n) : Prop := Equivalence P.Rel

    Mentions: OAI.PartitionConsistency.DiagramForcing.OverlapPrescription

27. theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.rel_same_copy line 144
28. def OAI.PartitionConsistency.DiagramForcing.HasFiniteMergers line 151

    Source documentation

    Precisely the finite-overlap realization property in thm:monoid, item 2. Existence of a monoid having this property is still a separate obligation.

    def HasFiniteMergers (M : Type u) [Monoid M] : Prop :=
    …

29. def OAI.PartitionConsistency.DiagramForcing.Diagram.ExactOverlap line 160

    Source documentation

    The pairwise hypothesis of the diagram amalgamation lemma.

    def ExactOverlap (r s : Diagram M I) : Prop :=
    …

    Mentions: OAI.PartitionConsistency.DiagramForcing.Diagram

30. theorem OAI.PartitionConsistency.DiagramForcing.Diagram.equal_iff_of_common_sub line 164
31. theorem OAI.PartitionConsistency.DiagramForcing.Diagram.exists_overlap_prescription line 180

    Source documentation

    Actual equality of labels gives a valid finite prescription whenever all pairwise range intersections are exact common subdiagrams.

    theorem exists_overlap_prescription {n : ℕ} (s : Fin n → Diagram M I)
        (hs : ∀ i j, i ≠ j → ExactOverlap (s i) (s j)) :
        ∃ P : OverlapPrescription M n, P.Valid ∧ ∀ z w : Fin n × M,
          s z.1 z.2 = s w.1 w.2 ↔ P.Rel z w := by
    …

    Mentions: OAI.PartitionConsistency.DiagramForcing.Diagram, OAI.PartitionConsistency.DiagramForcing.Diagram.ExactOverlap, OAI.PartitionConsistency.DiagramForcing.OverlapPrescription

32. theorem OAI.PartitionConsistency.DiagramForcing.Diagram.amalgamate line 217

    Source documentation

    Source lem:diagram-amalgamation, second part. The extension is an actual embedding on the whole monoid. The prescribed range overlaps are used to invoke the finite-merger property; no amalgamating diagram is a premise.

    theorem amalgamate [Infinite I] (hsize : Cardinal.mk M < Cardinal.mk I)
        (hmerger : HasFiniteMergers M) {n : ℕ} (s : Fin n → Diagram M I)
        (hs : ∀ i j, i ≠ j → ExactOverlap (s i) (s j)) :
        ∃ (r : Diagram M I) (l : Fin n → M), ∀ i, sub r (l i) = s i := by
    …

    Mentions: OAI.PartitionConsistency.DiagramForcing.HasFiniteMergers, OAI.PartitionConsistency.DiagramForcing.Diagram, OAI.PartitionConsistency.DiagramForcing.Diagram.ExactOverlap, OAI.PartitionConsistency.DiagramForcing.Diagram.sub

33. theorem OAI.PartitionConsistency.DiagramForcing.Diagram.common_extension line 245