Steinberg.lean`

146 declarations, 0 contain sorry, 0 declared as axioms

Nonunital correction, Steinberg groups, corners, and kernel annihilation.

def OAI.FiniteAlgebraicEnvelopes.correctedMap line 24
Source documentation
Adjoining the unchanged complementary identity to a nonunital map.
```
def correctedMap (ψ : R →ₙ+* S) : R →* S where
…
```
theorem OAI.FiniteAlgebraicEnvelopes.correctedMap_apply line 33
theorem OAI.FiniteAlgebraicEnvelopes.correctedMap_injective line 36

def OAI.FiniteAlgebraicEnvelopes.matrixNonunitalMap line 43

Source documentation

Entrywise extension before adjoining the unchanged identity.

def matrixNonunitalMap {ι : Type*} [Fintype ι] [DecidableEq ι] (ψ : R →ₙ+* S) :
    Matrix ι ι R →ₙ+* Matrix ι ι S where
…

theorem OAI.FiniteAlgebraicEnvelopes.matrixNonunitalMap_apply line 50
abbrev OAI.FiniteAlgebraicEnvelopes.Steinberg.Index line 61
abbrev OAI.FiniteAlgebraicEnvelopes.Steinberg.Generator line 62
def OAI.FiniteAlgebraicEnvelopes.Steinberg.freeRoot line 64
inductive OAI.FiniteAlgebraicEnvelopes.Steinberg.Relation line 67
abbrev OAI.FiniteAlgebraicEnvelopes.Steinberg.Group line 78
def OAI.FiniteAlgebraicEnvelopes.Steinberg.root line 82
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.mk_freeRoot line 85
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.root_add line 88
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.root_chain line 92
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.root_distant line 97
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.root_zero line 104
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.root_neg line 108
def OAI.FiniteAlgebraicEnvelopes.Steinberg.coefficientMap line 115
Source documentation
Every additive multiplicative coefficient map induces a Steinberg map; it is not required to preserve one.
```
def coefficientMap (ψ : R →ₙ+* S) : Group ι R →* Group ι S :=
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Steinberg.Group
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.coefficientMap_root line 131
def OAI.FiniteAlgebraicEnvelopes.Steinberg.x line 140
Source documentation
A total notation: the unused diagonal root is the identity.
```
def x (i j : ι) (a : R) : Group ι R := if h : i = j then 1 else root i j h a
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Steinberg.Group, OAI.FiniteAlgebraicEnvelopes.Steinberg.root
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.x_self line 142
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.x_of_ne line 144
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.x_zero line 147
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.x_add line 151
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.x_neg line 157
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.x_distant line 162
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.x_chain line 171
def OAI.FiniteAlgebraicEnvelopes.Steinberg.xAddHom line 177
Source documentation
Additive root parametrization, without assuming a commutative ring.
```
def xAddHom (i j : ι) : R →+ Additive (Group ι R) where
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Steinberg.Group
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.xAddHom_apply line 182
def OAI.FiniteAlgebraicEnvelopes.Steinberg.elementary line 191
Source documentation
Elementary matrices over an arbitrary, possibly noncommutative, ring.
```
def elementary (i j : ι) (h : i ≠ j) (a : R) : (Matrix ι ι R)ˣ where
…
```
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.elementary_val line 209
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.elementary_inv_val line 212
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.elementary_add line 215
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.elementary_chain line 223
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.elementary_distant line 234
def OAI.FiniteAlgebraicEnvelopes.Steinberg.matrixMap line 245
Source documentation
The matrix action of the presented Steinberg group. Its codomain here is all matrix units rather than the equal image subgroup E_n(R).
```
def matrixMap : Group ι R →* (Matrix ι ι R)ˣ :=
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Steinberg.Group
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.matrixMap_root line 261
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.matrixMap_coefficientMap line 265
Source documentation
Naturality of the matrix action for a nonunital coefficient map.
```
theorem matrixMap_coefficientMap (ψ : R →ₙ+* S) (z : Group ι R) :
    matrixMap (coefficientMap ψ z) =
      Units.map (correctedMap (matrixNonunitalMap ψ)) (matrixMap z) := by
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Steinberg.Group, OAI.FiniteAlgebraicEnvelopes.Steinberg.matrixMap, OAI.FiniteAlgebraicEnvelopes.Steinberg.coefficientMap, OAI.FiniteAlgebraicEnvelopes.correctedMap, OAI.FiniteAlgebraicEnvelopes.matrixNonunitalMap
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.coefficientMap_preserves_kernel line 282
Source documentation
In particular, coefficient maps preserve the full matrix kernel.
```
theorem coefficientMap_preserves_kernel (ψ : R →ₙ+* S) (z : Group ι R)
    (hz : matrixMap z = 1) : matrixMap (coefficientMap ψ z) = 1 := by
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Steinberg.Group, OAI.FiniteAlgebraicEnvelopes.Steinberg.matrixMap, OAI.FiniteAlgebraicEnvelopes.Steinberg.coefficientMap
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.column_roots_commute line 290
def OAI.FiniteAlgebraicEnvelopes.Steinberg.columnAddHom line 298
def OAI.FiniteAlgebraicEnvelopes.Steinberg.column line 303
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.column_single line 305
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.column_zero line 309
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.column_add line 312
def OAI.FiniteAlgebraicEnvelopes.Steinberg.mulVecAddHom line 316
Source documentation
Left multiplication of columns, viewed purely additively.
```
def mulVecAddHom (A : Matrix ι ι R) : (ι → R) →+ (ι → R) where
…
```
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.mulVecAddHom_apply line 322
def OAI.FiniteAlgebraicEnvelopes.Steinberg.conjugateAddHom line 326
Source documentation
Additive notation for conjugation in the Steinberg group.
```
def conjugateAddHom (g : Group ι R) : Additive (Group ι R) →+ Additive (Group ι R) :=
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Steinberg.Group
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.conjugateAddHom_apply line 330
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.elementary_mulVec line 333
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.x_conjugate_column line 339
Source documentation
Conjugation by one root acts on the external column as its elementary matrix.
```
theorem x_conjugate_column (i j k : ι) (hij : i ≠ j) (hik : i ≠ k) (hjk : j ≠ k)
    (a : R) (v : ι → R) :
    x i j a * column k v * (x i j a)⁻¹ =
      column k (Matrix.mulVec (elementary i j hij a).val v) := by
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Steinberg.x, OAI.FiniteAlgebraicEnvelopes.Steinberg.column, OAI.FiniteAlgebraicEnvelopes.Steinberg.elementary
def OAI.FiniteAlgebraicEnvelopes.Steinberg.omitting line 363
Source documentation
Words generated without using the index k.
```
def omitting (k : ι) : Subgroup (Group ι R) :=
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Steinberg.Group
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.x_mem_omitting line 367
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.conjugate_column_of_mem_omitting line 371
Source documentation
External-column action for an arbitrary word omitting k, not just for generators.
```
theorem conjugate_column_of_mem_omitting (k : ι) {z : Group ι R} (hz : z ∈ omitting k)
    (v : ι → R) : z * column k v * z⁻¹ = column k (Matrix.mulVec (matrixMap z).val v) := by
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Steinberg.Group, OAI.FiniteAlgebraicEnvelopes.Steinberg.omitting, OAI.FiniteAlgebraicEnvelopes.Steinberg.column, OAI.FiniteAlgebraicEnvelopes.Steinberg.matrixMap
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.row_roots_commute line 395
def OAI.FiniteAlgebraicEnvelopes.Steinberg.rowAddHom line 403
def OAI.FiniteAlgebraicEnvelopes.Steinberg.row line 408
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.row_single line 410
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.row_zero line 414
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.row_add line 416
def OAI.FiniteAlgebraicEnvelopes.Steinberg.vecMulAddHom line 419
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.vecMulAddHom_apply line 425
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.vecMul_single_matrix line 428
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.elementary_inv_vecMul line 435
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.x_conjugate_row line 444
Source documentation
Row form of the one-root conjugation identity.
```
theorem x_conjugate_row (i j k : ι) (hij : i ≠ j) (hik : i ≠ k) (hjk : j ≠ k)
    (a : R) (v : ι → R) :
    x i j a * row k v * (x i j a)⁻¹ =
      row k (Matrix.vecMul v ((elementary i j hij a)⁻¹).val) := by
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Steinberg.x, OAI.FiniteAlgebraicEnvelopes.Steinberg.row, OAI.FiniteAlgebraicEnvelopes.Steinberg.elementary
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.conjugate_row_of_mem_omitting line 471
Source documentation
External-row action for arbitrary words omitting k.
```
theorem conjugate_row_of_mem_omitting (k : ι) {z : Group ι R} (hz : z ∈ omitting k)
    (v : ι → R) : z * row k v * z⁻¹ = row k (Matrix.vecMul v ((matrixMap z)⁻¹).val) := by
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Steinberg.Group, OAI.FiniteAlgebraicEnvelopes.Steinberg.omitting, OAI.FiniteAlgebraicEnvelopes.Steinberg.row, OAI.FiniteAlgebraicEnvelopes.Steinberg.matrixMap
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.commute_commutator line 496
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.central_of_omitting line 503
Source documentation
A Steinberg element with trivial matrix and an unused index is central. This is the first centrality statement in the Steinberg kernel argument, with no rank-stability assumption.
```
theorem central_of_omitting (k : ι) {z : Group ι R} (hz : z ∈ omitting k)
    (hπ : matrixMap z = 1) : z ∈ Subgroup.center (Group ι R) := by
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Steinberg.Group, OAI.FiniteAlgebraicEnvelopes.Steinberg.omitting, OAI.FiniteAlgebraicEnvelopes.Steinberg.matrixMap
structure OAI.FiniteAlgebraicEnvelopes.Steinberg.CornerPair line 537
def OAI.FiniteAlgebraicEnvelopes.Steinberg.CornerPair.swap line 555
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.CornerPair.d_left line 569
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.CornerPair.d_right line 575
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.CornerPair.d_left_zero line 581
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.CornerPair.d_right_zero line 584
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.CornerPair.e_left line 587
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.CornerPair.e_right line 589
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.CornerPair.e_left_zero line 591
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.CornerPair.e_right_zero line 593
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.CornerPair.left_of_corner line 595
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.CornerPair.right_of_corner line 601
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.CornerPair.e_mul_corner line 607
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.CornerPair.corner_mul_d line 610
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.CornerPair.E_mul_d_corner line 613
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.CornerPair.corner_e_mul_E line 616
def OAI.FiniteAlgebraicEnvelopes.Steinberg.compression line 625
Source documentation
The actual compression word in the Steinberg kernel argument, not a matrix lift assumed to exist.
```
def compression (c : CornerPair R) (p q : ι) : Group ι R :=
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Steinberg.CornerPair, OAI.FiniteAlgebraicEnvelopes.Steinberg.Group
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.conjugate_mul line 629
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.compression_column_p line 632
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.compression_column_q line 645
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.compression_row_p line 665
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.compression_row_q line 678
def OAI.FiniteAlgebraicEnvelopes.Steinberg.cornerSubgroup line 699
Source documentation
Subgroup generated by root coefficients in an idempotent corner.
```
def cornerSubgroup (E : R) : Subgroup (Group ι R) :=
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Steinberg.Group
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.commutator_mem_subgroup line 703
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.compression_mem_omitting line 709
Source documentation
Compression sends all corner words into the subgroup with an unused index.
```
theorem compression_mem_omitting (c : CornerPair R) (p q r : ι)
    (hpq : p ≠ q) (hpr : p ≠ r) (hqr : q ≠ r)
    {z : Group ι R} (hz : z ∈ cornerSubgroup c.E) :
    compression c p q * z * (compression c p q)⁻¹ ∈ omitting q := by
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Steinberg.CornerPair, OAI.FiniteAlgebraicEnvelopes.Steinberg.Group, OAI.FiniteAlgebraicEnvelopes.Steinberg.cornerSubgroup, OAI.FiniteAlgebraicEnvelopes.Steinberg.compression, OAI.FiniteAlgebraicEnvelopes.Steinberg.omitting
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.central_of_corner line 771
Source documentation
the Steinberg kernel argument, corner-centrality. No relation for opposite roots is assumed.
```
theorem central_of_corner (c : CornerPair R) (p q r : ι)
    (hpq : p ≠ q) (hpr : p ≠ r) (hqr : q ≠ r)
    {z : Group ι R} (hz : z ∈ cornerSubgroup c.E) (hπ : matrixMap z = 1) :
    z ∈ Subgroup.center (Group ι R) := by
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Steinberg.CornerPair, OAI.FiniteAlgebraicEnvelopes.Steinberg.Group, OAI.FiniteAlgebraicEnvelopes.Steinberg.cornerSubgroup, OAI.FiniteAlgebraicEnvelopes.Steinberg.matrixMap
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.x_commute_of_zero_nonopposite line 788
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.corner_product_zero line 808
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.x_commute_orthogonal_corners line 817
Source documentation
Opposite roots also commute for orthogonal corner coefficients; this follows from a third root index, not from an additional Steinberg defining relation.
```
theorem x_commute_orthogonal_corners
    (hthird : ∀ i j : ι, ∃ k, k ≠ i ∧ k ≠ j)
    {E F : R} (hE : E * E = E) (hEF : E * F = 0) (hFE : F * E = 0)
    (i j k l : ι) (a b : R) (ha : E * a * E = a) (hb : F * b * F = b) :
    Commute (x i j a) (x k l b) := by
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Steinberg.x
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.cornerSubgroups_commute line 854
Source documentation
the Steinberg kernel argument, orthogonal-root-images, extended from roots to all words.
```
theorem cornerSubgroups_commute
    (hthird : ∀ i j : ι, ∃ k, k ≠ i ∧ k ≠ j)
    {E F : R} (hE : E * E = E) (hEF : E * F = 0) (hFE : F * E = 0)
    {z w : Group ι R} (hz : z ∈ cornerSubgroup E) (hw : w ∈ cornerSubgroup F) :
    Commute z w := by
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Steinberg.Group, OAI.FiniteAlgebraicEnvelopes.Steinberg.cornerSubgroup
def OAI.FiniteAlgebraicEnvelopes.Steinberg.weyl line 879
Source documentation
Weyl word for an involutive unit b=b⁻¹.
```
def weyl (b : R) (p q : ι) : Group ι R :=
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Steinberg.Group
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.weyl_column_p line 882
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.weyl_column_q line 899
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.weyl_row_p line 916
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.weyl_row_q line 933
def OAI.FiniteAlgebraicEnvelopes.Steinberg.balanced line 950
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.balanced_column_p line 952
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.balanced_column_q line 959
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.balanced_row_p line 966
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.balanced_row_q line 973
def OAI.FiniteAlgebraicEnvelopes.Steinberg.pairScalar line 980
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.balanced_root line 983
Source documentation
Exact balanced diagonal action, including the roots internal to its pair.
```
theorem balanced_root (b : R) (hb : b * b = 1)
    (hthird : ∀ i j : ι, ∃ k, k ≠ i ∧ k ≠ j)
    (p q : ι) (hpq : p ≠ q) (i j : ι) (y : R) :
    balanced b p q * x i j y * (balanced b p q)⁻¹ =
      x i j (pairScalar b p q i * y * pairScalar b p q j) := by
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Steinberg.balanced, OAI.FiniteAlgebraicEnvelopes.Steinberg.x, OAI.FiniteAlgebraicEnvelopes.Steinberg.pairScalar
def OAI.FiniteAlgebraicEnvelopes.Steinberg.scalarDiagonal line 1041
Source documentation
Scalar diagonal lift in rank six, exactly the three factors in the source.
```
def scalarDiagonal (b : R) : Group (Fin 6) R :=
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Steinberg.Group
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.scalarDiagonal_root line 1045
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.CornerPair.dd line 1071
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.CornerPair.ee line 1076
def OAI.FiniteAlgebraicEnvelopes.Steinberg.CornerPair.swapScalar line 1079
Source documentation
The involutive scalar interchanging the two corners.
```
def swapScalar : R := c.d + c.e + 1 - c.E - c.F
```
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.CornerPair.swapScalar_square line 1081
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.CornerPair.swapScalar_E line 1088
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.CornerPair.d_swapScalar line 1093
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.CornerPair.swapScalar_E_swapScalar line 1098
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.CornerPair.swapScalar_commute line 1101
def OAI.FiniteAlgebraicEnvelopes.Steinberg.cornerMap line 1108
Source documentation
Cutting down a nonunital coefficient map by a commuting idempotent.
```
def cornerMap (ψ : R →ₙ+* S) (E : S) (hE : E * E = E)
    (hc : ∀ a, Commute E (ψ a)) : R →ₙ+* S where
