ComponentGluing.lean`

43 declarations, 0 contain sorry, 0 declared as axioms

Component

structure OAI.PartitionConsistency.LocalDiagramSystem.Vertex line 15
Source documentation
The source vertex system includes its root equation. Thus its bounded ideal is tied to this actual diagram, not an independently selected poset.
```
structure Vertex (q : Diagram M I) where
…
```
structure OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Arrow line 25
Source documentation
A contraction with its uniquely determined monoid index.
```
structure Arrow (v w : Vertex q) where
…
```
Mentions: OAI.PartitionConsistency.LocalDiagramSystem.Vertex
instance OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Arrow.(instance at line 35) line 35
theorem OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Arrow.index_mul line 42
Source documentation
Equality of the right factors follows from equality of the root diagrams.
```
theorem index_mul (f : Arrow v w) : f.index * w.index = v.index := by
…
```
Mentions: OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Arrow
def OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Arrow.id line 46
def OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Arrow.comp line 57
theorem OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Arrow.between line 68
Source documentation
If two contractions from a vertex have comparable indices, the latter factors uniquely through the former.
```
theorem between (f : Arrow v w) (g : Arrow v z)
    (hle : (show LeftDivOrder M from f.index) ≤ g.index) : Nonempty (Arrow w z) := by
…
```
Mentions: OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Arrow
theorem OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Arrow.eq_of_index_one line 79
Source documentation
There is no nontrivial identity-index contraction.
```
theorem eq_of_index_one (f : Arrow v w) (h : f.index = 1) : v = w := by
…
```
Mentions: OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Arrow
def OAI.PartitionConsistency.LocalDiagramSystem.Vertex.contractAt line 100
Source documentation
The explicit contraction vertex. The right quotient is specified only to avoid a hidden choice; left cancellation makes it unique.
```
def contractAt (v : Vertex q) (n c : M)
    (hn : (show LeftDivOrder M from n) ∈ v.ideal.carrier) (hnc : n*c = v.index) : Vertex q where
…
```
Mentions: OAI.PartitionConsistency.LocalDiagramSystem.Vertex
def OAI.PartitionConsistency.LocalDiagramSystem.Vertex.toContractAt line 107
theorem OAI.PartitionConsistency.LocalDiagramSystem.Vertex.exists_contraction line 116
Source documentation
Every ideal element supplies an actual contraction.
```
theorem exists_contraction (v : Vertex q) (n : M)
    (hn : (show LeftDivOrder M from n) ∈ v.ideal.carrier) :
    ∃ w : Vertex q, ∃ f : Arrow v w, f.index = n := by
…
```
Mentions: OAI.PartitionConsistency.LocalDiagramSystem.Vertex, OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Arrow
theorem OAI.PartitionConsistency.LocalDiagramSystem.Vertex.successors_directed line 123
Source documentation
Finite directedness of successors, from conditional joins of indices.
```
theorem successors_directed (hj : HasConditionalJoins (LeftDivOrder M))
    {v w z : Vertex q} (f : Arrow v w) (g : Arrow v z) :
    ∃ t : Vertex q, Nonempty (Arrow w t) ∧ Nonempty (Arrow z t) := by
…
```
Mentions: OAI.PartitionConsistency.LocalDiagramSystem.Vertex, OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Arrow
def OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Common line 134
Source documentation
Two vertices have a common successor. Directedness will identify this with connectedness in the undirected contraction graph.
```
def Common (v w : Vertex q) : Prop :=
…
```
Mentions: OAI.PartitionConsistency.LocalDiagramSystem.Vertex
theorem OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Common.refl line 139
theorem OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Common.symm line 141
theorem OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Common.trans line 145
theorem OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Common.of_arrow line 151
theorem OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Common.iff_zigzag line 156
Source documentation
Common-successor equivalence is exactly the connected component relation, not a relation identifying more diagrams than finite zigzags do.
```
theorem iff_zigzag (hj : HasConditionalJoins (LeftDivOrder M)) (v w : Vertex q) :
    Common v w ↔ Relation.EqvGen (fun v w : Vertex q => Nonempty (Arrow v w)) v w := by
