GroupObstruction.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.NuclearUltrapower.InjectiveInducedSpace line 20
Source documentation
Induction along an honest subgroup inclusion; the index may be infinite.
```
abbrev InjectiveInducedSpace := lp (fun _ : Δ ⧸ f.range => π) 2
```
def OAI.NuclearUltrapower.injectiveInduced line 22
theorem OAI.NuclearUltrapower.injectiveInduction_intertwines line 26
Source documentation
On the identity coset the induced representation contains the original one.
```
theorem injectiveInduction_intertwines (g : Γ) (x : π) :
    inductionInclusion f.range (π.action g x) =
      injectiveInduced f hf π (f g) (inductionInclusion f.range x) := by
…
```
Mentions: OAI.NuclearUltrapower.inductionInclusion, OAI.NuclearUltrapower.injectiveInduced
theorem OAI.NuclearUltrapower.injectiveInduced_invariant_tensor line 37
Source documentation
The full group algebra sees the initial finite-dimensional constituent, using an algebraic invariant tensor in the identity coset of the induction.
```
theorem injectiveInduced_invariant_tensor :
    ∃ z : InjectiveInducedSpace f π ⊗[ℂ] π.dual, z ≠ 0 ∧
      ∀ g : Γ, TensorProduct.congrIsometry (injectiveInduced f hf π (f g))
        (π.dual.action g) z = z := by
…
```
Mentions: OAI.NuclearUltrapower.InjectiveInducedSpace, OAI.NuclearUltrapower.injectiveInduced

theorem OAI.NuclearUltrapower.faithful_hilbert_nontrivial line 67

Source documentation

A faithful unital representation of a nonzero algebra has nonzero Hilbert space.

theorem faithful_hilbert_nontrivial {B E : Type*} [CStarAlgebra B] [Nontrivial B]
    [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E]
    (ρ : B →⋆ₐ[ℂ] (E →L[ℂ] E)) (hρ : Function.Injective ρ) : Nontrivial E := by
…

theorem OAI.NuclearUltrapower.fullGroup_no_nuclear_ultrapower line 89
Source documentation
The spectral obstruction for an injective ascending subgroup in the exact ambient group, without assuming an initial match or a coordinate representation.
```
theorem fullGroup_no_nuclear_ultrapower (hB : IsNuclear.{0,0} B)
    (ω : Ultrafilter ℕ) (hω : IsFree ω) :
    ¬ ∃ φ : FullGroupModel.Full Δ →⋆ₐ[ℂ] NormUltrapower B ω,
      Function.Injective φ := by
…
```
Mentions: OAI.NuclearUltrapower.IsFree, OAI.NuclearUltrapower.FullGroupModel.Full, OAI.NuclearUltrapower.NormUltrapower