Semigroup.lean`

53 declarations, 0 contain sorry, 0 declared as axioms

Catalytic orders, ordered group completion, and normalized semigroup states.

theorem OAI.Kaplansky.nsmul_compression_iterate line 26
Source documentation
An order compression of successive multiples iterates without any cancellation assumption.
```
theorem nsmul_compression_iterate (u : S) (m : ℕ)
    (h : (m+1) • u ≤ m • u) : ∀ k : ℕ, (m+k) • u ≤ m • u := by
…
```
theorem OAI.Kaplansky.nsmul_compression_doubles line 41
Source documentation
The ordered-semigroup arithmetic used in MR Theorem 2.3: if a larger multiple of the unit is below a smaller one, some positive multiple is properly infinite in the semigroup sense. No Cuntz correspondence is assumed.
```
theorem nsmul_compression_doubles (u : S) (hu : 0 ≤ u) {m n : ℕ}
    (hmn : m < n) (h : n • u ≤ m • u) :
    ∃ k : ℕ, 0 < k ∧ (2*k) • u ≤ k • u := by
…
```
theorem OAI.Kaplansky.nsmul_unit_order_iff line 57
Source documentation
Absence of a properly infinite positive multiple makes the ordinary natural multiples of the unit order-reflecting. This is the first semigroup step toward quasitrace existence, not that existence theorem.
```
theorem nsmul_unit_order_iff (u : S) (hu : 0 ≤ u)
    (hfinite : ∀ k : ℕ, 0 < k → ¬ (2*k) • u ≤ k • u) (m n : ℕ) :
    m • u ≤ n • u ↔ m ≤ n := by
…
```
def OAI.Kaplansky.unitCyclicMonoid line 68
Source documentation
The ordinary cyclic additive submonoid generated by the order unit.
```
def unitCyclicMonoid (u : S) : AddSubmonoid S where
…
```
def OAI.Kaplansky.cyclicIndex line 75
theorem OAI.Kaplansky.cyclicIndex_spec line 78
theorem OAI.Kaplansky.unit_nsmul_injective line 81
def OAI.Kaplansky.cyclicUnitState line 89
theorem OAI.Kaplansky.cyclicUnitState_nsmul line 104
theorem OAI.Kaplansky.cyclicUnitState_monotone line 110
theorem OAI.Kaplansky.catalytic_nsmul_le line 127
Source documentation
A common summand can be retained while a comparison is iterated. There is no cancellation assumption on the monoid.
```
theorem catalytic_nsmul_le {a b c : S} (h : a + c ≤ b + c) (k : ℕ) :
    k • a + c ≤ k • b + c := by
…
```

theorem OAI.Kaplansky.catalytic_unit_order_iff line 141

Source documentation

A bounded nonnegative common summand cannot hide a compression of unit multiples when every positive multiple fails to be properly infinite.

theorem catalytic_unit_order_iff (u : S) (hu : 0 ≤ u)
    (hf : ∀ k : ℕ, 0 < k → ¬ (2*k) • u ≤ k • u)
    {c : S} (hc : 0 ≤ c) (hcu : ∃ N : ℕ, c ≤ N • u) (m n : ℕ) :
    m • u + c ≤ n • u + c ↔ m ≤ n := by
…

theorem OAI.Kaplansky.stabilized_unit_order_iff line 166

Source documentation

Stabilization by an arbitrary common summand preserves the natural order on the unit if every element is nonnegative and bounded by a unit multiple.

theorem stabilized_unit_order_iff (u : S) (hu : 0 ≤ u)
    (hf : ∀ k : ℕ, 0 < k → ¬ (2*k) • u ≤ k • u)
    (hpos : ∀ c : S, 0 ≤ c) (hbound : ∀ c : S, ∃ N : ℕ, c ≤ N • u)
    (m n : ℕ) :
    (∃ c : S, m • u + c ≤ n • u + c) ↔ m ≤ n := by
…

def OAI.Kaplansky.SemigroupDifference line 183
Source documentation
Formal differences, before identifying order-equivalent pairs.
```
def SemigroupDifference := S × S
```
instance OAI.Kaplansky.(instance at line 185) line 185
def OAI.Kaplansky.SemigroupDifference.Rel line 192
Source documentation
The stabilizing summand records the cancellation which is unavailable in the original monoid.
```
def SemigroupDifference.Rel (a b : SemigroupDifference S) : Prop :=
…
```
Mentions: OAI.Kaplansky.SemigroupDifference
theorem OAI.Kaplansky.SemigroupDifference.rel_refl line 196
theorem OAI.Kaplansky.SemigroupDifference.rel_trans line 198
instance OAI.Kaplansky.(instance at line 205) line 205
theorem OAI.Kaplansky.SemigroupDifference.add_le_add line 210
def OAI.Kaplansky.SemigroupDifference.flip line 218
theorem OAI.Kaplansky.SemigroupDifference.flip_le_flip line 220
abbrev OAI.Kaplansky.SemigroupOrderedGroup line 229
Source documentation
Ordered group completion: order-equivalent differences are identified. This need not embed the original noncancellative monoid injectively.
```
abbrev SemigroupOrderedGroup (S : Type*) [AddCommMonoid S] [PartialOrder S]
    [IsOrderedAddMonoid S] := Antisymmetrization (SemigroupDifference S) (· ≤ ·)
