FullGroupAlgebra.lean`

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

def OAI.NuclearUltrapower.GroupStarAlgebra.involutionAdd line 14
Source documentation
Algebraic involution on the complex group ring: conjugate coefficients and invert group elements. This is not the pointwise star on coefficient functions.
```
def involutionAdd : ℂ[Γ] →+ ℂ[Γ] :=
…
```
instance OAI.NuclearUltrapower.GroupStarAlgebra.(instance at line 20) line 20
theorem OAI.NuclearUltrapower.GroupStarAlgebra.star_single line 22
theorem OAI.NuclearUltrapower.GroupStarAlgebra.star_add' line 27
theorem OAI.NuclearUltrapower.GroupStarAlgebra.star_zero' line 30
instance OAI.NuclearUltrapower.GroupStarAlgebra.(instance at line 32) line 32
instance OAI.NuclearUltrapower.GroupStarAlgebra.(instance at line 41) line 41
instance OAI.NuclearUltrapower.GroupStarAlgebra.(instance at line 44) line 44
instance OAI.NuclearUltrapower.GroupStarAlgebra.(instance at line 56) line 56
def OAI.NuclearUltrapower.GroupStarAlgebra.evaluate line 72
Source documentation
A unitary group representation evaluates finite linear combinations.
```
def evaluate (ρ : Γ →* unitary D) : ℂ[Γ] →⋆ₐ[ℂ] D where
…
```
theorem OAI.NuclearUltrapower.GroupStarAlgebra.evaluate_single line 84
def OAI.NuclearUltrapower.GroupStarAlgebra.modelNormSet line 95
Source documentation
The possible operator norms in all unital C*-models of the group.
```
def modelNormSet (x : ℂ[Γ]) : Set ℝ :=
…
```
theorem OAI.NuclearUltrapower.GroupStarAlgebra.modelNormSet_nonempty line 98
theorem OAI.NuclearUltrapower.GroupStarAlgebra.models_bounded line 102
Source documentation
Every finite group-ring expression is bounded uniformly over ALL models.
```
theorem models_bounded (x : ℂ[Γ]) :
    ∃ M : ℝ, 0 ≤ M ∧ ∀ (D : Type) [CStarAlgebra D] (ρ : Γ →* unitary D), ‖evaluate ρ x‖ ≤ M := by
…
```
Mentions: OAI.NuclearUltrapower.GroupStarAlgebra.evaluate
theorem OAI.NuclearUltrapower.GroupStarAlgebra.modelNormSet_bdd line 126
def OAI.NuclearUltrapower.GroupStarAlgebra.universalNorm line 133
Source documentation
The full, not the reduced, universal C*-seminorm.
```
def universalNorm (x : ℂ[Γ]) : ℝ := sSup (modelNormSet x)
```
Mentions: OAI.NuclearUltrapower.GroupStarAlgebra.modelNormSet
theorem OAI.NuclearUltrapower.GroupStarAlgebra.model_norm_le line 135
theorem OAI.NuclearUltrapower.GroupStarAlgebra.universalNorm_le line 139
theorem OAI.NuclearUltrapower.GroupStarAlgebra.universalNorm_nonneg line 146
theorem OAI.NuclearUltrapower.GroupStarAlgebra.universalNorm_zero line 149
def OAI.NuclearUltrapower.GroupStarAlgebra.universalSeminorm line 156
Source documentation
The universal model supremum is a submultiplicative seminorm.
```
def universalSeminorm : RingSeminorm ℂ[Γ] where
…
```
instance OAI.NuclearUltrapower.GroupStarAlgebra.(instance at line 182) line 182
theorem OAI.NuclearUltrapower.GroupStarAlgebra.norm_eq_universalNorm line 184
instance OAI.NuclearUltrapower.GroupStarAlgebra.(instance at line 186) line 186
instance OAI.NuclearUltrapower.GroupStarAlgebra.(instance at line 192) line 192
theorem OAI.NuclearUltrapower.GroupStarAlgebra.norm_mul_self_le line 200
Source documentation
C*-identity at the seminorm level, which survives separated completion.
```
theorem norm_mul_self_le (x : ℂ[Γ]) : ‖x‖ * ‖x‖ ≤ ‖star x * x‖ := by
…
```
theorem OAI.NuclearUltrapower.GroupStarAlgebra.evaluate_continuous line 210
Source documentation
Every model evaluation is contractive for the universal seminorm.
```
theorem evaluate_continuous {D : Type} [CStarAlgebra D] (ρ : Γ →* unitary D) :
    Continuous (evaluate ρ) := by
