GroupAlgebraPresentation.lean`

35 declarations, 0 contain sorry, 0 declared as axioms

Section 2 bridge. All algebras here are associative, unital, and may be noncommutative. The defining congruence is generated by finitely many equations in a free associative algebra; no commutative finite-presentation API is used.

def OAI.LittleFinitistic.GroupAlgebraPresentation.word line 16
Source documentation
A representative word, chosen only to turn a group relator into a polynomial.
```
def word (g : FreeGroup α) : List (α × Bool) :=
…
```
theorem OAI.LittleFinitistic.GroupAlgebraPresentation.word_spec line 19
def OAI.LittleFinitistic.GroupAlgebraPresentation.polynomial line 22
theorem OAI.LittleFinitistic.GroupAlgebraPresentation.eval_polynomial line 27
abbrev OAI.LittleFinitistic.GroupAlgebraPresentation.Letter line 44
abbrev OAI.LittleFinitistic.GroupAlgebraPresentation.EquationIndex line 45
def OAI.LittleFinitistic.GroupAlgebraPresentation.equation line 48
Source documentation
Two inverse equations per generator, and one polynomial per group relator.
```
def equation : EquationIndex α rels → FreeAlgebra R (Letter α)
  | .inl (a,b) => FreeAlgebra.ι R (a,b) * FreeAlgebra.ι R (a,!b)
  | .inr r => polynomial R α r
```
Mentions: OAI.LittleFinitistic.GroupAlgebraPresentation.EquationIndex, OAI.LittleFinitistic.GroupAlgebraPresentation.Letter, OAI.LittleFinitistic.GroupAlgebraPresentation.polynomial
def OAI.LittleFinitistic.GroupAlgebraPresentation.relations line 52
abbrev OAI.LittleFinitistic.GroupAlgebraPresentation.PresentedAlgebra line 55
def OAI.LittleFinitistic.GroupAlgebraPresentation.quotientMap line 57
theorem OAI.LittleFinitistic.GroupAlgebraPresentation.equation_holds line 60
def OAI.LittleFinitistic.GroupAlgebraPresentation.generatorUnit line 64
theorem OAI.LittleFinitistic.GroupAlgebraPresentation.quotient_letter line 70
theorem OAI.LittleFinitistic.GroupAlgebraPresentation.unit_relator line 75
def OAI.LittleFinitistic.GroupAlgebraPresentation.groupToUnits line 81
def OAI.LittleFinitistic.GroupAlgebraPresentation.fromGroupAlgebra line 84
def OAI.LittleFinitistic.GroupAlgebraPresentation.groupAlgebraUnit line 87
def OAI.LittleFinitistic.GroupAlgebraPresentation.evaluation line 90
theorem OAI.LittleFinitistic.GroupAlgebraPresentation.evaluation_polynomial line 94
theorem OAI.LittleFinitistic.GroupAlgebraPresentation.evaluation_equation line 106
def OAI.LittleFinitistic.GroupAlgebraPresentation.toGroupAlgebra line 115
theorem OAI.LittleFinitistic.GroupAlgebraPresentation.toGroupAlgebra_quotient line 121
theorem OAI.LittleFinitistic.GroupAlgebraPresentation.fromGroupAlgebra_of line 124
theorem OAI.LittleFinitistic.GroupAlgebraPresentation.fromGroupAlgebra_inv_of line 129
theorem OAI.LittleFinitistic.GroupAlgebraPresentation.from_to_letter line 134
theorem OAI.LittleFinitistic.GroupAlgebraPresentation.from_to line 143
theorem OAI.LittleFinitistic.GroupAlgebraPresentation.to_from line 155
def OAI.LittleFinitistic.GroupAlgebraPresentation.quotientEquiv line 174
Source documentation
Explicit free associative algebra quotient presenting the group algebra.
```
def quotientEquiv : PresentedAlgebra R α rels ≃ₐ[R] MonoidAlgebra R (PresentedGroup rels) :=
…
```
Mentions: OAI.LittleFinitistic.GroupAlgebraPresentation.PresentedAlgebra
def OAI.LittleFinitistic.GroupAlgebraPresentation.HasFinitePresentation line 182
Source documentation
A finite presentation in the category of associative unital R-algebras. The finite generating set is not required to commute. A ring congruence is closed under multiplication on either side; these are two-sided equations.
```
def HasFinitePresentation (A : Type*) [Ring A] [Algebra R A] : Prop :=
…
```
theorem OAI.LittleFinitistic.GroupAlgebraPresentation.HasFinitePresentation.of_equiv line 189
Source documentation
Transport of a finite noncommutative presentation along an algebra equivalence.
```
theorem HasFinitePresentation.of_equiv {A B : Type*} [Ring A] [Ring B]
    [Algebra R A] [Algebra R B] (h : HasFinitePresentation R A) (e : A ≃ₐ[R] B) :
    HasFinitePresentation R B := by
…
```
Mentions: OAI.LittleFinitistic.GroupAlgebraPresentation.HasFinitePresentation
theorem OAI.LittleFinitistic.GroupAlgebraPresentation.presentedGroup_hasFinitePresentation line 197
Source documentation
Finitely many group generators and relators give finitely many algebra letters and equations, and the explicit quotient is the group algebra.
```
theorem presentedGroup_hasFinitePresentation (ι : Type) [Finite ι]
    (s : Set (FreeGroup ι)) [Finite s] :
    HasFinitePresentation R (MonoidAlgebra R (PresentedGroup s)) := by
…
```
Mentions: OAI.LittleFinitistic.GroupAlgebraPresentation.HasFinitePresentation
theorem OAI.LittleFinitistic.GroupAlgebraPresentation.groupAlgebra_hasFinitePresentation line 205
Source documentation
General Section 2 bridge, with no commutativity assumption on the group or its group algebra and no finite-presentation assumption on the algebra.
```
theorem groupAlgebra_hasFinitePresentation (G : Type*) [Group G]
    [Group.IsFinitelyPresented G] : HasFinitePresentation R (MonoidAlgebra R G) := by
…
```
Mentions: OAI.LittleFinitistic.GroupAlgebraPresentation.HasFinitePresentation
def OAI.LittleFinitistic.GroupAlgebraPresentation.zeroRelations line 214
Source documentation
Polynomial zero relations for the same explicit presentation.
```
def zeroRelations : RingCon (FreeAlgebra R (Letter α)) :=
…
```
Mentions: OAI.LittleFinitistic.GroupAlgebraPresentation.Letter
theorem OAI.LittleFinitistic.GroupAlgebraPresentation.relations_eq_zeroRelations line 220
Source documentation
Writing each equation p = 1 as p - 1 = 0 does not change the quotient. This matches the manuscript notation k⟨x₁,...,x_d⟩/(p₁,...,p_t).
```
theorem relations_eq_zeroRelations : relations R α rels = zeroRelations R α rels := by
…
```
Mentions: OAI.LittleFinitistic.GroupAlgebraPresentation.relations, OAI.LittleFinitistic.GroupAlgebraPresentation.zeroRelations
def OAI.LittleFinitistic.GroupAlgebraPresentation.zeroQuotientEquiv line 237
Source documentation
The explicit presentation is also a quotient by finitely many polynomial zero relations, in the exact form used by Section 3 of the manuscript.
```
def zeroQuotientEquiv : (zeroRelations R α rels).Quotient ≃ₐ[R]
    MonoidAlgebra R (PresentedGroup rels) :=
…
```
Mentions: OAI.LittleFinitistic.GroupAlgebraPresentation.zeroRelations