…
```
Mentions: OAI.PartitionConsistency.LocalDiagramSystem.Vertex, OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Common, OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Arrow
def OAI.PartitionConsistency.LocalDiagramSystem.Vertex.componentSetoid line 171
def OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Component line 176
Source documentation
Components are a quotient of the ground set of actual vertices.
```
def Component (q : Diagram M I) (hj : HasConditionalJoins (LeftDivOrder M)) :=
…
```
theorem OAI.PartitionConsistency.LocalDiagramSystem.Vertex.component_cofinal_chain line 182
Source documentation
A countable cofinal sequence in the bounded ideal yields a countable cofinal chain in the entire component. The target is not limited to the successors of the one initially selected vertex.
```
theorem component_cofinal_chain (hj : HasConditionalJoins (LeftDivOrder M))
    (H : HeightCost (LeftDivOrder M)) (v : Vertex q) :
    ∃ f : ℕ → Vertex q, f 0 = v ∧
      (∀ i j, i ≤ j → Nonempty (Arrow (f i) (f j))) ∧
      (∀ i, Common v (f i)) ∧
      ∀ w, Common v w → ∃ i, Nonempty (Arrow w (f i)) := by
…
```
Mentions: OAI.PartitionConsistency.LocalDiagramSystem.Vertex, OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Arrow, OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Common

theorem OAI.PartitionConsistency.LocalDiagramSystem.System.mem_availability_restrict line 216

Source documentation

Coordinatized form of availability contraction, allowing an equal but not definitionally identical target diagram.

theorem mem_availability_restrict (r s : Diagram M I) (a n c : M)
    (hs : r.sub n = s) (hnc : n*c = a) (y : D.Obj s) (x : LeftDivOrder M) :
    (show LeftDivOrder M from n)*x ∈
      (D.availability r a (D.restrict (show r ≤ s from ⟨n,hs⟩) y)).carrier ↔
      x ∈ (D.availability s c y).carrier := by
…

abbrev OAI.PartitionConsistency.LocalDiagramSystem.System.vertexFiber line 226
Source documentation
The exact fiber at a vertex of the source's contraction graph.
```
abbrev vertexFiber {q : Diagram M I} (v : Vertex q) :=
…
```
Mentions: OAI.PartitionConsistency.LocalDiagramSystem.Vertex
def OAI.PartitionConsistency.LocalDiagramSystem.System.arrowMap line 231
Source documentation
Inclusion along an actual contraction, with its proof that exact availability is preserved.
```
def arrowMap (hj : HasConditionalJoins (LeftDivOrder M))
    {q : Diagram M I} {v w : Vertex q} (f : v.Arrow w)
    (y : D.vertexFiber w) : D.vertexFiber v := by
…
```
Mentions: OAI.PartitionConsistency.LocalDiagramSystem.Vertex
theorem OAI.PartitionConsistency.LocalDiagramSystem.System.arrowMap_val line 252
theorem OAI.PartitionConsistency.LocalDiagramSystem.System.arrowMap_bijective line 257
Source documentation
Every contraction induces a bijection of its actual exact fibers.
```
theorem arrowMap_bijective (hj : HasConditionalJoins (LeftDivOrder M))
    {q : Diagram M I} {v w : Vertex q} (f : v.Arrow w) :
    Function.Bijective (D.arrowMap hj f) := by
…
```
Mentions: OAI.PartitionConsistency.LocalDiagramSystem.Vertex
theorem OAI.PartitionConsistency.LocalDiagramSystem.System.arrowMap_comp line 277
Source documentation
All composition is the literal composition of inclusions. In particular parallel chains cannot independently permute a fiber.
```
theorem arrowMap_comp (hj : HasConditionalJoins (LeftDivOrder M))
    {q : Diagram M I} {v w z : Vertex q} (f : v.Arrow w) (g : w.Arrow z)
    (x : D.vertexFiber z) : D.arrowMap hj f (D.arrowMap hj g x) = D.arrowMap hj (f.comp g) x := by
