Main results
The main results that the formalization.yaml of FormalFrontier/stable-range lists under status.main_results at commit 4d01f179, each that the scan finds declared in the file the yaml gives, with its line. They are listed here, not made articles: in several Formal Frontier libraries this list is close to the whole API. The notes are the yaml's.
| Declaration | Kind | Where | Note |
|---|---|---|---|
Bass.StableRangeCondition |
def | StableRange/Basic.lean, line 62 | Bass S_n uses finite right-unimodular rows with witness coefficients on the right; IsStableRange is a relational least natural index, not a default value when no finite bound exists. |
Bass.stableRangeCondition_one_of_finite_maximalSpectrum |
theorem | StableRange/Semilocal.lean, line 39 | Under CommRing and finite maximal spectrum, the proved S_1 condition shortens the second entry of a right-unimodular pair by b - a*t, including the zero ring. |
Bass.stableRangeCondition_one_corner |
theorem | StableRange/Corner.lean, line 35 | For any idempotent e in a possibly noncommutative ring satisfying S_1, Mathlib's corner eRe with identity e also satisfies S_1. Neither centrality, fullness nor nontriviality is required. |
Bass.stableRangeCondition_mono |
theorem | StableRange/Basic.lean, line 150 | S_m implies S_n for m <= n, over arbitrary possibly noncommutative rings. |
Bass.stableRangeCondition_of_surjective |
theorem | StableRange/Quotient.lean, line 62 | Stable-range conditions descend along surjective ring homomorphisms. |
Bass.stableRangeCondition_quotient_iff |
theorem | StableRange/Quotient.lean, line 135 | Quotienting by a quasiregular two-sided ideal preserves every S_n; reflection is not asserted for arbitrary quotient ideals. |
Bass.stableRange_one_of_isLocalRing |
theorem | StableRange/Local.lean, line 252 | A native possibly noncommutative local ring has least stable range one. The native local-ring hypotheses exclude the zero ring. |
IsLocalRing.le_ringJacobson |
theorem | StableRange/Local.lean, line 308 | Every proper left ideal of a possibly noncommutative local ring lies in its Jacobson radical, without a two-sidedness hypothesis. Locality includes nontriviality. |
IsLocalRing.isMaximal_iff_eq_ringJacobson |
theorem | StableRange/Local.lean, line 332 | In any possibly noncommutative local ring, a left ideal is maximal exactly when it is the Jacobson radical. The radical is maximal, and every maximal left ideal is identified with this same ideal; no two-sidedness hypothesis is imposed. Locality includes nontriviality. |
IsLocalRing.of_ringJacobson_isMaximal |
theorem | StableRange/Local.lean, line 366 | For any possibly noncommutative ring, maximality of its canonical Jacobson radical among all left ideals supplies unit-theoretic locality. No locality or separate nontriviality premise is required; maximality includes properness. |
IsLocalRing.iff_ringJacobson_isMaximal |
theorem | StableRange/Local.lean, line 398 | A ring is local exactly when its canonical Jacobson radical is maximal among all left ideals, not only two-sided ideals. This ring criterion does not subsume Mathlib's commutative-semiring unique-maximal-ideal provider. |
Bass.stableRangeCondition_one_isDedekindFinite |
theorem | StableRange/Regular.lean, line 46 | S_1 makes every one-sided inverse two-sided. |
Bass.isUnitRegular_iff_stableRangeCondition_one |
theorem | StableRange/Regular.lean, line 365 | For a von Neumann-regular ring, unit-regularity is equivalent to S_1. Replacing S_1 by least stable range one additionally requires Nontrivial. |
Bass.principalRightIdeals_isCompl_of_innerInverse |
theorem | StableRange/Regular.lean, line 185 | An inner inverse x for a gives complementary aR and (1-a*x)R, represented as submodules over the opposite ring. |
Bass.not_isUnitRegular_moduleEnd_finsupp_nat |
theorem | StableRange/Regular.lean, line 287 | The endomorphism ring of a countable direct sum of copies of any nonzero additive module is not unit-regular. Neither the coefficient module nor this direct sum is asserted to be free. |
CategoryTheory.nonempty_iso_of_biprod_iso_of_end_stableRangeCondition_one |
theorem | StableRange/CategoryTheory/Cancellation.lean, line 101 | In a preadditive category with independent object and Hom universes, S_1 for the canonical End(X) makes X cancel from X biprod Y isomorphic to X biprod Z. Only those two biproducts are required, with no restrictions on Y or Z. The End ring need not be commutative or nontrivial. This generalizes the existing module cancellation proof. |
CategoryTheory.nonempty_iso_of_biprod_iso_of_isLocalRing_end |
theorem | StableRange/CategoryTheory/Cancellation.lean, line 119 | A possibly noncommutative local endomorphism ring supplies S_1 and hence biproduct cancellation with the same two-sum floor. |
Bass.exists_linearEquiv_of_prod_of_end_stableRangeCondition_one |
theorem | StableRange/Cancellation.lean, line 53 | If End_R(M) satisfies S_1, an equivalence M x A = M x B gives an equivalence A = B, with no finiteness or projectivity hypothesis. This is a specialization of categorical cancellation, retaining all independent scalar and carrier universes. |
Bass.IsUnitRegular.subsingleton_of_fin_linearEquiv_fin_prod |
theorem | StableRange/Cancellation.lean, line 107 | Finite powers of the regular right module over a unit-regular ring cannot absorb a nontrivial complementary module, including power zero. |
Bass.isVonNeumannRegular_moduleEnd |
theorem | StableRange/DivisionRing.lean, line 125 | The endomorphism ring of any vector space over a division ring is regular. |
Bass.isUnitRegular_matrix |
theorem | StableRange/DivisionRing.lean, line 133 | Every finite square matrix ring over a division ring is unit-regular, including the empty index case; finite dimension supplies automorphic inner inverses, unlike the arbitrary-vector-space assertion. |
Matrix.repeatBlockHom |
def | StableRange/RepeatedBlock.lean, line 59 | Repeating square matrices on finite diagonal blocks is a ring homomorphism at NonAssocSemiring generality. Its value is Kronecker product with an identity; injectivity needs a nonempty block family. |
Matrix.rowRank |
def | StableRange/DivisionRingRank.lean, line 49 | Finrank of the range of the left-linear row-vector map given by right multiplication, over a possibly noncommutative division ring. The API includes multiplication bounds, reindex invariance and additivity on mutually orthogonal idempotents. |
Matrix.exists_rowRank_eq |
theorem | StableRange/DivisionRingRank.lean, line 158 | Every natural rank bounded by the finite square size is realized. |
Matrix.rowRank_repeatBlock |
theorem | StableRange/DivisionRingRank.lean, line 327 | Repeated blocks scale row rank by their number, including an empty block family. |
Matrix.normalizedRowRank_repeatBlock |
theorem | StableRange/DivisionRingRank.lean, line 421 | Normalized real rank is preserved for nonempty square matrices and nonempty finite block families. Normalized rank of the identity is one only under the nonempty-size hypothesis; empty-size division is totalized in Lean and does not give that assertion. |
Bass.isVonNeumannRegular_iff_isReduced_and_krullDimLE_zero |
theorem | StableRange/Commutative.lean, line 111 | Commutative regular rings are exactly reduced rings of Krull dimension at most zero. |
Bass.IsVonNeumannRegular.flat |
theorem | StableRange/Commutative.lean, line 142 | Every module over a commutative regular ring is flat, with no finite-generation assumption. |
Bass.stableRangeCondition_one_of_krullDimLE_zero |
theorem | StableRange/CommutativeStableRange.lean, line 112 | Krull dimension at most zero implies S_1 for commutative rings, without reducedness or nontriviality. The separate least-index-one result requires Nontrivial; the zero ring satisfies S_0. |
Bass.IsVonNeumannRegular.isUnitRegular |
theorem | StableRange/CommutativeStableRange.lean, line 50 | Every commutative regular ring is unit-regular. |
Bass.stableRangeCondition_succ_of_krullDimLE |
theorem | StableRange/BassDimension.lean, line 561 | A commutative noetherian ring of Krull dimension at most d satisfies S_(d+1). No reducedness, nontriviality or infinite-residue-field assumption is imposed; the proof uses finite-prime avoidance and height. |
LinearMap.kerProdEquivOfRightInverse |
def | StableRange/Module/SplitSurjective.lean, line 96 | Over a semiring, a specified linear right inverse gives ker(f) x N equivalent to the additive-group source M, with additive-monoid target N and independent universes. Forward coordinates add the kernel element to the section image; inverse coordinates are x - s(f(x)) and f(x). Neither finiteness, projectivity nor freeness is required. |
LinearMap.kerProdEquivOfRightInverse_ofInjective |
theorem | StableRange/Module/SplitSurjective.lean, line 216 | Under the ring hypotheses of Mathlib's right-split-exact equivalence, identifying any injective first map with the kernel transports the kernel-product equivalence to that construction using the same section. |
LinearMap.isRightUnimodular_iff_surjective_dotProductBilin |
theorem | StableRange/RowKernel.lean, line 605 | For any ring R and finite row a, the right-linear map over Rᵐᵒᵖ evaluates to sum a_i*x_i. Right-unimodularity is equivalent to its surjectivity; companion section and right-span criteria include the empty row and the zero ring. |
LinearEquiv.rightCoefficientKernelProd |
def | StableRange/RowKernel.lean, line 541 | A right-inverse column b gives the section y ↦ (b_i*y) and an explicit right-linear equivalence ker(σ) × R ≃ R^n whose inverse second coordinate is the original row σ. No free kernel or matrix completion follows from this arbitrary-ring splitting. |
LinearEquiv.rightCoefficientRowCoordinates |
def | StableRange/RightRowCompletion.lean, line 44 | A chosen right-inverse column and finite coordinates of the right kernel give a right-linear equivalence whose first coordinate is the original row and whose tail is the chosen coordinate of its witness-dependent kernel projection. |
Matrix.rightRowCompletion |
def | StableRange/RightRowCompletion.lean, line 131 | The supplied witness and kernel coordinates yield a rectangular matrix with first row equal to the original row, paired with an explicit two-sided inverse that retains the supplied witness as its first column. Matrix actions agree with the coordinate maps. |
LinearEquiv.rightCoefficientKernelEquivOfMatrixInverse |
def | StableRange/RightRowCompletion.lean, line 254 | A two-sided rectangular inverse with specified first row gives actual right-kernel coordinates by tail(A ᵥ k), reconstructed by B ᵥ Fin.cons 0 t; no prior freeness assumption is required. |
Matrix.isRightUnimodular_and_free_kernel_iff_exists_rectangular_inverse |
theorem | StableRange/RightRowCompletion.lean, line 416 | Over any ring, right-unimodularity with a free right kernel is equivalent to some finite rectangular two-sided inverse pair retaining the row. Splitting derives finite generation of the kernel; no commutativity, stable-range or invariant-basis-number condition is imposed. |
LinearEquiv.isRightUnimodular_iff_exists_kernelProdEquiv |
theorem | StableRange/RowKernel.lean, line 678 | A finite row is right-unimodular exactly when it has a kernel-product equivalence over the opposite ring with inverse second coordinate equal to the original row, not just an abstract product equivalence. |
LinearEquiv.kernelProdEquivOfIsRightUnimodular_eq_rightCoefficientKernelProd |
theorem | StableRange/RowKernel.lean, line 760 | For commutative rings, kernel transport compares the scalar and right-linear splittings using the same chosen witness in both; the comparison does not identify that witness with a test fixture. |
Bass.coefficientRowKernelEquivSuccOfStableRangeCondition |
def | StableRange/RowKernel.lean, line 448 | Over a commutative ring satisfying S_n, a right-unimodular row of length n+1 has kernel explicitly equivalent to the free module on Fin n. Monotonicity gives free kernels for lengths at least s+1 under S_s, without Noetherianity or a dimension bound. |
Bass.coefficientRowKernelEquivOfMatrixInverse |
def | StableRange/RowKernel.lean, line 172 | Over a commutative ring, any chosen row i of a matrix with a specified two-sided inverse has kernel equivalent to functions on the other indices. No stable-range assumption is used; i : Fin n supplies nonemptiness and n=1 gives the empty complementary index type. |
Matrix.coefficientRowCompletionTwo |
def | StableRange/RowCompletionTwo.lean, line 50 | Over any commutative ring, a specified witness a₀b₀+a₁b₁=1 completes the row (a₀,a₁) to a determinant-one matrix with second row (-b₁,b₀). Its inverse has rows (b₀,-a₁) and (b₁,a₀). |
Bass.coefficientRowKernelEquivTwo |
def | StableRange/RowCompletionTwo.lean, line 222 | The supplied completion identifies the kernel of the original two-element coefficient functional with R, with coordinate -b₁x₀+b₀x₁ and inverse generator (-a₁t,a₀t). |
LinearEquiv.coefficientProductCancellationTwo |
def | StableRange/RowCompletionTwo.lean, line 343 | Any supplied (Fin 2 → R) ≃ₗ[R] (R × P) over a commutative ring identifies P ≃ₗ[R] R via its original first projection and kernel; no stable-range, freeness or nontriviality hypothesis is required. |
Module.finLinearEquivOfStableRangeCondition |
def | StableRange/FiniteFree.lean, line 47 | For a commutative R satisfying S_s, an explicit equivalence P x R^m = R^(n+m) with s <= n yields P = R^n, with the exact coordinate count, independent module universe and zero ring allowed. The noetherian Krull-dimension-bound specialization has separate hypotheses. |
LinearEquiv.coefficientRowCompletionOfStableRangeCondition |
def | StableRange/RowCompletion.lean, line 44 | A right-unimodular row of length n+1 over a commutative ring satisfying S_s with s <= n yields a self-equivalence whose first output coordinate is the original coefficient functional. Its matrix has that first row and the same specified inverse satisfies both inverse identities. |
Matrix.GeneralLinearGroup.exists_elementary_unit_pivot_of_stableRangeCondition_one |
theorem | StableRange/ElementaryGeneration.lean, line 40 | Bass S_1 over a commutative ring yields an elementary left factor with a unit leading entry for every invertible successor-rank matrix, including rank one and the zero ring; locality is not required. |
Matrix.GeneralLinearGroup.exists_elementary_diagonalization_of_stableRangeCondition_one |
theorem | StableRange/ElementaryGeneration.lean, line 93 | Two-sided elementary factors diagonalize every invertible Fin n matrix into units under commutative S_1, including the empty matrix. The generic all-rank unit-pivot induction comes from general-linear-groups. |
Matrix.GeneralLinearGroup.exists_elementary_diagonalization_finite_of_stableRangeCondition_one |
theorem | StableRange/ElementaryGeneration.lean, line 104 | The same diagonalization transports along a finite equivalence to any finite decidable index type, without a chosen order or Nontrivial. |
Matrix.GeneralLinearGroup.mem_elementarySubgroup_iff_det_eq_one_of_stableRangeCondition_one |
theorem | StableRange/DeterminantGeneration.lean, line 78 | Over a commutative S_1 ring, an invertible matrix at any finite decidable index type is elementary exactly when its determinant is one; the empty index type and the zero ring are included. |
Matrix.GeneralLinearGroup.StableGL.elementary_eq_ker_det_of_stableRangeCondition_one |
theorem | StableRange/DeterminantGeneration.lean, line 104 | The stable elementary subgroup is the kernel of the stable determinant, by reducing a stable representative to a finite stage. |
Matrix.GeneralLinearGroup.StableGL.quotientDetMulEquivOfStableRangeConditionOne |
def | StableRange/DeterminantGeneration.lean, line 142 | The stable elementary quotient is equivalent to the coefficient units; the forward map is the quotient determinant and the inverse is the existing rank-one section. |
Quoted from the main results in formalization.yaml of FormalFrontier/stable-range at commit 4d01f179, Apache-2.0.
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.