```
Mentions: OAI.Kaplansky.SemigroupDifference
def OAI.Kaplansky.semigroupDifferenceClass line 232
theorem OAI.Kaplansky.semigroupDifferenceClass_le line 235
instance OAI.Kaplansky.(instance at line 240) line 240
instance OAI.Kaplansky.(instance at line 242) line 242
instance OAI.Kaplansky.(instance at line 247) line 247
theorem OAI.Kaplansky.semigroupDifferenceClass_add line 251
theorem OAI.Kaplansky.semigroupDifferenceClass_zero line 254
theorem OAI.Kaplansky.semigroupDifferenceClass_flip line 257
instance OAI.Kaplansky.(instance at line 260) line 260
instance OAI.Kaplansky.(instance at line 289) line 289
def OAI.Kaplansky.semigroupToOrderedGroup line 298
Source documentation
The actual additive map from the monoid into its ordered completion.
```
def semigroupToOrderedGroup : S →+ SemigroupOrderedGroup S where
…
```
Mentions: OAI.Kaplansky.SemigroupOrderedGroup
theorem OAI.Kaplansky.semigroupToOrderedGroup_le_iff line 306
theorem OAI.Kaplansky.semigroupToOrderedGroup_monotone line 311
theorem OAI.Kaplansky.semigroupDifferenceClass_eq_sub line 320
theorem OAI.Kaplansky.semigroupOrderedGroup_exists_difference line 326

theorem OAI.Kaplansky.semigroupOrderedGroup_unit_order line 333

Source documentation

The image of the unit remains order-reflecting on all natural multiples, including after passage to the ordered group quotient.

theorem semigroupOrderedGroup_unit_order (u : S)
    (hf : ∀ k : ℕ, 0 < k → ¬ (2*k) • u ≤ k • u)
    (hpos : ∀ c : S, 0 ≤ c) (hbound : ∀ c : S, ∃ N : ℕ, c ≤ N • u)
    (m n : ℕ) :
    m • semigroupToOrderedGroup u ≤ n • semigroupToOrderedGroup u ↔ m ≤ n := by
…

Mentions: OAI.Kaplansky.semigroupToOrderedGroup

theorem OAI.Kaplansky.semigroupOrderedGroup_unit_nonneg line 341
theorem OAI.Kaplansky.semigroupOrderedGroup_unit_ne_zero line 345
theorem OAI.Kaplansky.semigroupOrderedGroup_order_unit line 355
Source documentation
The original order-unit bound becomes a two-sided bound on every element of the ordered group. No finite generation is needed.
```
theorem semigroupOrderedGroup_order_unit (u : S)
    (hpos : ∀ c : S, 0 ≤ c) (hbound : ∀ c : S, ∃ N : ℕ, c ≤ N • u)
    (x : SemigroupOrderedGroup S) :
    ∃ N : ℕ, -(N • semigroupToOrderedGroup u) ≤ x ∧
      x ≤ N • semigroupToOrderedGroup u := by