…
```
Mentions: OAI.PartitionConsistency.LocalDiagramSystem.Vertex
theorem OAI.PartitionConsistency.LocalDiagramSystem.System.arrowMap_id line 283
abbrev OAI.PartitionConsistency.LocalDiagramSystem.System.Point line 303
Source documentation
The disjoint union used for gluing; its summands are the actual exact fibers of the inclusion system.
```
abbrev Point (q : Diagram M I) := Σ w : Vertex q, D.vertexFiber w
```
Mentions: OAI.PartitionConsistency.LocalDiagramSystem.Vertex
def OAI.PartitionConsistency.LocalDiagramSystem.System.Matches line 306
Source documentation
Two representatives agree when compared at a common contraction.
```
def Matches (x y : D.Point q) : Prop :=
…
```
theorem OAI.PartitionConsistency.LocalDiagramSystem.System.Matches.refl line 312
theorem OAI.PartitionConsistency.LocalDiagramSystem.System.Matches.symm line 315
theorem OAI.PartitionConsistency.LocalDiagramSystem.System.Matches.trans line 321
Source documentation
Transitivity uses directedness and surjectivity of the restriction maps; no independent bijections are chosen at vertices.
```
protected theorem trans {x y z : D.Point q}
    (hxy : D.Matches hj x y) (hyz : D.Matches hj y z) : D.Matches hj x z := by
…
```
theorem OAI.PartitionConsistency.LocalDiagramSystem.System.Matches.same line 336
Source documentation
Gluing does not make any two different members of one fiber equal.
```
theorem same (w : Vertex q) (x y : D.vertexFiber w) :
    D.Matches hj ⟨w,x⟩ ⟨w,y⟩ ↔ x = y := by
…
```
Mentions: OAI.PartitionConsistency.LocalDiagramSystem.Vertex
theorem OAI.PartitionConsistency.LocalDiagramSystem.System.Matches.common line 345
abbrev OAI.PartitionConsistency.LocalDiagramSystem.System.ComponentPoint line 354
Source documentation
Representatives in one component, before taking the identification quotient. The selected vertex determines a component, not an additional edge relation or a different family of fibers.
```
abbrev ComponentPoint (root : Vertex q) := {x : D.Point q // Vertex.Common root x.1}
```
Mentions: OAI.PartitionConsistency.LocalDiagramSystem.Vertex, OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Common
def OAI.PartitionConsistency.LocalDiagramSystem.System.gluingSetoid line 356
def OAI.PartitionConsistency.LocalDiagramSystem.System.Glued line 362
Source documentation
The source glued component.
```
def Glued (root : Vertex q) := Quotient (D.gluingSetoid hj root)
```
Mentions: OAI.PartitionConsistency.LocalDiagramSystem.Vertex
def OAI.PartitionConsistency.LocalDiagramSystem.System.toGlued line 364
theorem OAI.PartitionConsistency.LocalDiagramSystem.System.toGlued_injective line 368
Source documentation
Inclusion of each entire fiber is injective.
```
theorem toGlued_injective (root w : Vertex q) (hw : Vertex.Common root w) :
    Function.Injective (D.toGlued hj root w hw) := by
…
```
Mentions: OAI.PartitionConsistency.LocalDiagramSystem.Vertex, OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Common
theorem OAI.PartitionConsistency.LocalDiagramSystem.System.toGlued_surjective line 375
Source documentation
Every representative of the glued set has a unique representative in any specified vertex fiber.
```
theorem toGlued_surjective (root w : Vertex q) (hw : Vertex.Common root w) :
    Function.Surjective (D.toGlued hj root w hw) := by
…
```
Mentions: OAI.PartitionConsistency.LocalDiagramSystem.Vertex, OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Common
def OAI.PartitionConsistency.LocalDiagramSystem.System.fiberEquivGlued line 385
theorem OAI.PartitionConsistency.LocalDiagramSystem.System.toGlued_arrow line 391
Source documentation
The canonical fiber identifications commute with the gluing maps.
```
theorem toGlued_arrow (root w z : Vertex q) (hw : Vertex.Common root w)
    (hz : Vertex.Common root z) (f : w.Arrow z) (x : D.vertexFiber z) :
    D.toGlued hj root w hw (D.arrowMap hj f x) = D.toGlued hj root z hz x := by
…
```
Mentions: OAI.PartitionConsistency.LocalDiagramSystem.Vertex, OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Common