…
```
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.cornerMap_apply line 1121
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.cornerMap_corner line 1124
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.coefficientMap_mem_corner line 1134
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.coefficientMap_corner_central line 1145
Source documentation
Centrality of every corner image of an arbitrary matrix-kernel element.
```
theorem coefficientMap_corner_central (ψ : R →ₙ+* S) (c : CornerPair S)
    (hE : ∀ a, Commute c.E (ψ a)) (p q r : ι)
    [Fintype ι] (hpq : p ≠ q) (hpr : p ≠ r) (hqr : q ≠ r)
    {z : Group ι R} (hz : matrixMap z = 1) :
    coefficientMap (cornerMap ψ c.E c.E_idem hE) z ∈ Subgroup.center (Group ι S) :=
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Steinberg.CornerPair, OAI.FiniteAlgebraicEnvelopes.Steinberg.Group, OAI.FiniteAlgebraicEnvelopes.Steinberg.matrixMap, OAI.FiniteAlgebraicEnvelopes.Steinberg.coefficientMap, OAI.FiniteAlgebraicEnvelopes.Steinberg.cornerMap
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.corner_comparison line 1157
Source documentation
the Steinberg kernel argument, corner-comparison, with exact group elements rather than K₂ classes.
```
theorem corner_comparison (ψ : R →ₙ+* S) (c : CornerPair S)
    (hE : ∀ a, Commute c.E (ψ a)) (hF : ∀ a, Commute c.F (ψ a))
    (hd : ∀ a, Commute c.d (ψ a)) (he : ∀ a, Commute c.e (ψ a))
    {z : Group (Fin 6) R} (hz : matrixMap z = 1) :
    coefficientMap (cornerMap ψ c.E c.E_idem hE) z =
      coefficientMap (cornerMap ψ c.F c.F_idem hF) z := by
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Steinberg.CornerPair, OAI.FiniteAlgebraicEnvelopes.Steinberg.Group, OAI.FiniteAlgebraicEnvelopes.Steinberg.matrixMap, OAI.FiniteAlgebraicEnvelopes.Steinberg.coefficientMap, OAI.FiniteAlgebraicEnvelopes.Steinberg.cornerMap
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.orthogonal_sum_idem line 1190

theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.coefficientMap_corner_sum line 1195

Source documentation

Orthogonal corner images split without any residual central factor.

theorem coefficientMap_corner_sum [DecidableEq ι]
    (hthird : ∀ i j : ι, ∃ k, k ≠ i ∧ k ≠ j)
    (ψ : R →ₙ+* S) (E F : S) (hE : E * E = E) (hF : F * F = F)
    (hEF : E * F = 0) (hFE : F * E = 0)
    (hcE : ∀ a, Commute E (ψ a)) (hcF : ∀ a, Commute F (ψ a)) (z : Group ι R) :
    coefficientMap (cornerMap ψ (E + F) (orthogonal_sum_idem hE hF hEF hFE)
      (fun a => (hcE a).add_left (hcF a))) z =
      coefficientMap (cornerMap ψ E hE hcE) z *
        coefficientMap (cornerMap ψ F hF hcF) z := by
…

Mentions: OAI.FiniteAlgebraicEnvelopes.Steinberg.Group, OAI.FiniteAlgebraicEnvelopes.Steinberg.coefficientMap, OAI.FiniteAlgebraicEnvelopes.Steinberg.cornerMap, OAI.FiniteAlgebraicEnvelopes.Steinberg.orthogonal_sum_idem

structure OAI.FiniteAlgebraicEnvelopes.Steinberg.SupportedPair line 1231
Source documentation
A pair of supported one-sided inverse elements, with the prescribed commutation with the nonunital coefficient image.
```
structure SupportedPair (ψ : R →ₙ+* S) where
…
```
def OAI.FiniteAlgebraicEnvelopes.Steinberg.SupportedPair.E line 1245
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.SupportedPair.E_idem line 1247
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.SupportedPair.commE line 1253
def OAI.FiniteAlgebraicEnvelopes.Steinberg.SupportedPair.comp line 1256
Source documentation
Composition gives the descendants 00 and 01 of the zero corner.
```
def comp : SupportedPair ψ where
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Steinberg.SupportedPair
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.SupportedPair.E_mul_E line 1270
def OAI.FiniteAlgebraicEnvelopes.Steinberg.SupportedPair.corners line 1277
Source documentation
Explicit equivalence data between two orthogonal supported corners.
```
def corners (hpq : p.V * q.U = 0) (hqp : q.V * p.U = 0) : CornerPair S where
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Steinberg.CornerPair
def OAI.FiniteAlgebraicEnvelopes.Steinberg.SupportedPair.image line 1307
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.SupportedPair.image_eq line 1310
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.SupportedPair.comp_cross line 1316
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.SupportedPair.comp_cross_right line 1322
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.SupportedPair.comp_cross_left line 1327
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.SupportedPair.comp_split line 1332
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.SupportedPair.image_split line 1340
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.SupportedPair.annihilation line 1358
Source documentation
The source four-corner swindle. All comparison and commutation facts above hold in St₆ itself, so the final cancellation is an equality of group elements.
```
theorem annihilation (hpq : p.V * q.U = 0) (hqp : q.V * p.U = 0)
    (hsum : p.E + q.E = ψ 1) {z : Group (Fin 6) R} (hz : matrixMap z = 1) :
    coefficientMap ψ z = 1 := by
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Steinberg.Group, OAI.FiniteAlgebraicEnvelopes.Steinberg.matrixMap, OAI.FiniteAlgebraicEnvelopes.Steinberg.coefficientMap
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.left_support_of_corner line 1390
Source documentation
Elementary support calculus for the corner ψ(1)Rψ(1).
```
theorem left_support_of_corner {P a : S} (hP : P * P = P) (ha : P * a * P = a) :
    P * a = a := by
…
```
theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.right_support_of_corner line 1397

