AuxiliaryGroupAlgebraPresentation.lean`

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

def OAI.LittleFinitistic.GroupAlgebraPresentation.auxiliaryGroupAlgebraEquiv line 11
Source documentation
Section 2's complex group algebra, for the exact auxiliary group supplied by the manuscript. The stable finite model has 18 generators, including the three redundant diagonal W generators killed by its relations.
```
def auxiliaryGroupAlgebraEquiv :
    PresentedAlgebra ℂ FinitePresentation.SeedGenerator FinitePresentation.finiteRelators ≃ₐ[ℂ]
      MonoidAlgebra ℂ Presentation.AuxiliaryGroup :=
…
```
Mentions: OAI.LittleFinitistic.GroupAlgebraPresentation.PresentedAlgebra, OAI.LittleFinitistic.FinitePresentation.SeedGenerator, OAI.LittleFinitistic.FinitePresentation.finiteRelators, OAI.LittleFinitistic.Presentation.AuxiliaryGroup
def OAI.LittleFinitistic.GroupAlgebraPresentation.auxiliaryGroupAlgebraZeroEquiv line 18
Source documentation
Same explicit presentation expressed as polynomial zero relations.
```
def auxiliaryGroupAlgebraZeroEquiv :
    (zeroRelations ℂ FinitePresentation.SeedGenerator FinitePresentation.finiteRelators).Quotient ≃ₐ[ℂ]
      MonoidAlgebra ℂ Presentation.AuxiliaryGroup :=
…
```
Mentions: OAI.LittleFinitistic.GroupAlgebraPresentation.zeroRelations, OAI.LittleFinitistic.FinitePresentation.SeedGenerator, OAI.LittleFinitistic.FinitePresentation.finiteRelators, OAI.LittleFinitistic.Presentation.AuxiliaryGroup
theorem OAI.LittleFinitistic.GroupAlgebraPresentation.auxiliaryGroupAlgebra_hasFinitePresentation line 26
Source documentation
The finite-presentation assertion for R = ℂ[G] in Section 2's proof of Proposition selection. This is a NONCOMMUTATIVE unital algebra presentation.
```
theorem auxiliaryGroupAlgebra_hasFinitePresentation :
    HasFinitePresentation ℂ (MonoidAlgebra ℂ Presentation.AuxiliaryGroup) := by
…
```
Mentions: OAI.LittleFinitistic.GroupAlgebraPresentation.HasFinitePresentation, OAI.LittleFinitistic.Presentation.AuxiliaryGroup
theorem OAI.LittleFinitistic.GroupAlgebraPresentation.auxiliary_algebra_generator_count line 32
Source documentation
Positive and negative letters for the stable finite model: 36 algebra generators.
```
theorem auxiliary_algebra_generator_count :
    Fintype.card (Letter FinitePresentation.SeedGenerator) = 36 := by
…
```
Mentions: OAI.LittleFinitistic.GroupAlgebraPresentation.Letter, OAI.LittleFinitistic.FinitePresentation.SeedGenerator