QuotientTransport.lean`

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Transport

theorem OAI.PartitionConsistency.ForcingQuotient.GenericFilter.move_refl line 12
theorem OAI.PartitionConsistency.ForcingQuotient.GenericFilter.move_trans line 17
theorem OAI.PartitionConsistency.ForcingQuotient.GenericFilter.move_symm line 22
def OAI.PartitionConsistency.ProductForcing.LocalName.rebase line 40
Source documentation
Equal supporting diagrams can be identified without changing any name code. This explicit version has a definitionally unchanged underlying name.
```
def LocalName.rebase {r s : Diagram M I} (hrs : r = s) (σ : LocalName hμ c r) :
    LocalName hμ c s := ⟨σ.val,by rw [← hrs]; exact σ.property⟩
```
Mentions: OAI.PartitionConsistency.ProductForcing.LocalName
theorem OAI.PartitionConsistency.ProductForcing.LocalName.rebase_name line 43
def OAI.PartitionConsistency.ProductForcing.LocalName.transportEquiv line 48
Source documentation
Literal name transport is a bijection of the whole ground collection, including the support and normalization requirements.
```
def LocalName.transportEquiv (π : Equiv.Perm I) (r : Diagram M I) :
    LocalName hμ c r ≃ LocalName hμ c (r.permute π) where
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.LocalName
theorem OAI.PartitionConsistency.ProductForcing.local_eq_transport_iff line 65
Source documentation
Equality of local names is preserved and reflected between the original filter and the moved filter. Only actual product-forcing symmetry is used.
```
theorem local_eq_transport_iff (F : GenericFilter (CohenForcing.Condition I κ))
    (π : Equiv.Perm I) (r : Diagram M I) (σ τ : LocalName hμ c r) :
    (localAtomic hμ (r.permute π)).EqG
        (F.move (CohenForcing.Condition.permuteOrderIso π))
        (σ.transport hμ π).name (τ.transport hμ π).name ↔
      (localAtomic hμ r).EqG F σ.name τ.name := by
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.LocalName, OAI.PartitionConsistency.ProductForcing.localAtomic, OAI.PartitionConsistency.CohenForcing.Condition.permuteOrderIso
theorem OAI.PartitionConsistency.ProductForcing.LocalQuotient.transport_ofName line 90
theorem OAI.PartitionConsistency.ProductForcing.LocalQuotient.transport_injective line 95
theorem OAI.PartitionConsistency.ProductForcing.LocalQuotient.transport_surjective line 106
def OAI.PartitionConsistency.ProductForcing.LocalQuotient.transportEquiv line 116
Source documentation
Source (symbolic-transport) is a genuine equivalence, not only a map. It does not assert an automorphism of one fixed interpreted model.
```
def transportEquiv (π : Equiv.Perm I) (r : Diagram M I) :
    LocalQuotient (c := c) hμ F r ≃
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.LocalQuotient
theorem OAI.PartitionConsistency.ProductForcing.LocalQuotient.transport_restrict line 123
Source documentation
Coordinate transport commutes literally with restriction of symbolic names. This is the naturality needed for contraction and gluing.
```
@[simp] theorem transport_restrict (π : Equiv.Perm I) {r s : Diagram M I} (hsr : s ≤ r)
    (x : LocalQuotient (c := c) hμ F r) :
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.LocalQuotient
theorem OAI.PartitionConsistency.ProductForcing.eligibleName_coordinate_transport line 135
Source documentation
Eligibility uses the moved equivalence-relation name and the moved filter; the set of Cohen labels itself is fixed by coordinate permutations.
```
theorem eligibleName_coordinate_transport (F : GenericFilter (CohenForcing.Condition I κ))
    (π : Equiv.Perm I) (r : Diagram M I)
    (E : (system (M := M) (I := I) (κ := κ) hμ).Name) (τ : LocalName hμ c r) :
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.system, OAI.PartitionConsistency.ProductForcing.LocalName
theorem OAI.PartitionConsistency.ProductForcing.eligible_coordinate_transport line 162
def OAI.PartitionConsistency.ProductForcing.eligibleTransportEquiv line 173
Source documentation
Transport of actual eligible classes, without assumptions that an arbitrary model is generic or that E's quotient has chosen representatives.
```
def eligibleTransportEquiv (F : GenericFilter (CohenForcing.Condition I κ))
    (π : Equiv.Perm I) (r : Diagram M I)
    (E : (system (M := M) (I := I) (κ := κ) hμ).Name) :
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.system
structure OAI.PartitionConsistency.LocalDiagramSystem.ReindexIso line 199
Source documentation
A reindexing isomorphism of diagram systems. The compatibility square uses the already-defined literal restriction maps.
```
structure ReindexIso (D : System.{u,v} M I) (E : System.{u,w} M I) (π : Equiv.Perm I) where
…
```
theorem OAI.PartitionConsistency.LocalDiagramSystem.ReindexIso.available_iff line 210
Source documentation
An available local element remains available at exactly the same monoid positions after both its diagram and its name are transported.
```
theorem available_iff (r : Diagram M I) (x : D.Obj r) (n : M) :
    E.Available (r.permute π) (T.app r x) n ↔ D.Available r x n := by
…
```
theorem OAI.PartitionConsistency.LocalDiagramSystem.ReindexIso.availability line 231
Source documentation
Thus the entire availability ideal, not only an individual cofinal sequence, is literally unchanged as a subset of the monoid cone.
```
theorem availability (r : Diagram M I) (a : M) (x : D.Obj r) :
    E.availability (r.permute π) a (T.app r x) = D.availability r a x := by
