Enveloping.lean`

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

Tensor-enveloping algebra actions, simplicity, and elementary row control.

abbrev OAI.FiniteAlgebraicEnvelopes.Enveloping.Coeff line 14
def OAI.FiniteAlgebraicEnvelopes.Enveloping.right line 17
Source documentation
Right multiplication, with its order correctly reversed.
```
def right : Bᵐᵒᵖ →ₐ[k] Module.End k B where
…
```
def OAI.FiniteAlgebraicEnvelopes.Enveloping.representation line 26
Source documentation
The true enveloping-ring action on the algebra.
```
def representation : Coeff k B →ₐ[k] Module.End k B :=
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Enveloping.Coeff
instance OAI.FiniteAlgebraicEnvelopes.Enveloping.module line 32
theorem OAI.FiniteAlgebraicEnvelopes.Enveloping.tmul_smul line 34
def OAI.FiniteAlgebraicEnvelopes.Enveloping.eval line 39
theorem OAI.FiniteAlgebraicEnvelopes.Enveloping.eval_apply line 40
theorem OAI.FiniteAlgebraicEnvelopes.Enveloping.eval_tmul line 41
def OAI.FiniteAlgebraicEnvelopes.Enveloping.difference line 43
theorem OAI.FiniteAlgebraicEnvelopes.Enveloping.difference_zero line 45
theorem OAI.FiniteAlgebraicEnvelopes.Enveloping.difference_one line 46
theorem OAI.FiniteAlgebraicEnvelopes.Enveloping.difference_add line 47
theorem OAI.FiniteAlgebraicEnvelopes.Enveloping.difference_mul line 50
theorem OAI.FiniteAlgebraicEnvelopes.Enveloping.difference_algebraMap line 56
def OAI.FiniteAlgebraicEnvelopes.Enveloping.relations line 61
Source documentation
The generators of the kernel, exactly d_y=y⊗1−1⊗yᵒᵖ.
```
def relations (Y : Set B) : Submodule (Coeff k B) (Coeff k B) :=
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Enveloping.Coeff
theorem OAI.FiniteAlgebraicEnvelopes.Enveloping.difference_mem line 65
Source documentation
The product identity propagates the kernel generators through the whole algebra.
```
theorem difference_mem (Y : Set B) (hgen : Algebra.adjoin k Y = ⊤) (b : B) :
    difference k B b ∈ relations (k:=k) Y := by
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Enveloping.difference, OAI.FiniteAlgebraicEnvelopes.Enveloping.relations
theorem OAI.FiniteAlgebraicEnvelopes.Enveloping.relations_le_kernel line 76
theorem OAI.FiniteAlgebraicEnvelopes.Enveloping.reduce_tensor line 84
Source documentation
Every tensor is congruent to its value tensored with one.
```
theorem reduce_tensor (Y : Set B) (hgen : Algebra.adjoin k Y = ⊤) (r : Coeff k B) :
    r - (eval k B r ⊗ₜ[k] (1:Bᵐᵒᵖ)) ∈ relations (k:=k) Y := by
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Enveloping.Coeff, OAI.FiniteAlgebraicEnvelopes.Enveloping.eval, OAI.FiniteAlgebraicEnvelopes.Enveloping.relations
theorem OAI.FiniteAlgebraicEnvelopes.Enveloping.kernel_eq line 101
theorem OAI.FiniteAlgebraicEnvelopes.Enveloping.eval_surjective line 110
def OAI.FiniteAlgebraicEnvelopes.Enveloping.quotientEquiv line 115
Source documentation
The cyclic-module lemma, with no assumed tensor action identities.
```
noncomputable def quotientEquiv (Y : Set B) (hgen : Algebra.adjoin k Y = ⊤) :
    (Coeff k B ⧸ relations (k:=k) Y) ≃ₗ[Coeff k B] B := by
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Enveloping.Coeff, OAI.FiniteAlgebraicEnvelopes.Enveloping.relations
def OAI.FiniteAlgebraicEnvelopes.Enveloping.reachable line 137
Source documentation
The coefficients that can be reached from one input form a two-sided ideal; unitality of the inclusion into B is deliberately not required.
```
def reachable (i : A →ₙₐ[k] B) (u : A) : TwoSidedIdeal A :=
…
```
theorem OAI.FiniteAlgebraicEnvelopes.Enveloping.coefficient_control line 157
Source documentation
Simplicity supplies every desired row operation.
```
theorem coefficient_control (i : A →ₙₐ[k] B) (u d : A) (hu : u ≠ 0) :
    ∃ r : Coeff k B, r • i u = i d := by
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Enveloping.Coeff
def OAI.FiniteAlgebraicEnvelopes.RowControl.act line 179
theorem OAI.FiniteAlgebraicEnvelopes.RowControl.act_one line 182
theorem OAI.FiniteAlgebraicEnvelopes.RowControl.act_mul line 183
theorem OAI.FiniteAlgebraicEnvelopes.RowControl.act_root line 185
def OAI.FiniteAlgebraicEnvelopes.RowControl.Related line 190
theorem OAI.FiniteAlgebraicEnvelopes.RowControl.Related.refl line 194
theorem OAI.FiniteAlgebraicEnvelopes.RowControl.Related.trans line 196
theorem OAI.FiniteAlgebraicEnvelopes.RowControl.Related.symm line 202
theorem OAI.FiniteAlgebraicEnvelopes.RowControl.set_row line 209
Source documentation
A genuine Steinberg element sets any nonpivot row to the desired value.
```
theorem set_row (i : A →ₙₐ[k] B) (v : Fin 6 → A) (j l : Fin 6)
    (hj : v j ≠ 0) (hl : l ≠ j) (a : A) : Related i v (Function.update v l a) := by
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.RowControl.Related
theorem OAI.FiniteAlgebraicEnvelopes.RowControl.set_rows line 222
Source documentation
Eliminate any finite set of rows around a fixed nonzero pivot.
```
theorem set_rows (i : A →ₙₐ[k] B) (v w : Fin 6 → A) (j : Fin 6)
    (hj : v j ≠ 0) (s : Finset (Fin 6)) (hs : j ∉ s) :
    Related i v (fun a => if a ∈ s then w a else v a) := by
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.RowControl.Related
theorem OAI.FiniteAlgebraicEnvelopes.RowControl.normalize line 242
Source documentation
Every nonzero vector in the simple-algebra image reaches the same standard column.
```
theorem normalize (i : A →ₙₐ[k] B) (v : Fin 6 → A) (hv : v ≠ 0) :
    Related i v (Pi.single 5 1) := by
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.RowControl.Related
theorem OAI.FiniteAlgebraicEnvelopes.RowControl.transitive_nonzero line 271
Source documentation
The linear core of two-transitivity, with actual root words.
```
theorem transitive_nonzero (i : A →ₙₐ[k] B) (v w : Fin 6 → A)
    (hv : v ≠ 0) (hw : w ≠ 0) : Related i v w :=
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.RowControl.Related