theorem OAI.FiniteAlgebraicEnvelopes.Steinberg.kernel_annihilation line 1406

Source documentation

the Steinberg kernel argument, Theorem kernel. A nonunital coefficient map with a commuting binary splitting pair annihilates the entire rank-six matrix kernel in one step. The four support equations say exactly that U₀,U₁,V₀,V₁ lie in PRP, P=ψ(1).

theorem kernel_annihilation (ψ : R →ₙ+* R) (U₀ U₁ V₀ V₁ : R)
    (hU₀ : ψ 1 * U₀ * ψ 1 = U₀) (hU₁ : ψ 1 * U₁ * ψ 1 = U₁)
    (hV₀ : ψ 1 * V₀ * ψ 1 = V₀) (hV₁ : ψ 1 * V₁ * ψ 1 = V₁)
    (cU₀ : ∀ a, Commute U₀ (ψ a)) (cU₁ : ∀ a, Commute U₁ (ψ a))
    (cV₀ : ∀ a, Commute V₀ (ψ a)) (cV₁ : ∀ a, Commute V₁ (ψ a))
    (h00 : V₀ * U₀ = ψ 1) (h11 : V₁ * U₁ = ψ 1)
    (h01 : V₀ * U₁ = 0) (h10 : V₁ * U₀ = 0)
    (hsum : U₀ * V₀ + U₁ * V₁ = ψ 1)
    (z : Group (Fin 6) R) (hz : matrixMap z = 1) : coefficientMap ψ z = 1 := by
…

Mentions: OAI.FiniteAlgebraicEnvelopes.Steinberg.Group, OAI.FiniteAlgebraicEnvelopes.Steinberg.matrixMap, OAI.FiniteAlgebraicEnvelopes.Steinberg.coefficientMap