…
```
Mentions: OAI.Kaplansky.SemigroupOrderedGroup, OAI.Kaplansky.semigroupToOrderedGroup
theorem OAI.Kaplansky.semigroupDifference_value_mono line 379
def OAI.Kaplansky.semigroupOrderedGroupLift line 390
Source documentation
Every monotone additive map to an ordered group descends to the ordered completion. This constructs the map; it does not postulate a state.
```
def semigroupOrderedGroupLift (f : S →+ G) (hf : Monotone f) : SemigroupOrderedGroup S →+ G where
…
```
Mentions: OAI.Kaplansky.SemigroupOrderedGroup
theorem OAI.Kaplansky.semigroupOrderedGroupLift_apply line 402
theorem OAI.Kaplansky.semigroupOrderedGroupLift_unit line 405
theorem OAI.Kaplansky.semigroupOrderedGroupLift_monotone line 410
theorem OAI.Kaplansky.semigroup_state_iff_orderedGroup_state line 417
theorem OAI.Kaplansky.positive_orderUnit_normalized_state line 434
Source documentation
State construction on a positive ordered commutative monoid with an order unit and no properly infinite positive unit multiple. Cancellation and unperforation are not hypotheses. This is an abstract semigroup theorem, not yet a quasitrace on an algebra.
```
theorem positive_orderUnit_normalized_state (u : S)
    (hpos : ∀ c : S, 0 ≤ c) (hbound : ∀ c : S, ∃ N : ℕ, c ≤ N • u)
    (hf : ∀ k : ℕ, 0 < k → ¬ (2*k) • u ≤ k • u) :
    ∃ f : S →+ ℝ, Monotone f ∧ f u = 1 := by
…
```

theorem OAI.Kaplansky.normalized_semigroup_state_nsmul line 451

Source documentation

Every normalized state has the prescribed cyclic values.

theorem normalized_semigroup_state_nsmul (u : S) (f : S →+ ℝ) (hu : f u = 1) (n : ℕ) :
    f (n • u) = (n : ℝ) := by simp [hu]
…

theorem OAI.Kaplansky.normalized_semigroup_state_no_compression line 457
Source documentation
Conversely a normalized monotone state rules out every properly infinite positive multiple.
```
theorem normalized_semigroup_state_no_compression (u : S) (f : S →+ ℝ)
    (hm : Monotone f) (hu : f u = 1) :
    ∀ k : ℕ, 0 < k → ¬ (2*k) • u ≤ k • u := by
…
```
theorem OAI.Kaplansky.positive_orderUnit_state_iff line 470
Source documentation
Exact abstract state criterion. Applying it to a C*-algebra still requires its actual positive ordered Cuntz semigroup and the analytic dimension-function/quasitrace correspondence.
```
theorem positive_orderUnit_state_iff (u : S)
    (hpos : ∀ c : S, 0 ≤ c) (hbound : ∀ c : S, ∃ N : ℕ, c ≤ N • u) :
    (∃ f : S →+ ℝ, Monotone f ∧ f u = 1) ↔
      ∀ k : ℕ, 0 < k → ¬ (2*k) • u ≤ k • u := by
…
```

theorem OAI.Kaplansky.positive_orderUnit_state_extends_cyclic line 481

Source documentation

The constructed full state extends the already verified initial cyclic state. This explicitly closes the abstract extension step.

theorem positive_orderUnit_state_extends_cyclic (u : S)
    (hpos : ∀ c : S, 0 ≤ c) (hbound : ∀ c : S, ∃ N : ℕ, c ≤ N • u)
    (hf : ∀ k : ℕ, 0 < k → ¬ (2*k) • u ≤ k • u) :
    ∃ f : S →+ ℝ, Monotone f ∧ f u = 1 ∧
      ∀ v : unitCyclicMonoid u, f v = cyclicUnitState u (hpos u) hf v := by
…

Mentions: OAI.Kaplansky.unitCyclicMonoid, OAI.Kaplansky.cyclicUnitState