…
```
def OAI.PartitionConsistency.LocalDiagramSystem.ReindexIso.fiberEquiv line 241
Source documentation
Isomorphism of the actual exact fibers at moved vertices.
```
def fiberEquiv (a : Vertex q) : D.vertexFiber a ≃ E.vertexFiber (g • a) :=
…
```
Mentions: OAI.PartitionConsistency.LocalDiagramSystem.Vertex
theorem OAI.PartitionConsistency.LocalDiagramSystem.ReindexIso.fiberEquiv_val line 247
theorem OAI.PartitionConsistency.LocalDiagramSystem.ReindexIso.fiberEquiv_arrow line 252
Source documentation
Every contraction and its transported contraction give the same map on symbolic elements after transport.
```
theorem fiberEquiv_arrow (hj : HasConditionalJoins (LeftDivOrder M))
    {a b : Vertex q} (f : a.Arrow b) (x : D.vertexFiber b) :
    T.fiberEquiv g a (D.arrowMap hj f x) =
      E.arrowMap hj (f.move g) (T.fiberEquiv g b x) := by
…
```
Mentions: OAI.PartitionConsistency.LocalDiagramSystem.Vertex
def OAI.PartitionConsistency.LocalDiagramSystem.ReindexIso.gluedEquiv line 261
Source documentation
A component equivalence obtained through a root fiber. The independent proof below shows that it agrees with transport at every other vertex.
```
noncomputable def gluedEquiv (hj : HasConditionalJoins (LeftDivOrder M)) (a : Vertex q) :
    D.Glued hj a ≃ E.Glued hj (g • a) :=
…
```
Mentions: OAI.PartitionConsistency.LocalDiagramSystem.Vertex
theorem OAI.PartitionConsistency.LocalDiagramSystem.ReindexIso.gluedEquiv_root line 267
theorem OAI.PartitionConsistency.LocalDiagramSystem.ReindexIso.gluedEquiv_toGlued line 278
Source documentation
Naturality on the whole component. In particular the root-fiber construction of gluedEquiv does not make independent choices at vertices.
```
theorem gluedEquiv_toGlued (hj : HasConditionalJoins (LeftDivOrder M))
    (a b : Vertex q) (hb : Vertex.Common a b) (x : D.vertexFiber b) :
    T.gluedEquiv g hj a (D.toGlued hj a b hb x) =
      E.toGlued hj (g • a) (g • b) (hb.move g) (T.fiberEquiv g b x) := by
…
```
Mentions: OAI.PartitionConsistency.LocalDiagramSystem.Vertex, OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Common
def OAI.PartitionConsistency.ProductForcing.eligibleSystemTransport line 309
Source documentation
The source and target here are the actual systems of eligible classes. Transport of the filter, names and diagrams supplies every axiom of the reindexing isomorphism. Since the permutation fixes q, it fixes E literally.
```
def eligibleSystemTransport [Infinite M] [Infinite I]
    (hcard : Cardinal.mk M ≤ μ) (hsize : Cardinal.mk M < Cardinal.mk I)
    (hmerger : HasFiniteMergers M) (F : GenericFilter (CohenForcing.Condition I κ))
    (q : Diagram M I) (E : (system (M := M) (I := I) (κ := κ) hμ).Name)
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.system
def OAI.PartitionConsistency.LocalDiagramSystem.System.rebaseGlued line 353
Source documentation
Changing the root inside its component changes only the proof that a representative belongs to the component.
```
def rebaseGlued {a b : Vertex q} (hab : Vertex.Common a b) :
    D.Glued hj a ≃ D.Glued hj b where
…
```
Mentions: OAI.PartitionConsistency.LocalDiagramSystem.Vertex, OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Common
theorem OAI.PartitionConsistency.LocalDiagramSystem.System.rebaseGlued_toGlued line 362
theorem OAI.PartitionConsistency.LocalDiagramSystem.System.rebaseGlued_refl line 367
theorem OAI.PartitionConsistency.LocalDiagramSystem.System.rebaseGlued_trans line 372
theorem OAI.PartitionConsistency.LocalDiagramSystem.ReindexIso.gluedEquiv_rebase line 391
Source documentation
Naturality also holds when both chosen roots are changed.
```
theorem gluedEquiv_rebase {a b : Vertex q} (hab : Vertex.Common a b)
    (x : D.Glued hj a) :
    T.gluedEquiv g hj b (D.rebaseGlued hj hab x) =
      E.rebaseGlued hj (hab.move g) (T.gluedEquiv g hj a x) := by
…
```
Mentions: OAI.PartitionConsistency.LocalDiagramSystem.Vertex, OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Common
def OAI.PartitionConsistency.LocalDiagramSystem.ReindexIso.componentEquiv line 401
Source documentation
If g stabilizes the component, transport is an equivalence to the symbolic component at the original chosen root of the moved system.
```
def componentEquiv (a : Vertex q) (ha : Vertex.Common a (g • a)) :
    D.Glued hj a ≃ E.Glued hj a :=
…
```
Mentions: OAI.PartitionConsistency.LocalDiagramSystem.Vertex, OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Common
theorem OAI.PartitionConsistency.LocalDiagramSystem.ReindexIso.componentEquiv_toGlued line 405