NormUltrapower.lean`

22 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.NuclearUltrapower.isUnit_of_star_products line 20
Source documentation
Both-sided approximate-unitarity is essential: no stable-finiteness or Dedekind-finiteness is assumed for the ambient C*-algebra.
```
theorem isUnit_of_star_products {a : A} (hl : IsUnit (star a * a))
    (hr : IsUnit (a * star a)) : IsUnit a := by
…
```
def OAI.NuclearUltrapower.polarUnitary line 40
Source documentation
The polar retraction on the open set of invertible elements.
```
def polarUnitary (a : A) (ha : IsUnit a) : unitary A := by
…
```
theorem OAI.NuclearUltrapower.polarUnitary_value line 61
def OAI.NuclearUltrapower.unitaryReplacement line 66
Source documentation
A unitary-valued extension of polar retraction. Away from invertibles it is set equal to 1.
```
def unitaryReplacement (a : A) : unitary A := by
…
```

theorem OAI.NuclearUltrapower.unitaryReplacement_tendsto line 72

Source documentation

Asymptotically unitary bounded families admit genuine unitary replacements with norm-null difference along any filter.

theorem unitaryReplacement_tendsto {ι : Type*} {l : Filter ι} (a : ι → A)
    (hb : IsBoundedUnder (· ≤ ·) l (fun i => ‖a i‖))
    (hl : Tendsto (fun i => star (a i) * a i) l (𝓝 1))
    (hr : Tendsto (fun i => a i * star (a i)) l (𝓝 1)) :
    Tendsto (fun i => (unitaryReplacement (a i) : A) - a i) l (𝓝 0) := by
…

Mentions: OAI.NuclearUltrapower.unitaryReplacement

theorem OAI.NuclearUltrapower.ultraRel_iff_norm line 104
theorem OAI.NuclearUltrapower.seq_bounded line 109
theorem OAI.NuclearUltrapower.ultraRel_star line 113
def OAI.NuclearUltrapower.normUltrapowerMk line 118
Source documentation
The canonical quotient map, preserving the unit and the complex star algebra.
```
def normUltrapowerMk : BoundedSeq B →⋆ₐ[ℂ] NormUltrapower B ω where
…
```
Mentions: OAI.NuclearUltrapower.BoundedSeq, OAI.NuclearUltrapower.NormUltrapower
def OAI.NuclearUltrapower.boundedUnitarySeq line 129
Source documentation
Every unitary sequence is bounded by one.
```
def boundedUnitarySeq (u : ℕ → unitary B) : BoundedSeq B :=
…
```
Mentions: OAI.NuclearUltrapower.BoundedSeq
theorem OAI.NuclearUltrapower.boundedUnitarySeq_apply line 135
theorem OAI.NuclearUltrapower.normUltrapowerMk_eq_iff line 139
theorem OAI.NuclearUltrapower.normUltrapowerMk_surjective line 145
Source documentation
The defining quotient map is surjective, with no assumed model of the quotient.
```
theorem normUltrapowerMk_surjective : Function.Surjective (normUltrapowerMk B ω) :=
…
```
Mentions: OAI.NuclearUltrapower.normUltrapowerMk
theorem OAI.NuclearUltrapower.unitary_lift line 150
Source documentation
24--36, with both left and right unitarity used. The result requires neither stable finiteness nor separability.
```
theorem unitary_lift (u : unitary (NormUltrapower B ω)) :
    ∃ x : ℕ → unitary B, normUltrapowerMk B ω (boundedUnitarySeq x) = (u : NormUltrapower B ω) := by
…
```
Mentions: OAI.NuclearUltrapower.NormUltrapower, OAI.NuclearUltrapower.normUltrapowerMk, OAI.NuclearUltrapower.boundedUnitarySeq
theorem OAI.NuclearUltrapower.unitary_lift_defects line 170
Source documentation
Coordinatewise lifts preserve each fixed multiplicative relation in the norm ultralimit. No simultaneous coordinate relations or countable intersection of large sets are asserted.
```
theorem unitary_lift_defects {Γ : Type*} [Group Γ]
    (ρ : Γ →* unitary (NormUltrapower B ω)) (x : Γ → ℕ → unitary B)
    (hx : ∀ g, normUltrapowerMk B ω (boundedUnitarySeq (x g)) = (ρ g : NormUltrapower B ω))
    (g h : Γ) :
    Tendsto (fun n => (x g n : B) * (x h n : B) - (x (g * h) n : B))
      (ω : Filter ℕ) (𝓝 0) := by
…
```
Mentions: OAI.NuclearUltrapower.NormUltrapower, OAI.NuclearUltrapower.normUltrapowerMk, OAI.NuclearUltrapower.boundedUnitarySeq

theorem OAI.NuclearUltrapower.exists_unitary_lifts line 182

Source documentation

Choice of unitary lifts, normalized at the group identity.

theorem exists_unitary_lifts {Γ : Type*} [Group Γ]
    (ρ : Γ →* unitary (NormUltrapower B ω)) :
    ∃ x : Γ → ℕ → unitary B, (∀ n, x 1 n = 1) ∧
      (∀ g, normUltrapowerMk B ω (boundedUnitarySeq (x g)) = (ρ g : NormUltrapower B ω)) ∧
      ∀ g h, Tendsto (fun n => (x g n : B) * (x h n : B) - (x (g * h) n : B))
        (ω : Filter ℕ) (𝓝 0) := by
…

Mentions: OAI.NuclearUltrapower.NormUltrapower, OAI.NuclearUltrapower.normUltrapowerMk, OAI.NuclearUltrapower.boundedUnitarySeq

def OAI.NuclearUltrapower.boundedSeqToLp line 214
Source documentation
The two standard bounded-sequence presentations agree coordinatewise.
```
def boundedSeqToLp : BoundedSeq B →⋆ₐ[ℂ] VariableUltra.Seq (fun _ : ℕ => B) where
…
```
Mentions: OAI.NuclearUltrapower.BoundedSeq, OAI.NuclearUltrapower.VariableUltra.Seq
theorem OAI.NuclearUltrapower.boundedSeqToLp_apply line 225
def OAI.NuclearUltrapower.normUltraToCStar line 230
Source documentation
Endow the norm-null ring quotient with its canonical C*-model, without replacing the norm-null ideal by any algebraic relation.
```
def normUltraToCStar : NormUltrapower B ω →⋆ₐ[ℂ] VariableUltra.Algebra (fun _ : ℕ => B) ω where
…
```
Mentions: OAI.NuclearUltrapower.NormUltrapower, OAI.NuclearUltrapower.VariableUltra.Algebra
theorem OAI.NuclearUltrapower.normUltraToCStar_mk line 246
theorem OAI.NuclearUltrapower.normUltraToCStar_injective line 250
theorem OAI.NuclearUltrapower.boundedSeqToLp_unitary line 256