MergerPushouts.lean`

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

MergerPresentation

def OAI.PartitionConsistency.MergerAlgebra.Word.evaluate line 17
Source documentation
Interpretation of an actual merger normal form. New letters are evaluated in their displayed order; the target is an arbitrary monoid.
```
def evaluate (f : M →* N) (g : D → N) : Word M D → N
  | old x => f x
  | snoc x d => evaluate f g x * g d

variable (f : M →* N) (g : D → N)
  (hg : ∀ d x, g (RightFreeAction.act d x) = g d * f x)

include hg in
```
Mentions: OAI.PartitionConsistency.MergerAlgebra.Word
theorem OAI.PartitionConsistency.MergerAlgebra.Word.evaluate_act line 25
theorem OAI.PartitionConsistency.MergerAlgebra.Word.evaluate_mul line 34
def OAI.PartitionConsistency.MergerAlgebra.Word.liftHom line 44
Source documentation
Universal evaluation of merger words for an equivariant interpretation of the quotient of copies.
```
def liftHom : Word M D →* N where
…
```
Mentions: OAI.PartitionConsistency.MergerAlgebra.Word
theorem OAI.PartitionConsistency.MergerAlgebra.Word.liftHom_old line 49
theorem OAI.PartitionConsistency.MergerAlgebra.Word.liftHom_letter line 51
theorem OAI.PartitionConsistency.MergerAlgebra.Word.hom_ext line 59
Source documentation
Old coefficients and the single-letter words generate the extension. This asserts uniqueness in arbitrary target monoids, not just conservative ones.
```
theorem hom_ext (F G : Word M D →* N)
    (ho : ∀ x, F (old x) = G (old x))
    (hn : ∀ d, F (snoc (old 1) d) = G (snoc (old 1) d)) : F = G := by
…
```
Mentions: OAI.PartitionConsistency.MergerAlgebra.Word
def OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.Satisfies line 85
Source documentation
Precisely the finite list of merger relations, interpreted in N. Diagonal entries of start are ignored, as in the definition of Rel. Reflected joins, nonjoins or injectivity are not required in the target.
```
def Satisfies : Prop :=
…
```
theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.satisfies_rel line 91
def OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.interpretedCopy line 110
Source documentation
Interpretation of the actual prescribed quotient, not of a free collection of formal copies.
```
def interpretedCopy : P.Copies hP → N :=
…
```
theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.interpretedCopy_copy line 114
theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.interpretedCopy_act line 117
def OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.presentedLift line 127
Source documentation
The merger normal forms have the universal property of the finite relative monoid presentation used in the countable-base rearrangement.
```
def presentedLift : P.Merger hP →* N :=
…
```
theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.presentedLift_old line 131
theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.presentedLift_root line 134
theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.presentedHom_ext line 142
Source documentation
All normal forms are determined by the old elements and the finitely many roots. This is the uniqueness part needed when comparing reordered presentations.
```
theorem presentedHom_ext (F G : P.Merger hP →* N)
    (ho : ∀ x, F (.old x) = G (.old x))
    (hn : ∀ i, F (P.root hP i) = G (P.root hP i)) : F = G := by
…
```
theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.existsUnique_presentedHom line 154
theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.roots_satisfy line 167
Source documentation
The literal roots satisfy every relation of their relative presentation.
```
theorem roots_satisfy : P.Satisfies MergerAlgebra.Word.oldHom (P.root hP) := by
…
```
Mentions: OAI.PartitionConsistency.MergerAlgebra.Word.oldHom
theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.map_roots_satisfy line 175
Source documentation
Every homomorphism from a merger, with no conservation assumption, necessarily satisfies those relations.
```
theorem map_roots_satisfy (F : P.Merger hP →* N) :
    P.Satisfies (F.comp MergerAlgebra.Word.oldHom) (fun i => F (P.root hP i)) := by
