OAI/Analysis/NuclearUltrapower/FiniteInduction.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.NuclearUltrapower.lp_finiteDimensional line 14
2. instance OAI.NuclearUltrapower.induced_nontrivial line 28
3. def OAI.NuclearUltrapower.finiteInduced line 32

   Source documentation

   Finite-index unitary induction, using the exact coset cocycle.

   def finiteInduced : FiniteUnitaryRep.{u,u} Γ where
   …

4. def OAI.NuclearUltrapower.restrictSubgroup line 37

   Source documentation

   Restriction changes only the action, not the Hilbert carrier.

   def restrictSubgroup (σ : FiniteUnitaryRep.{u,u} Γ) : FiniteUnitaryRep.{u,u} H :=
   …

5. def OAI.NuclearUltrapower.identityCoordinate line 41

   Source documentation

   Identity-coordinate projection on the induced Hilbert space.

   def identityCoordinate : finiteInduced H α →L[ℂ] α :=
   …

   Mentions: OAI.NuclearUltrapower.finiteInduced

6. theorem OAI.NuclearUltrapower.identityCoordinate_apply line 44
7. theorem OAI.NuclearUltrapower.identityCoordinate_intertwines line 47
8. theorem OAI.NuclearUltrapower.identityCoordinate_nonzero line 54

   Source documentation

   Every nonzero subrepresentation of a finite induction has a nonzero identity-coordinate map. This is the all-constituent point in Frobenius reciprocity.

   theorem identityCoordinate_nonzero {σ : FiniteUnitaryRep.{u,u} Γ}
       (U : σ →ₗᵢ[ℂ] finiteInduced H α)
       (hU : ∀ g x, U (σ.action g x) = (finiteInduced H α).action g (U x)) :
       (identityCoordinate H α).comp U.toContinuousLinearMap ≠ 0 := by
   …

   Mentions: OAI.NuclearUltrapower.finiteInduced, OAI.NuclearUltrapower.identityCoordinate

9. theorem OAI.NuclearUltrapower.frobenius_all_constituents line 70
10. def OAI.NuclearUltrapower.tensorMapBetween line 114

    Source documentation

    Heterogeneous completion of the Hilbert tensor functor.

    def tensorMapBetween (U : E →L[ℂ] E') (V : F →L[ℂ] F') :
        TensorHilbert E F →L[ℂ] TensorHilbert E' F' := (TensorProduct.mapL U V).completion

    Mentions: OAI.NuclearUltrapower.TensorHilbert

11. theorem OAI.NuclearUltrapower.tensorMapBetween_coe line 117
12. theorem OAI.NuclearUltrapower.tensorMapBetween_comp line 122
13. theorem OAI.NuclearUltrapower.tensorMapBetween_one line 128
14. theorem OAI.NuclearUltrapower.tensorMapBetween_add_right line 131
15. theorem OAI.NuclearUltrapower.tensorMapBetween_zero_right line 135
16. def OAI.NuclearUltrapower.tensorIsometry line 140

    Source documentation

    Isometries remain isometries upon completion, proved using density.

    def tensorIsometry (U : E →ₗᵢ[ℂ] E') (V : F →ₗᵢ[ℂ] F') :
        TensorHilbert E F →ₗᵢ[ℂ] TensorHilbert E' F' where
    …

    Mentions: OAI.NuclearUltrapower.TensorHilbert

17. theorem OAI.NuclearUltrapower.tensorIsometry_toCLM line 153
18. theorem OAI.NuclearUltrapower.tensorMapBetween_adjoint line 157
19. def OAI.NuclearUltrapower.tensorInclusion line 184
20. def OAI.NuclearUltrapower.tensorProjection line 187
21. theorem OAI.NuclearUltrapower.tensorInclusion_projection line 191
22. theorem OAI.NuclearUltrapower.tensorProjection_norm_sq line 197
23. def OAI.NuclearUltrapower.coordinateInclusion line 258
24. theorem OAI.NuclearUltrapower.coordinateInclusion_apply line 264
25. theorem OAI.NuclearUltrapower.coordinateInclusion_identity line 267
26. theorem OAI.NuclearUltrapower.coordinateInclusion_action line 270
27. theorem OAI.NuclearUltrapower.cosetCocycle_factor line 284
28. theorem OAI.NuclearUltrapower.identityCoordinate_inclusion line 294
29. theorem OAI.NuclearUltrapower.identityCoordinate_norm_le line 303