SaturatedMonoids.lean`

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

SaturationData

theorem OAI.PartitionConsistency.MonoidConstruction._root_.OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.ext line 14
theorem OAI.PartitionConsistency.MonoidConstruction.Saturation.probe_stage line 24
Source documentation
All the parameters of a final probe occur before one complete round. Its comparisons reflect to that stage; they are not separately postulated.
```
theorem probe_stage (d : ProbeData (target M K)) :
    ∃ j : OuterIndex.{u}, j < ⊤ ∧ ∃ d₀ : ProbeData ((tower M K).obj j),
      fromStage M K j d₀.a = d.a ∧ fromStage M K j d₀.b = d.b ∧
        ∀ i, fromStage M K j (d₀.path.node i) = d.path.node i := by
…
```
Mentions: OAI.PartitionConsistency.MonoidConstruction.ProbeData, OAI.PartitionConsistency.MonoidConstruction.Saturation.target, OAI.PartitionConsistency.MonoidConstruction.Saturation.tower, OAI.PartitionConsistency.MonoidConstruction.Saturation.fromStage
def OAI.PartitionConsistency.MonoidConstruction.Saturation.afterRound line 53
Source documentation
Inclusion of the completed successor round into the final union.
```
def afterRound (j : OuterIndex.{u}) (hj : j < ⊤) :
    CompleteRound.target ((tower M K).obj j) K ⟶ target M K :=
…
```
Mentions: OAI.PartitionConsistency.MonoidConstruction.CompleteRound.target, OAI.PartitionConsistency.MonoidConstruction.Saturation.tower, OAI.PartitionConsistency.MonoidConstruction.Saturation.target
theorem OAI.PartitionConsistency.MonoidConstruction.Saturation.inclusion_afterRound line 57
theorem OAI.PartitionConsistency.MonoidConstruction.Saturation.afterRound_preservesProfiles line 65
theorem OAI.PartitionConsistency.MonoidConstruction.Saturation.probes line 72
Source documentation
Saturation for countable paths, including the complete final divisor profile and pairwise exact intersections in the final monoid.
```
theorem probes (d : ProbeData (target M K)) :
    ∃ m : K → target M K, Function.Injective m ∧
      (∀ i, ProbeProfile d.a d.b (target M K).e (m i) d.path.node) ∧
      ∀ i j, i ≠ j → ∀ z : target M K,
        m i ∣ z ∧ m j ∣ z ↔ d.a * (target M K).e ∣ z := by
…
```
Mentions: OAI.PartitionConsistency.MonoidConstruction.ProbeData, OAI.PartitionConsistency.MonoidConstruction.Saturation.target
theorem OAI.PartitionConsistency.MonoidConstruction.Saturation.prescription_stage line 99
Source documentation
Every finite prescription, without a validity restriction, is the image of its actual parameters in a proper stage.
```
theorem prescription_stage {n : ℕ} (P : OverlapPrescription (target M K) n) :
    ∃ j : OuterIndex.{u}, j < ⊤ ∧ ∃ P₀ : OverlapPrescription ((tower M K).obj j) n,
      P₀.map (fromStage M K j).toMonoidHom = P := by
…
```
Mentions: OAI.PartitionConsistency.MonoidConstruction.Saturation.target, OAI.PartitionConsistency.MonoidConstruction.Saturation.tower, OAI.PartitionConsistency.MonoidConstruction.Saturation.fromStage
theorem OAI.PartitionConsistency.MonoidConstruction.Saturation.realizes_prescription line 121
Source documentation
Exact cone realizations persist after all the later rounds, including for right factors which did not exist when the merger was executed.
```
theorem realizes_prescription {n : ℕ} (P : OverlapPrescription (target M K) n)
    (hP : P.Valid) : ∃ l : Fin n → target M K, P.RootSystem l := by
…
```
Mentions: OAI.PartitionConsistency.MonoidConstruction.Saturation.target
theorem OAI.PartitionConsistency.MonoidConstruction.Saturation.finiteMergers line 146
theorem OAI.PartitionConsistency.MonoidConstruction.Saturation.ideal_probes line 153
Source documentation
The final ideal requirement uses all divisors in the final monoid, not only those belonging to the scheduling stage.
```
theorem ideal_probes (a b : target M K) (hb : b ≠ 1)
    (U : ConeIdeal (α := LeftDivOrder (target M K)) a) :
…
```
Mentions: OAI.PartitionConsistency.MonoidConstruction.Saturation.target
theorem OAI.PartitionConsistency.MonoidConstruction.Saturation.complement_probes line 180
Source documentation
The executed probes at a = 1, b = e lie outside the full cone eT.
```
theorem complement_probes : ∃ m : K → target M K,
    Function.Injective m ∧ ∀ i, ¬ (target M K).e ∣ m i := by
…
```
Mentions: OAI.PartitionConsistency.MonoidConstruction.Saturation.target
theorem OAI.PartitionConsistency.MonoidConstruction.Saturation.target_cardinal line 198
theorem OAI.PartitionConsistency.MonoidConstruction.Saturation.complement_cardinal line 206