FiniteRepresentations.lean`

26 declarations, 0 contain sorry, 0 declared as axioms

structure OAI.NuclearUltrapower.FiniteUnitaryRep line 16
Source documentation
A nonzero finite-dimensional unitary representation.
```
structure FiniteUnitaryRep (Γ : Type u) [Group Γ] where
…
```
instance OAI.NuclearUltrapower.(instance at line 27) line 27
def OAI.NuclearUltrapower.FiniteUnitaryRep.Irreducible line 35
Source documentation
Irreducibility with exactly the invariant-subspace convention of the source.
```
def Irreducible (π : FiniteUnitaryRep.{u,v} Γ) : Prop :=
…
```
def OAI.NuclearUltrapower.FiniteUnitaryRep.pull line 38
theorem OAI.NuclearUltrapower.FiniteUnitaryRep.pull_action line 41
theorem OAI.NuclearUltrapower.FiniteUnitaryRep.pull_one line 44
theorem OAI.NuclearUltrapower.FiniteUnitaryRep.pull_pull line 48
def OAI.NuclearUltrapower.FiniteUnitaryRep.Embeds line 52
Source documentation
Isometric inclusion as a subrepresentation: no quotients of representations.
```
def Embeds (π τ : FiniteUnitaryRep.{u,v} Γ) : Prop :=
…
```
def OAI.NuclearUltrapower.FiniteUnitaryRep.Equivalent line 56
Source documentation
Unitary equivalence, not merely equality of dimensions.
```
def Equivalent (π τ : FiniteUnitaryRep.{u,v} Γ) : Prop :=
…
```
theorem OAI.NuclearUltrapower.FiniteUnitaryRep.embeds_refl line 59
theorem OAI.NuclearUltrapower.FiniteUnitaryRep.equivalent_refl line 62
theorem OAI.NuclearUltrapower.FiniteUnitaryRep.Embeds.trans line 65
theorem OAI.NuclearUltrapower.FiniteUnitaryRep.Equivalent.symm line 71
theorem OAI.NuclearUltrapower.FiniteUnitaryRep.Equivalent.trans line 78
theorem OAI.NuclearUltrapower.FiniteUnitaryRep.Equivalent.embeds line 84
theorem OAI.NuclearUltrapower.FiniteUnitaryRep.Embeds.pull line 89
theorem OAI.NuclearUltrapower.FiniteUnitaryRep.Equivalent.pull line 94

theorem OAI.NuclearUltrapower.FiniteUnitaryRep.Embeds.equivalent_of_finrank_eq line 100

Source documentation

Equidimensional subrepresentations are unitary equivalences.

theorem Embeds.equivalent_of_finrank_eq {π τ : FiniteUnitaryRep.{u,v} Γ}
    (h : π.Embeds τ) (hd : Module.finrank ℂ π = Module.finrank ℂ τ) : π.Equivalent τ := by
…

theorem OAI.NuclearUltrapower.FiniteUnitaryRep.Equivalent.irreducible line 107
Source documentation
Irreducibility is preserved under unitary equivalence.
```
theorem Equivalent.irreducible {π τ : FiniteUnitaryRep.{u,v} Γ}
    (h : π.Equivalent τ) (hπ : π.Irreducible) : τ.Irreducible := by
…
```
theorem OAI.NuclearUltrapower.FiniteUnitaryRep.Embeds.equivalent_of_irreducible line 134
Source documentation
A nonzero subrepresentation of an irreducible representation is the whole.
```
theorem Embeds.equivalent_of_irreducible {π τ : FiniteUnitaryRep.{u,v} Γ}
    (h : π.Embeds τ) (hτ : τ.Irreducible) : π.Equivalent τ := by
…
```
theorem OAI.NuclearUltrapower.FiniteUnitaryRep.irreducible_of_pull line 149
Source documentation
If a deeper pullback is irreducible, every preceding pullback is irreducible.
```
theorem irreducible_of_pull {π : FiniteUnitaryRep.{u,v} Γ} (θ : Monoid.End Γ)
    (h : (π.pull θ).Irreducible) : π.Irreducible := by
…
```
Mentions: OAI.NuclearUltrapower.FiniteUnitaryRep.Irreducible
theorem OAI.NuclearUltrapower.FiniteUnitaryRep.irreducible_pull_of_periodic line 156
Source documentation
Periodicity forces every positive pullback to remain irreducible, the critical step often missed when a predecessor chain has a nonempty tail.
```
theorem irreducible_pull_of_periodic {π : FiniteUnitaryRep.{u,v} Γ}
    (hπ : π.Irreducible) (θ : Monoid.End Γ) {p : ℕ} (hp : 0 < p)
    (he : π.Equivalent (π.pull (θ ^ p))) (j : ℕ) : (π.pull (θ ^ j)).Irreducible := by
…
```
Mentions: OAI.NuclearUltrapower.FiniteUnitaryRep.Irreducible
theorem OAI.NuclearUltrapower.FiniteUnitaryRep.finite_predecessor_cycle line 176
Source documentation
Source lem:finite-predecessor-cycle, expressed using any finite list of representatives. Duplicates are harmless; no bijective predecessor selection is assumed, and the possibly nonempty tail is fully accounted for.
```
theorem finite_predecessor_cycle {ι : Type*} [Finite ι]
    (π : ι → FiniteUnitaryRep.{u,v} Γ) (hπ : ∀ i, (π i).Irreducible)
    (θ : Monoid.End Γ) (hprev : ∀ i, ∃ j, (π i).Embeds ((π j).pull θ)) (i : ι) :
    ∃ p : ℕ, 0 < p ∧ (π i).Equivalent ((π i).pull (θ ^ p)) := by
…
```
Mentions: OAI.NuclearUltrapower.FiniteUnitaryRep.Irreducible, OAI.NuclearUltrapower.FiniteUnitaryRep.Embeds, OAI.NuclearUltrapower.FiniteUnitaryRep.pull, OAI.NuclearUltrapower.FiniteUnitaryRep.Equivalent

def OAI.NuclearUltrapower.FiniteUnitaryRep.restrict line 213

Source documentation

Restriction to an invariant subspace, with the inherited Hilbert norm.

def restrict (π : FiniteUnitaryRep.{u,v} Γ) (W : Submodule ℂ π)
    (hW : ∀ g x, x ∈ W → π.action g x ∈ W) [Nontrivial W] : FiniteUnitaryRep.{u,v} Γ where
…

theorem OAI.NuclearUltrapower.FiniteUnitaryRep.restrict_embeds line 228
theorem OAI.NuclearUltrapower.FiniteUnitaryRep.exists_irreducible line 235
Source documentation
Every nonzero finite-dimensional unitary representation has an irreducible subrepresentation. This uses minimal dimension, not a semisimplicity assumption.
```
theorem exists_irreducible (π : FiniteUnitaryRep.{u,v} Γ) :
    ∃ τ : FiniteUnitaryRep.{u,v} Γ, τ.Irreducible ∧ τ.Embeds π := by
…
```