Main results 101 to 200
| Declaration | Kind | Where | Note |
|---|---|---|---|
Matrix.GeneralLinearGroup.stabilize_commutator_eq_blockDiagonalUnit_mul |
theorem | GeneralLinearGroups/RelativeWhiteheadConsequences.lean, line 39 | The ordered commutator has a three-diagonal factorization after doubling. The final diagonal is indexed by (h * g)⁻¹, not (g * h)⁻¹. |
Matrix.GeneralLinearGroup.stabilize_conj_mem_relativeElementarySubgroup |
theorem | GeneralLinearGroups/RelativeWhiteheadConsequences.lean, line 47 | An arbitrary general linear conjugator preserves relative elementary membership after doubling, in the ambient general linear group. |
Matrix.GeneralLinearGroup.stabilize_commutator_mem_relativeElementarySubgroup |
theorem | GeneralLinearGroups/RelativeWhiteheadConsequences.lean, line 71 | The ordered commutator of two congruence units is relative elementary after doubling, with no original-rank commutator containment asserted. |
Matrix.GeneralLinearGroup.diagonalPairUnit |
def | GeneralLinearGroups/RectangularBlockUnits.lean, line 35 | Assembles explicit diagonal GL units over independent finite X and Y using existing stabilization and reindexing; works over Semiring and includes empty blocks. |
Matrix.GeneralLinearGroup.diagonalPairUnit_val |
theorem | GeneralLinearGroups/RectangularBlockUnits.lean, line 41 | The assembled unit is the diagonal block matrix with zero off-diagonal blocks. |
Matrix.GeneralLinearGroup.diagonalPairUnit_inv |
theorem | GeneralLinearGroups/RectangularBlockUnits.lean, line 56 | The inverse is the diagonal pair of the supplied inverse units. |
Matrix.GeneralLinearGroup.diagonalPairUnit_one_right |
theorem | GeneralLinearGroups/RectangularBlockUnits.lean, line 64 | An identity right block recovers the existing stabilization map. |
Matrix.GeneralLinearGroup.diagonalPairUnit_one_left |
theorem | GeneralLinearGroups/RectangularBlockUnits.lean, line 70 | An identity left block recovers reindexed stabilization of the right unit. |
Matrix.GeneralLinearGroup.rectangularUpperUnit |
def | GeneralLinearGroups/RectangularBlockUnits.lean, line 82 | Upper off-block unipotent GL unit for rectangular C over any Ring; its inverse has block -C. |
Matrix.GeneralLinearGroup.rectangularUpperUnit_val |
theorem | GeneralLinearGroups/RectangularBlockUnits.lean, line 89 | Reads the upper off-diagonal C and identity diagonal blocks. |
Matrix.GeneralLinearGroup.rectangularUpperUnit_inv |
theorem | GeneralLinearGroups/RectangularBlockUnits.lean, line 113 | The inverse upper unit has off-block -C. |
Matrix.GeneralLinearGroup.rectangularUpperUnit_zero |
theorem | GeneralLinearGroups/RectangularBlockUnits.lean, line 119 | The zero rectangular block gives the identity unit. |
Matrix.GeneralLinearGroup.rectangularUpperUnit_add |
theorem | GeneralLinearGroups/RectangularBlockUnits.lean, line 125 | Addition of rectangular blocks becomes ordered multiplication of upper units. |
Matrix.GeneralLinearGroup.rectangularUpperUnit_single |
theorem | GeneralLinearGroups/RectangularBlockUnits.lean, line 131 | A single off-block entry is the existing elementary generator. |
Matrix.GeneralLinearGroup.rectangularUpperUnit_mem_elementarySubgroup |
theorem | GeneralLinearGroups/RectangularBlockUnits.lean, line 140 | Every upper rectangular unit lies in the existing finite elementary subgroup, including empty-block cases. |
Matrix.GeneralLinearGroup.triangularUnit |
def | GeneralLinearGroups/RectangularBlockUnits.lean, line 153 | Uses explicit diagonal units A and D and ordered B * D⁻¹ to assemble an upper triangular unit over any Ring. |
Matrix.GeneralLinearGroup.triangularUnit_eq_upper_mul_diagonal |
theorem | GeneralLinearGroups/RectangularBlockUnits.lean, line 158 | First factorization is upper unit of B * D⁻¹ times the diagonal pair. |
Matrix.GeneralLinearGroup.triangularUnit_val |
theorem | GeneralLinearGroups/RectangularBlockUnits.lean, line 165 | Reads the upper triangular block matrix A, B, 0, D. |
Matrix.GeneralLinearGroup.triangularUnit_eq_diagonal_mul_upper |
theorem | GeneralLinearGroups/RectangularBlockUnits.lean, line 175 | Complementary ordered factorization is diagonal pair times upper unit of A⁻¹ * B. |
Matrix.GeneralLinearGroup.triangularUnit_inv_val |
theorem | GeneralLinearGroups/RectangularBlockUnits.lean, line 190 | Ordered inverse off-block is -(A⁻¹ * B * D⁻¹), not a reversed or unsigned product. |
Matrix.GeneralLinearGroup.map_triangularUnit_eq_diagonalPairUnit |
theorem | GeneralLinearGroups/RectangularBlockUnits.lean, line 205 | A group hom killing E forgets the off-block, with no abelian-target or ambient-normality hypothesis. |
Matrix.GeneralLinearGroup.rectangularUpperUnit_eq_upperUnit |
theorem | GeneralLinearGroups/RectangularBlockUnits.lean, line 217 | Equal-index rectangular upper units agree with existing Whitehead upperUnit. |
Matrix.GeneralLinearGroup.diagonalPairUnit_inv_pair |
theorem | GeneralLinearGroups/RectangularBlockUnits.lean, line 223 | Equal-index inverse diagonal pairs agree with existing blockDiagonalUnit. |
Ideal.principalUnitsQuotientEquiv |
def | GeneralLinearGroups/PrincipalUnits.lean, line 212 | For arbitrary left ideals in a Ring with I^2 contained in J and I contained in the Jacobson radical, the quotient of original units principal modulo I by the coordinate kernel is the additive layer I/(I intersect J), written multiplicatively. The inverse on a representative is the original-ring unit with value 1+x. |
Ideal.principalUnitsToQuotient_ker |
theorem | GeneralLinearGroups/PrincipalUnits.lean, line 175 | Under I^2 contained in J alone, the coordinate kernel is the relative J-stabilizer inside the I-stabilizer. Its normality is derived, not assumed; no J contained in I or two-sidedness is needed. |
Ideal.commutator_stabilizer_quotient_one_le |
theorem | GeneralLinearGroups/PrincipalUnits/Filtration.lean, line 135 | For arbitrary left ideals A, B in any Ring, including noncommutative and zero rings, the commutator of their principal-unit subgroups lies in the principal units at AB+BA. Principal units use the stock R-unit stabilizer of 1 in the quotient left module R/I; for two-sided I this agrees with the kernel of reduction on units to the quotient ring. The commutator inclusion requires neither two-sidedness nor ambient normality. |
Ideal.commutator_stabilizer_quotient_one_pow_le |
theorem | GeneralLinearGroups/PrincipalUnits/Filtration.lean, line 215 | For a two-sided ideal I in a Ring, the commutator of principal units at I^a and I^b lies in those at I^(a+b) for all natural indices a, b, including zero. No nilpotence assumption is imposed; two-sidedness is required for this all-index bound. |
Ideal.stabilizer_quotient_one_lowerCentralSeries_le_pow |
theorem | GeneralLinearGroups/PrincipalUnits/Filtration.lean, line 229 | For any left ideal I in a Ring and k a natural number, the kth lower central term of its principal-unit subgroup, computed in the ambient unit group, lies in the principal units at I^(k+1). The zeroth term is the principal-unit subgroup itself; no two-sidedness or ambient normality is assumed. |
Ideal.stabilizer_quotient_one_lowerCentralSeries_eq_bot_of_pow_eq_bot |
theorem | GeneralLinearGroups/PrincipalUnits/Filtration.lean, line 249 | If a left ideal I in a Ring satisfies I^N=bot, the lower central series of its principal-unit subgroup is bot at index N-1, using natural subtraction. N=0 and N=1 are included and give a trivial zeroth term. |
Ideal.isNilpotent_stabilizer_quotient_one_of_pow_eq_bot |
theorem | GeneralLinearGroups/PrincipalUnits/Filtration.lean, line 267 | For any left ideal I in a Ring with I^N=bot, its principal-unit subgroup is a nilpotent group. This includes N=0 and N=1 and asserts no nilpotence of the full ambient unit group. |
Ideal.nilpotencyClass_stabilizer_quotient_one_le_of_pow_eq_bot |
theorem | GeneralLinearGroups/PrincipalUnits/Filtration.lean, line 278 | For any left ideal I in a Ring with I^N=bot, the nilpotency class of its principal-unit subgroup is at most N-1, using natural subtraction. Nilpotence is supplied by isNilpotent_stabilizer_quotient_one_of_pow_eq_bot; N=0 and N=1 give the trivial subgroup and class zero. |
Ideal.mem_map_stabilizer_quotient_one_iff |
theorem | GeneralLinearGroups/PrincipalUnits/Images.lean, line 45 | For a ring homomorphism f from a Ring R to a Ring S in independent universes and a left ideal I contained in Ideal.jacobson bot, a unit u of S lies in the image under Units.map f.toMonoidHom of the original R-unit stabilizer of [1] in the quotient left module R/I if and only if there is a in I with f(a) = u - 1. This is the set image of ideal elements, not membership in Ideal.map f I; neither injectivity of f nor commutativity of either ring is required, and there is no domain, local-ring or valuation hypothesis. |
RingHom.unitsKerEquivOfSquareZero |
def | GeneralLinearGroups/SquareZeroUnits.lean, line 59 | Square-zero kernel, Ring domain and Semiring codomain; algebraic unit coordinates, not a quotient-unit lifting theorem. |
DualNumber.fstRingHom_ker_sq |
theorem | GeneralLinearGroups/DualNumberKernels.lean, line 38 | |
Matrix.DualNumberKernels.unitsKerEquiv_eq_unitsKerEquivOfSquareZero_symm |
theorem | GeneralLinearGroups/DualNumberSquareZeroUnits.lean, line 36 | Pointwise comparison on every coefficient through the canonical inr inclusion. |
DualNumber.mapRingHom |
def | GeneralLinearGroups/DualNumberKernels.lean, line 44 | |
Matrix.DualNumberKernels.glKerEquiv |
def | GeneralLinearGroups/DualNumberKernels.lean, line 145 | |
Matrix.DualNumberKernels.unitsKerEquiv |
def | GeneralLinearGroups/DualNumberKernels.lean, line 250 | |
Matrix.DualNumberKernels.det_liftMatrix |
theorem | GeneralLinearGroups/DualNumberKernels.lean, line 291 | |
Matrix.DualNumberKernels.detKer |
def | GeneralLinearGroups/DualNumberKernels.lean, line 305 | |
Matrix.DualNumberKernels.detKer_glKerEquiv |
theorem | GeneralLinearGroups/DualNumberKernels.lean, line 316 | |
Matrix.DualNumberKernels.slKerEquiv |
def | GeneralLinearGroups/DualNumberKernels.lean, line 374 | |
Matrix.DualNumberKernels.slToGL |
def | GeneralLinearGroups/DualNumberKernels.lean, line 337 | |
Matrix.DualNumberKernels.slToGL_slKerEquiv |
theorem | GeneralLinearGroups/DualNumberKernels.lean, line 409 | |
Matrix.DualNumberKernels.glKernel_mul_comm |
theorem | GeneralLinearGroups/DualNumberKernels.lean, line 169 | |
Matrix.DualNumberKernels.slKernel_mul_comm |
theorem | GeneralLinearGroups/DualNumberKernels.lean, line 403 | |
Matrix.DualNumberKernels.glKerMap |
def | GeneralLinearGroups/DualNumberKernels.lean, line 421 | |
Matrix.DualNumberKernels.slKerMap |
def | GeneralLinearGroups/DualNumberKernels.lean, line 445 | |
Matrix.DualNumberKernels.unitsKerMap |
def | GeneralLinearGroups/DualNumberKernels.lean, line 433 | |
Matrix.DualNumberKernels.glKerMap_glKerEquiv |
theorem | GeneralLinearGroups/DualNumberKernels.lean, line 489 | |
Matrix.DualNumberKernels.slKerMap_slKerEquiv |
theorem | GeneralLinearGroups/DualNumberKernels.lean, line 511 | |
Matrix.DualNumberKernels.unitsKerMap_unitsKerEquiv |
theorem | GeneralLinearGroups/DualNumberKernels.lean, line 500 | |
Matrix.DualNumberKernels.detKer_natural |
theorem | GeneralLinearGroups/DualNumberKernels.lean, line 522 | |
Matrix.DualNumberKernels.slToGL_natural |
theorem | GeneralLinearGroups/DualNumberKernels.lean, line 531 | |
Matrix.DualNumberKernels.slAdjoint |
def | GeneralLinearGroups/DualNumberKernelAdjoint.lean, line 29 | |
Matrix.DualNumberKernels.slAdjoint_val |
theorem | GeneralLinearGroups/DualNumberKernelAdjoint.lean, line 48 | |
Matrix.DualNumberKernels.glKerEquiv_conj |
theorem | GeneralLinearGroups/DualNumberKernelAdjoint.lean, line 114 | |
Matrix.DualNumberKernels.glReadback_conj |
theorem | GeneralLinearGroups/DualNumberKernelAdjoint.lean, line 136 | |
Matrix.DualNumberKernels.slToGL_conj |
theorem | GeneralLinearGroups/DualNumberKernelAdjoint.lean, line 147 | |
Matrix.DualNumberKernels.slReadback_conj |
theorem | GeneralLinearGroups/DualNumberKernelAdjoint.lean, line 158 | |
Matrix.DualNumberKernels.glKerMap_conj |
theorem | GeneralLinearGroups/DualNumberKernelAdjoint.lean, line 173 | |
Steinberg.Presented |
abbrev | GeneralLinearGroups/Steinberg.lean, line 58 | |
Steinberg.generator_add |
theorem | GeneralLinearGroups/Steinberg.lean, line 65 | |
Steinberg.generator_commutator_disjoint |
theorem | GeneralLinearGroups/Steinberg.lean, line 91 | |
Steinberg.generator_commutator |
theorem | GeneralLinearGroups/Steinberg.lean, line 99 | |
Steinberg.generator_commutator_reverse |
theorem | GeneralLinearGroups/Steinberg.lean, line 112 | |
Steinberg.lift |
def | GeneralLinearGroups/Steinberg.lean, line 121 | |
Steinberg.lift_generator |
theorem | GeneralLinearGroups/Steinberg.lean, line 141 | |
Steinberg.hom_ext |
theorem | GeneralLinearGroups/Steinberg.lean, line 148 | |
Steinberg.lift_unique |
theorem | GeneralLinearGroups/Steinberg.lean, line 155 | |
Steinberg.toElementary |
def | GeneralLinearGroups/Steinberg.lean, line 174 | |
Steinberg.toElementary_surjective |
theorem | GeneralLinearGroups/Steinberg.lean, line 206 | |
Steinberg.toGL_range |
theorem | GeneralLinearGroups/Steinberg.lean, line 217 | |
Matrix.DualNumberMixedCommutator.innerConstant |
def | GeneralLinearGroups/DualNumberMixedCommutator.lean, line 28 | |
Matrix.DualNumberMixedCommutator.innerPure |
def | GeneralLinearGroups/DualNumberMixedCommutator.lean, line 32 | |
Matrix.DualNumberMixedCommutator.epsilonLiftGL |
def | GeneralLinearGroups/DualNumberMixedCommutator.lean, line 36 | |
Matrix.DualNumberMixedCommutator.etaLiftGL |
def | GeneralLinearGroups/DualNumberMixedCommutator.lean, line 46 | |
Matrix.DualNumberMixedCommutator.epsilonLiftGL_val |
theorem | GeneralLinearGroups/DualNumberMixedCommutator.lean, line 51 | |
Matrix.DualNumberMixedCommutator.epsilonLiftGL_inv_val |
theorem | GeneralLinearGroups/DualNumberMixedCommutator.lean, line 56 | |
Matrix.DualNumberMixedCommutator.etaLiftGL_val |
theorem | GeneralLinearGroups/DualNumberMixedCommutator.lean, line 62 | |
Matrix.DualNumberMixedCommutator.etaLiftGL_inv_val |
theorem | GeneralLinearGroups/DualNumberMixedCommutator.lean, line 67 | |
Matrix.DualNumberMixedCommutator.epsilon_reduce |
theorem | GeneralLinearGroups/DualNumberMixedCommutator.lean, line 140 | |
Matrix.DualNumberMixedCommutator.eta_reduce |
theorem | GeneralLinearGroups/DualNumberMixedCommutator.lean, line 148 | |
Matrix.DualNumberMixedCommutator.epsilon_eta_commutator |
theorem | GeneralLinearGroups/DualNumberMixedCommutator.lean, line 154 | |
Matrix.DualNumberMixedCommutator.mixedKernel |
def | GeneralLinearGroups/DualNumberMixedCommutator.lean, line 180 | |
Matrix.DualNumberMixedCommutator.mixedKernel_val |
theorem | GeneralLinearGroups/DualNumberMixedCommutator.lean, line 184 | |
Matrix.DualNumberMixedCommutator.mixedKernel_readback |
theorem | GeneralLinearGroups/DualNumberMixedCommutator.lean, line 190 | |
Matrix.DualNumberMixedCommutator.mixedKernel_fst |
theorem | GeneralLinearGroups/DualNumberMixedCommutator.lean, line 198 | |
Matrix.DualNumberMixedCommutator.mixedKernel_snd_fst |
theorem | GeneralLinearGroups/DualNumberMixedCommutator.lean, line 205 | |
Matrix.DualNumberMixedCommutator.mixedKernel_snd_snd |
theorem | GeneralLinearGroups/DualNumberMixedCommutator.lean, line 212 | |
Matrix.DualNumberMixedSLCommutator.innerPureSL |
def | GeneralLinearGroups/DualNumberMixedSLCommutator.lean, line 29 | |
Matrix.DualNumberMixedSLCommutator.epsilonLiftSL |
def | GeneralLinearGroups/DualNumberMixedSLCommutator.lean, line 38 | |
Matrix.DualNumberMixedSLCommutator.etaLiftSL |
def | GeneralLinearGroups/DualNumberMixedSLCommutator.lean, line 44 | |
Matrix.DualNumberMixedSLCommutator.epsilonLiftSL_val |
theorem | GeneralLinearGroups/DualNumberMixedSLCommutator.lean, line 49 | |
Matrix.DualNumberMixedSLCommutator.etaLiftSL_val |
theorem | GeneralLinearGroups/DualNumberMixedSLCommutator.lean, line 54 | |
Matrix.DualNumberMixedSLCommutator.epsilonLiftSL_toGL |
theorem | GeneralLinearGroups/DualNumberMixedSLCommutator.lean, line 62 | |
Matrix.DualNumberMixedSLCommutator.etaLiftSL_toGL |
theorem | GeneralLinearGroups/DualNumberMixedSLCommutator.lean, line 68 | |
Matrix.DualNumberMixedSLCommutator.epsilonLiftSL_reduce |
theorem | GeneralLinearGroups/DualNumberMixedSLCommutator.lean, line 74 | |
Matrix.DualNumberMixedSLCommutator.etaLiftSL_reduce |
theorem | GeneralLinearGroups/DualNumberMixedSLCommutator.lean, line 87 | |
Matrix.DualNumberMixedSLCommutator.epsilon_eta_SL_commutator |
theorem | GeneralLinearGroups/DualNumberMixedSLCommutator.lean, line 93 |
Quoted from the main results in formalization.yaml of FormalFrontier/general-linear-groups at commit a2199cf0, Apache-2.0.
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.