…
```
Mentions: OAI.NuclearUltrapower.GroupStarAlgebra.evaluate
instance OAI.NuclearUltrapower.UniversalCompletion.completionStar line 225
theorem OAI.NuclearUltrapower.UniversalCompletion.star_coe line 227
instance OAI.NuclearUltrapower.UniversalCompletion.completionContinuousStar line 230
instance OAI.NuclearUltrapower.UniversalCompletion.completionInvolutiveStar line 233
instance OAI.NuclearUltrapower.UniversalCompletion.completionStarRing line 239
instance OAI.NuclearUltrapower.UniversalCompletion.completionNormedStar line 249
instance OAI.NuclearUltrapower.UniversalCompletion.completionNormedAlgebra line 257
instance OAI.NuclearUltrapower.UniversalCompletion.completionStarModule line 260
def OAI.NuclearUltrapower.UniversalCompletion.cstarAlgebra line 270
Source documentation
The separated completion of a C*-seminormed star algebra is a C*-algebra.
```
@[instance_reducible] def cstarAlgebra (hc : ∀ x : R, ‖x‖ * ‖x‖ ≤ ‖star x * x‖) : CStarAlgebra (Completion R) where
…
```
def OAI.NuclearUltrapower.UniversalCompletion.inclusion line 277
Source documentation
The canonical, dense star algebra map to the universal completion.
```
def inclusion : R →⋆ₐ[ℂ] Completion R where
…
```
def OAI.NuclearUltrapower.UniversalCompletion.extend line 287
Source documentation
Any continuous model map extends uniquely over the completed algebra.
```
def extend {D : Type*} [CStarAlgebra D] (f : R →⋆ₐ[ℂ] D) (hf : Continuous f) :
    Completion R →⋆ₐ[ℂ] D where
…
```
theorem OAI.NuclearUltrapower.UniversalCompletion.extend_coe line 306
def OAI.NuclearUltrapower.FullGroupModel.Full line 319
Source documentation
A separated completion in the supremum over all unitary models.
```
def Full := Completion ℂ[Γ]
```
instance OAI.NuclearUltrapower.FullGroupModel.(instance at line 321) line 321
def OAI.NuclearUltrapower.FullGroupModel.algebraicInclusion line 324
def OAI.NuclearUltrapower.FullGroupModel.generator line 327
Source documentation
The canonical group generators are unitaries in the full completion.
```
def generator (g : Γ) : unitary (Full Γ) :=
…
```
Mentions: OAI.NuclearUltrapower.FullGroupModel.Full
def OAI.NuclearUltrapower.FullGroupModel.inclusion line 338
theorem OAI.NuclearUltrapower.FullGroupModel.inclusion_coe line 350
def OAI.NuclearUltrapower.FullGroupModel.modelMap line 354
Source documentation
Extension to every model, not merely to Hilbert-space models.
```
def modelMap {D : Type} [CStarAlgebra D] (ρ : Γ →* unitary D) : Full Γ →⋆ₐ[ℂ] D :=
…
```
Mentions: OAI.NuclearUltrapower.FullGroupModel.Full
theorem OAI.NuclearUltrapower.FullGroupModel.modelMap_coe line 357
theorem OAI.NuclearUltrapower.FullGroupModel.modelMap_generator line 361
instance OAI.NuclearUltrapower.FullGroupModel.(instance at line 365) line 365
theorem OAI.NuclearUltrapower.FullGroupModel.dense_span line 372
Source documentation
The linear span, not just the algebra generated by the generators, is dense.
```
theorem dense_span : Dense (Submodule.span ℂ (Set.range (fun g => (inclusion Γ g : Full Γ))) : Set (Full Γ)) := by
…
```
Mentions: OAI.NuclearUltrapower.FullGroupModel.inclusion, OAI.NuclearUltrapower.FullGroupModel.Full
theorem OAI.NuclearUltrapower.FullGroupModel.modelMap_unique line 384
Source documentation
Uniqueness is proved from continuity and dense generation.
```
theorem modelMap_unique {D : Type} [CStarAlgebra D] (ρ : Γ →* unitary D)
    (φ : Full Γ →⋆ₐ[ℂ] D) (hφ : ∀ g, φ (inclusion Γ g) = (ρ g : D)) :
    φ = modelMap Γ ρ := by
…
```
Mentions: OAI.NuclearUltrapower.FullGroupModel.Full, OAI.NuclearUltrapower.FullGroupModel.inclusion, OAI.NuclearUltrapower.FullGroupModel.modelMap
instance OAI.NuclearUltrapower.FullGroupModel.(instance at line 404) line 404
Source documentation
Countability of the group gives the standing separability conclusion.
```
instance [Countable Γ] : TopologicalSpace.SeparableSpace (Full Γ) := by
…
```
Mentions: OAI.NuclearUltrapower.FullGroupModel.Full