…
```
Mentions: OAI.PartitionConsistency.MergerAlgebra.Word.oldHom
structure OAI.PartitionConsistency.MonoidPushout.IsPushout line 195
def OAI.PartitionConsistency.MonoidPushout.IsPushout.lift line 204
theorem OAI.PartitionConsistency.MonoidPushout.IsPushout.lift_comp_left line 207
theorem OAI.PartitionConsistency.MonoidPushout.IsPushout.lift_comp_right line 211
theorem OAI.PartitionConsistency.MonoidPushout.IsPushout.hom_ext line 216
def OAI.PartitionConsistency.MonoidPushout.IsPushout.equiv line 224
Source documentation
Apexes of two actual pushout squares are isomorphic over both bases.
```
def equiv {E : Type u} [Monoid E] {i' : B →* E} {j' : C →* E}
    (h' : IsPushout f g i' j') : D ≃* E := by
…
```
Mentions: OAI.PartitionConsistency.MonoidPushout.IsPushout
theorem OAI.PartitionConsistency.MonoidPushout.IsPushout.equiv_comp_left line 242
theorem OAI.PartitionConsistency.MonoidPushout.IsPushout.equiv_comp_right line 246
theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.mergerSimulation_root line 262
theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.satisfies_map_iff line 271
theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.mergerSimulation_pushout line 288
Source documentation
Simulating a finite merger is extension of scalars for its literal relative presentation.
```
theorem mergerSimulation_pushout :
    IsPushout (Word.oldHom : A →* P.Merger hP) f
      (P.mergerSimulation hP hA hf)
      (Word.oldHom : B →* (P.map f).Merger (P.valid_map hP hA hf)) where
…
```
Mentions: OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.Merger
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.simulation_pushout line 333
Source documentation
Simulating an indexed probe is a pushout for exactly its countable transition and exit presentation. No universal property is assumed.
```
theorem simulation_pushout :
    IsPushout (Word.oldHom (P.alphabet he) b) f (P.simulation he hf b)
      (Word.oldHom ((P.map f).alphabet
        (fun h => he (hf.injective (h.trans f.map_one.symm)))) (f b)) where
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word.oldHom, OAI.PartitionConsistency.ProbeAlgebra.Path.alphabet
theorem OAI.PartitionConsistency.MonoidPushout.IsPushout.flip line 390
Source documentation
Reflection across the diagonal does not change a pushout.
```
theorem flip {f : A →* B} {g : A →* C} {i : B →* D} {j : C →* D}
    (h : IsPushout f g i j) : IsPushout g f j i where
…
```
Mentions: OAI.PartitionConsistency.MonoidPushout.IsPushout
theorem OAI.PartitionConsistency.MonoidPushout.IsPushout.paste line 399
Source documentation
Two adjoining pushout squares give the outer pushout. In the diagram A → B → E, C → D → F, the two vertical composites are unchanged.
```
theorem paste {f : A →* B} {g : A →* C} {i : B →* D} {j : C →* D}
    {k : B →* E} {l : D →* F} {m : E →* F}
    (h : IsPushout f g i j) (h' : IsPushout k i m l) :
    IsPushout (k.comp f) g m (l.comp j) where
…
```
Mentions: OAI.PartitionConsistency.MonoidPushout.IsPushout
theorem OAI.PartitionConsistency.MonoidPushout.IsPushout.cancel_left line 425
Source documentation
Conversely, if the left square and the outer rectangle are pushouts, then the right square is a pushout. This is the cancellation used after the selected future cells have been moved in front of one omitted cell.
```
theorem cancel_left {f : A →* B} {g : A →* C} {i : B →* D} {j : C →* D}
    {k : B →* E} {l : D →* F} {m : E →* F}
    (h : IsPushout f g i j) (hc : m.comp k = l.comp i)
    (ho : IsPushout (k.comp f) g m (l.comp j)) : IsPushout k i m l where
…
```
Mentions: OAI.PartitionConsistency.MonoidPushout.IsPushout
theorem OAI.PartitionConsistency.MonoidPushout.IsPushout.of_id line 448
Source documentation
The degenerate cell is also a pushout; no generator is added.
```
theorem of_id (f : A →* B) :
    IsPushout (MonoidHom.id A) f f (MonoidHom.id B) where
…
```
Mentions: OAI.PartitionConsistency.MonoidPushout.IsPushout
theorem OAI.PartitionConsistency.MonoidPushout.IsPushout.map_apex line 459
Source documentation
Postcomposing a pushout apex with a fixed monoid isomorphism preserves its full universal property, not just its conservative embeddings.
```
theorem map_apex {f : A →* B} {g : A →* C} {i : B →* D} {j : C →* D}
    (h : IsPushout f g i j) (e : D ≃* E) :
    IsPushout f g (e.toMonoidHom.comp i) (e.toMonoidHom.comp j) where
…
```
Mentions: OAI.PartitionConsistency.MonoidPushout.IsPushout