Main results 101 to 200
| Declaration | Kind | Where | Note |
|---|---|---|---|
KTheory.ProjectiveClass.finrankHom_comp_map |
theorem | ProjectiveModules/KTheory/Rank.lean, line 469 | Scalar extension along any unital φ : D →+* S between division rings preserves natural class dimension as an equality of whole canonical additive homomorphisms, with independent scalar universes. |
KTheory.K0.finrankHom_comp_map |
theorem | ProjectiveModules/KTheory/Rank.lean, line 504 | The induced K₀ scalar-extension map along the same arbitrary unital division-ring homomorphism preserves integer dimension as an equality of whole canonical homomorphisms, by group completion. |
KTheory.ProjectiveClass.map_bijective |
theorem | ProjectiveModules/KTheory/Rank.lean, line 487 | Scalar extension along any unital homomorphism between division rings induces a bijective additive class map, using the canonical natural dimension equivalences and their whole-map compatibility. The scalar homomorphism need not be surjective; its universes are independent. |
KTheory.K0.map_bijective |
theorem | ProjectiveModules/KTheory/Rank.lean, line 513 | The induced K₀ map between division rings is bijective, using the canonical integer dimension equivalences and naturality. This concerns all group elements, including negative regular-generator multiples, not only the positive class generators. |
KTheory.K0.subsingleton_of_subsingleton |
instance | ProjectiveModules/KTheory/ZeroRing.lean, line 71 | The entire K₀ group of a subsingleton ring is a subsingleton, as is the direct-sum class monoid. Generator normalization does not use the nonadditive zero-ring convention for module finrank. |
ModuleCat.Stable.quotient_map_eq_iff |
lemma | ProjectiveModules/Category/Stable.lean, line 157 | Stable equality is factorization of the difference through a projective; the quotient is preadditive. |
ModuleCat.FactorsThroughProjective.iff_ext_one_precomp_eq_zero |
lemma | ProjectiveModules/Category/Stable.lean, line 221 | Detect projective factorization by all Ext-one precomposition maps; retains the Small.{uM} R universe hypothesis. No abelian stable-category structure, completed-group-ring duality or transpose theory is asserted. |
BalancedTensorProduct.lift |
def | ProjectiveModules/Module/BalancedTensorProduct.lean, line 171 | Universal additive balanced map for a right and a left module over an arbitrary ring. |
Module.Projective.balancedTensor_short_exact |
theorem | ProjectiveModules/Module/BalancedTensorExact.lean, line 397 | Tensoring a left-module short exact pair with a fixed projective right module preserves exactness. |
Module.Projective.hom_short_exact |
theorem | ProjectiveModules/Module/HomExact.lean, line 96 | Additive Hom exactness for a projective source over an arbitrary semiring. |
Module.piRightModule |
def | ProjectiveModules/Module/RightProduct.lean, line 67 | Named coordinatewise opposite-scalar action on a family of semimodules over a family of semirings. Index, coefficient and carrier universes are independent; the family need not be finite. No global action instance or unital coordinate-inclusion homomorphism is introduced. |
Module.projective_piRight |
theorem | ProjectiveModules/Module/RightProduct.lean, line 120 | For a finite index, coefficient-product assembly preserves arbitrary projectivity over semirings, without finite-generation assumptions. Independently sized binary semiring factors have the corresponding projective closure theorem. |
ModuleCat.FiniteProjective.pi |
def | ProjectiveModules/Module/RightProduct.lean, line 651 | Canonical coefficient-product bundle of a finite family of finite-projective right modules over arbitrary rings. Finite generation and projectivity of the output are proved, with carrier, coordinate, action, extensionality and finite reconstruction APIs. |
ModuleCat.FiniteProjective.prodRight |
def | ProjectiveModules/Module/RightProduct.lean, line 736 | Binary finite-projective coefficient-product assembly with separately quantified scalar and carrier universes. Zero module factors and zero coefficient rings are not excluded. |
ModuleCat.RightExtension.piRecoverLinearEquiv |
def | ProjectiveModules/Module/RightProduct.lean, line 1008 | Extension of an assembled right-module family along a coordinate projection recovers that factor, with forward and inverse pure-tensor formulas. The index need not be finite; no finite-generation or projectivity premise is required. |
ModuleCat.RightExtension.piLinearEquiv |
def | ProjectiveModules/Module/RightProduct.lean, line 803 | An arbitrary right module over a finite product of arbitrary rings is linearly equivalent to the product of its coordinate projection extensions. Both directions use the balanced tensor construction and supported coordinate idempotents; scalar, index and carrier universes are independent, including empty families and zero rings. |
Module.piRightHomAddEquiv |
def | ProjectiveModules/Module/RightProduct/Hom.lean, line 87 | For an arbitrary index and a family of possibly noncommutative semirings, maps linear for the canonical piRightModule coefficient-product action on right-module families with additive commutative monoid fibers correspond additively to families of factor-linear maps. The component at i sends m to f (Pi.single i m) i; the inverse acts coordinatewise. Component evaluation, supported inputs, equality detection, identity and composition laws retain independent index, coefficient, source, target and third-family universes. This is an additive equivalence, with no finiteness, finite-generation, projectivity, presentation or commutativity hypotheses; it is separate from reconstruction of arbitrary modules over finite products of rings by projection scalar extension. |
Module.piRightEndEquiv |
def | ProjectiveModules/Module/RightProduct/Hom.lean, line 285 | Semiring equivalence between endomorphisms of the canonical assembled right module and the family of factor endomorphism semirings, using precisely the additive data of piRightHomAddEquiv. Components evaluate on supported inputs and the inverse acts coordinatewise; identities and multiplication are preserved in the order f * g = f.comp g. The index is arbitrary, semiring coefficients need not commute, and fibers need only be additive commutative monoids with their right module structures. Index, coefficient and carrier universes are independent; no finite-generation, projectivity or presentation assumption is imposed. |
KTheory.ProjectiveClass.piEquiv |
def | ProjectiveModules/KTheory/Product.lean, line 379 | Additive monoid equivalence from finite-projective classes over a finite coefficient product of arbitrary rings to the family of factor classes, with the existing projection scalar-extension maps as its forward homomorphism. The inverse assembles canonical coefficient-product modules; whole-hom, coordinate, module-generator and equality-detection laws include empty families and zero rings. |
KTheory.ProjectiveClass.prodEquiv |
def | ProjectiveModules/KTheory/Product.lean, line 518 | Binary projective-class additive equivalence along the two projection scalar extensions, with separately quantified scalar and module carrier universes. Factors need not be commutative or nontrivial; no cancellation of classes is required. |
KTheory.K0.piEquiv |
def | ProjectiveModules/KTheory/Product.lean, line 793 | Additive group equivalence between K0 of a finite product of arbitrary rings and the family of factor K0 groups. Forward whole-hom and coordinate formulas agree with projection scalar extension; inverse module-generator, group-completion and signed-presentation formulas compute general differences of finite-projective classes, without assuming injectivity of the class-to-K0 map. |
KTheory.K0.prodEquiv |
def | ProjectiveModules/KTheory/Product.lean, line 970 | Binary K0 additive equivalence with independent scalar and carrier universes, inverse generator and signed formulas, and coordinate equality detection. Zero rings and noncommutative factors are included; signed classes do not require cancellation. |
ModuleCat.RightExtension.adjunction |
def | ProjectiveModules/Module/RightExtension.lean, line 535 | Right-module scalar extension/restriction adjunction for arbitrary ring maps, with finite/projective preservation. |
IsIdempotentElem.rightSpanFiniteProjective |
def | ProjectiveModules/Module/RightExtensionIdeal.lean, line 51 | Bundle the principal right ideal of an idempotent over an arbitrary ring as a finite projective right module. |
ModuleCat.RightExtension.spanFiniteProjective |
def | ProjectiveModules/Module/RightExtensionIdeal.lean, line 276 | Bundle scalar extension of an idempotent right ideal as a finite projective right module over arbitrary source and target rings. |
ModuleCat.RightExtension.spanLinearEquivOfMapEqOne |
def | ProjectiveModules/Module/RightExtensionIdeal.lean, line 225 | Along an arbitrary ring map from R to S, the principal right ideal generated by op e extends to the regular right S-module when f e = 1. No idempotence, centrality of the generator or whole homomorphism image, commutativity or nontriviality hypothesis is imposed. The image of e itself is necessarily central. Forward evaluation is m tensor s mapped to op (f (unop m) * s), with the inverse given by the tensor of e with the target scalar. |
ModuleCat.RightExtension.span_subsingleton_of_map_eq_zero |
theorem | ProjectiveModules/Module/RightExtensionIdeal.lean, line 195 | Over arbitrary source and target rings, extension of the right ideal generated by an idempotent e is a subsingleton when f e = 0, including the zero-ring cases. The proof uses idempotent action only on the generator, then principal generation and balancing; the idempotent need not fix every member of the source ideal. |
ModuleCat.RightExtension.tmulOne_surjective |
theorem | ProjectiveModules/Module/RightExtension.lean, line 277 | The canonical scalar-extension map is surjective when the coefficient homomorphism is surjective. |
ModuleCat.RightExtension.idealQuotientLinearEquiv |
def | ProjectiveModules/Module/RightExtensionQuotient.lean, line 236 | Scalar extension along a two-sided ideal quotient agrees with the right-module ideal-action quotient. |
ModuleCat.RightExtension.finrank_idealQuotient_prod_of_isMaximal |
theorem | ProjectiveModules/Module/RightExtensionFiniteResidue.lean, line 122 | Residue dimensions add for finite modules, retaining two-sided/maximal and division-quotient hypotheses. |
ModuleCat.RightExtension.rightFreeLinearEquiv |
def | ProjectiveModules/Module/RightExtensionFree.lean, line 133 | Explicit scalar extension of finite standard right-free modules, including empty coordinates. |
ModuleCat.RightExtension.innerLinearEquiv |
def | ProjectiveModules/Module/RightExtensionConjugacy.lean, line 82 | For arbitrary rings R and S, homomorphisms φ ψ : R →+* S, and a unit u with u * φ r = ψ r * u for every r, the two extensions of any right R-module are right-S-linearly equivalent. A pure tensor m ⊗_φ s maps to m ⊗_ψ (u * s), with inverse coefficient u⁻¹ * s; the right target action is unchanged. Scalar and carrier universes are independent, without commutativity, finite generation, projectivity or centrality assumptions. |
ModuleCat.RightExtension.innerLinearEquiv_toLinearMap_eq_iff |
theorem | ProjectiveModules/Module/RightExtensionConjugacy.lean, line 161 | One-generator values characterize the entire right-linear comparison. The characteristic API also gives both ordered tensor formulas, source balancing, fixed right scalar action, the whole inverse equivalence and the identity for the unit 1. |
ModuleCat.RightExtension.idLinearEquiv |
def | ProjectiveModules/Module/RightExtensionComparison.lean, line 100 | Identity extension of an arbitrary right module over a ring is linearly equivalent to the original module: m ⊗ r maps to op r • m and the inverse sends m to m ⊗ 1. Scalar and module universes are independent; no finite-generation, projectivity or nontriviality premise is needed. |
ModuleCat.RightExtension.compLinearEquiv |
def | ProjectiveModules/Module/RightExtensionComparison.lean, line 249 | For arbitrary ring homomorphisms φ : R →+ S and ψ : S →+ T, iterated right extension is linearly equivalent to extension along ψ.comp φ. The pure-tensor formula is (m ⊗ s) ⊗ t ↦ m ⊗ (ψ s * t), with inverse m ⊗ t ↦ (m ⊗ 1) ⊗ t, preserving multiplication order. Scalar and module universes are independent; no commutativity, injectivity, surjectivity, finiteness or projectivity is assumed. |
ModuleCat.RightExtension.compLinearEquiv_id_left |
theorem | ProjectiveModules/Module/RightExtensionComparisonCoherence.lean, line 58 | Composition comparison with an identity first equals scalar extension of the identity comparison as a linear map. Both send (m ⊗ r) ⊗ s to m ⊗ (φ r * s), for arbitrary rings and right modules with independent scalar and module universes. This is a simp law. |
ModuleCat.RightExtension.compLinearEquiv_id_right |
theorem | ProjectiveModules/Module/RightExtensionComparisonCoherence.lean, line 90 | Composition comparison with an identity last equals the identity comparison on the extended module as a linear equivalence. Both evaluate z ⊗ s by the right S-action on z, over arbitrary rings and right modules with independent scalar and module universes. This is a simp law. |
ModuleCat.RightExtension.compLinearEquiv_assoc |
theorem | ProjectiveModules/Module/RightExtensionComparisonCoherence.lean, line 121 | Comparing the first two extensions and then the third equals comparing the last two and then the first, as linear maps. For arbitrary rings R, S, T, U, ring homomorphisms φ, ψ, θ and a module with only an AddCommGroup and a Module Rᵐᵒᵖ action, all five universes are independent. The pure-tensor identity is θ (ψ s * t) * u = θ (ψ s) * (θ t * u). No commutativity, injectivity, surjectivity, freeness, finiteness or projectivity is required, and no categorical coherence is asserted. |
ModuleCat.RightExtension.tensorProductObj_smul_tmul |
theorem | ProjectiveModules/Module/RightExtensionTensorProduct.lean, line 192 | Right target scalars act on the module-first tensor by coefficient right multiplication s * t, for a commutative base and arbitrary ring target; no central image is assumed. |
ModuleCat.RightExtension.tensorProductLinearEquiv |
def | ProjectiveModules/Module/RightExtensionTensorProduct.lean, line 451 | For CommRing R, Ring S and any right R-module in an independent universe, right extension along a unital φ agrees with the module-first Mathlib tensor using the canonical restricted source and coefficient actions. |
ModuleCat.RightExtension.tensorProductLinearEquiv_tmul |
theorem | ProjectiveModules/Module/RightExtensionTensorProduct.lean, line 592 | The module-first comparison sends the balanced pure tensor m tensor s to tensorProductTmul φ M m s with the specified coefficient action. |
ModuleCat.RightExtension.tensorProductLinearEquiv_symm_tmul |
theorem | ProjectiveModules/Module/RightExtensionTensorProduct.lean, line 603 | The inverse module-first comparison sends that Mathlib pure tensor to the corresponding balanced pure tensor. |
ModuleCat.RightExtension.tensorProductLinearEquiv_naturality |
theorem | ProjectiveModules/Module/RightExtensionTensorProduct.lean, line 613 | For a morphism of right modules in a common carrier universe, the comparison intertwines extension of the source map with its restricted tensor map and the identity of the specified coefficient module. |
ModuleCat.RightExtension.tensorProductLinearEquiv_functor'_map |
theorem | ProjectiveModules/Module/RightExtensionTensorProduct.lean, line 674 | The same module-first intertwining law uses the right-extension functor' map, with independent source and output carrier universes. |
ModuleCat.RightExtension.extendScalarsLinearEquiv |
def | ProjectiveModules/Module/RightExtensionTensorProduct.lean, line 702 | For CommRing R and CommRing S, right extension agrees pointwise with the right-module view of Mathlib's scalar-first ModuleCat.extendScalars φ; the output carrier is in max uM uS. |
ModuleCat.RightExtension.extendScalarsLinearEquiv_tmul |
theorem | ProjectiveModules/Module/RightExtensionTensorProduct.lean, line 788 | The scalar-first comparison sends m tensor s to s tensor m using the canonical homomorphism-induced coefficient module and opposite source view. |
ModuleCat.RightExtension.extendScalarsLinearEquiv_symm_tmul |
theorem | ProjectiveModules/Module/RightExtensionTensorProduct.lean, line 807 | The inverse scalar-first comparison sends s tensor m to the corresponding module-first balanced pure tensor. |
ModuleCat.RightExtension.extendScalarsLinearEquiv_eq_comm |
theorem | ProjectiveModules/Module/RightExtensionTensorProduct.lean, line 832 | On carriers, the scalar-first comparison is TensorProduct.comm after the module-first comparison for the same specified module structures. |
ModuleCat.RightExtension.extendScalarsLinearEquiv_naturality |
theorem | ProjectiveModules/Module/RightExtensionTensorProduct.lean, line 845 | Pointwise scalar-first naturality intertwines right extension of a module morphism with the maps of Mathlib's extension and both opposite scalar restriction functors. |
Module.rightFreeLinearMapScalarExtension |
def | ProjectiveModules/Module/RightEndomorphismMatrix.lean, line 160 | Transport a supplied right-linear map from ι → R to κ → R along any unital homomorphism R →+* S of semirings. Only the source requires a Fintype instance; the target is arbitrary. Scalar and index universes are independent. Empty indices and zero semirings are not excluded. No commutativity, injectivity, surjectivity, IBN or equal index cardinalities are assumed. The noncomputable constructor needs no caller DecidableEq instance. Laws cover zero, addition, identities, coefficient images and coefficient-homomorphism composition. |
Module.rightFreeScalarExtensionEquiv |
def | ProjectiveModules/Module/RightEndomorphismMatrix.lean, line 175 | Under the same semiring and homomorphism hypotheses, transport a supplied right-linear equivalence and its inverse, with Fintype instances on both indices in independent universes. This does not assert that unequal finite ranks admit an equivalence. Laws give compatibility with the underlying transported map, inverse, equivalence composition, identity and coefficient-homomorphism identity and composition, without caller DecidableEq instances. |
Module.rightFreeLinearMapScalarExtension_apply |
theorem | ProjectiveModules/Module/RightEndomorphismMatrix.lean, line 208 | For a finite source and arbitrary target, the i-th coordinate on y is ∑ j, f (g (Pi.single j 1) i) * y j. Coefficients multiply on the left; opposite-semiring module scalars act on the right. The single-vector and entrywise opposite-coordinate row-matrix laws characterize the same transport. |
Module.rightFreeLinearMapScalarExtension_map_comp |
theorem | ProjectiveModules/Module/RightEndomorphismMatrix.lean, line 311 | Transport respects composition when the source and intermediate coordinate types have Fintype instances; the final target is arbitrary. All three index universes remain independent. |
Module.rightFreeScalarExtensionEquiv_apply |
theorem | ProjectiveModules/Module/RightEndomorphismMatrix.lean, line 356 | For a supplied equivalence with both coordinate types finite, the i-th coordinate on y is ∑ j, f (e (Pi.single j 1) i) * y j, agreeing with transport of its underlying right-linear map. |
Module.rightFreeLinearMapScalarExtension_eq_rightExtension_of_decidableEq |
theorem | ProjectiveModules/Module/RightEndomorphismMatrix.lean, line 448 | Over rings with both indices finite, identify coefficient transport with the unbundled ModuleCat.RightExtension.map conjugated by the finite right-free coordinate equivalences. This variant uses the caller's DecidableEq instances on both indices; the corresponding rightFreeLinearMapScalarExtension_eq_rightExtension law chooses them internally. These are data-compatibility bridges, not extra mathematical premises of the semiring constructor. |
Module.rightFreeLinearMapScalarExtension_tmul_of_decidableEq |
theorem | ProjectiveModules/Module/RightEndomorphismMatrix.lean, line 478 | Over rings with both indices finite and caller DecidableEq instances, compatibility on pure tensors sends the coordinates of x ⊗ s to those of g x ⊗ s. The rightFreeLinearMapScalarExtension_tmul law chooses equality decisions internally. No infinite-product tensor equivalence is asserted by arbitrary-target map transport. |
Module.rightFreeScalarExtensionEquiv_toLinearMap_eq_rightExtension_of_decidableEq |
theorem | ProjectiveModules/Module/RightEndomorphismMatrix.lean, line 505 | Over rings with both indices finite, the underlying map of a supplied transported equivalence agrees with the unbundled tensor map in finite right-free coordinates, using caller DecidableEq instances. The rightFreeScalarExtensionEquiv_toLinearMap_eq_rightExtension law chooses equality decisions internally. Independent index and scalar universes are retained. |
Module.rightEndomorphismMatrixEquiv |
def | ProjectiveModules/Module/RightEndomorphismMatrix.lean, line 59 | Column-convention square matrices represent opposite-scalar linear endomorphisms with same-order composition. The square rightEndomorphismScalarExtension specializes rectangular coefficient transport and retains its finite-coordinate Ring tensor bridge. |
Module.rightEndomorphism_bijective_of_quotientScalarExtension_bijective |
theorem | ProjectiveModules/Module/RightEndomorphismMatrix.lean, line 601 | Reflect finite right-module invertibility through a quasiregular two-sided quotient, not arbitrary quotients. |
LinearMap.splitKernelProjection |
def | ProjectiveModules/Module/ProjectiveKernel.lean, line 46 | For Semiring R, AddCommGroup M and AddCommMonoid A with R-module structures, R-linear maps i : A → M and r : M → A with r.comp i = id give a projection M → ker r. Its underlying value is x - i (r x). Scalar and both carrier universes are independent; no finiteness, projectivity, freeness, Noetherian, commutativity or Small premise. The projection follows Formal Frontier's formalization and uses Mathlib's linear-map and kernel APIs. |
LinearMap.splitKernelProjection_apply |
theorem | ProjectiveModules/Module/ProjectiveKernel.lean, line 65 | The coerced projection value is x - i (r x), over any semiring with additive-commutative-group source M and additive-commutative-monoid target A, R-linear i : A → M, r : M → A and r.comp i = id. No finite or projective premise; all three universes are independent. |
LinearMap.splitKernelProjection_comp_subtype |
theorem | ProjectiveModules/Module/ProjectiveKernel.lean, line 75 | The projection composed with (ker r).subtype is the identity on ker r. Only Semiring R, AddCommGroup M, AddCommMonoid A, their R-module structures and R-linear i : A → M, r : M → A with r.comp i = id are required, with independent scalar and carrier universes. |
LinearMap.finite_splitKernel |
theorem | ProjectiveModules/Module/ProjectiveKernel.lean, line 118 | For Semiring R, AddCommGroup M and AddCommMonoid A with R-module structures, R-linear i : A → M, r : M → A and r.comp i = id, Module.Finite R M gives Module.Finite R (ker r). Source projectivity is not required, nor target finiteness or projectivity, freeness, Noetherian or commutative scalars, or Small. All three universes are independent. The proof uses the projection retraction and Mathlib's Module.Finite.of_surjective. |
LinearMap.projective_splitKernel |
theorem | ProjectiveModules/Module/ProjectiveKernel.lean, line 131 | For Semiring R, AddCommGroup M and AddCommMonoid A with R-module structures, R-linear i : A → M, r : M → A and r.comp i = id, Module.Projective R M gives Module.Projective R (ker r). No source finiteness or target finiteness/projectivity is required, nor freeness, Noetherian or commutative scalars, or Small. All three universes are independent. The proof reuses Mathlib's Module.Projective.of_split with the kernel inclusion and projection. |
Module.Projective.pi |
instance | ProjectiveModules/Module/ProjectivePi.lean, line 40 | Supporting projectivity instance for finite dependent products over any semiring, with canonical pointwise module structure and independent scalar, index and carrier universes. Only projectivity of the factors is required, not finite generation, freeness or additive inverses. The proof transports Mathlib's dependent finitely supported projectivity along its finite-index linear equivalence. |
Module.Projective.exists_fin_generating_family_iff_exists_prod_equiv |
theorem | ProjectiveModules/Module/ProjectiveComplement.lean, line 149 | Explicit n-generator/projective-complement equivalence, including the zero-generator case. |
Module.Basis.exists_hasMinimalSupport |
theorem | ProjectiveModules/Module/MinimalSupport.lean, line 37 | Minimal support relative to a supplied fixed-index basis. |
Module.Projective.free_of_isUnit_compl |
theorem | ProjectiveModules/Module/LocalProjective.lean, line 395 | Finite projective right modules are free given a proper two-sided ideal whose complement consists of units. The ring hypotheses exclude the zero ring; the zero module and zero rank remain allowed. |
Module.Projective.exists_fin_rightFree_split_containing |
theorem | ProjectiveModules/Module/LocalProjectiveElement.lean, line 34 | Under the same proper-ideal/unit-complement hypotheses, contain an element in a finite right-free split summand. |
Module.CountablyGenerated |
def | ProjectiveModules/Module/CountablyGenerated.lean, line 32 | Sequence-spanning countable generation, including padded finite families and countable supported free modules. |
Module.CountablyGenerated.submodule_of_isNoetherianRing |
theorem | ProjectiveModules/Module/CountablyGenerated/Noetherian.lean, line 24 | Every submodule of a sequence-spanned module over a possibly noncommutative left-Noetherian ring is countably generated; no ambient Noetherian, free or projective module assumption. |
Module.Projective.exists_fin_rightFree_biorthogonal_exhaustion_of_countablyGenerated |
theorem | ProjectiveModules/Module/CountableLocalProjective.lean, line 425 | Countable finite-free biorthogonal exhaustion for projectives under proper-ideal/unit-complement hypotheses. |
Module.Projective.exists_sigma_fin_rightBasis_of_countablyGenerated |
theorem | ProjectiveModules/Module/CountableLocalProjectiveFree.lean, line 122 | Assemble that exhaustion into a basis indexed by a sigma of finite blocks, allowing rank-zero blocks. |
LinearMap.exists_countable_invariant_supported |
theorem | ProjectiveModules/Module/CountableCoordinateClosure.lean, line 81 | Countable invariant supported closure for an endomorphism of a standard free module; no idempotence assumption. |
LinearMap.exists_countable_invariant_coordinate_filtration |
theorem | ProjectiveModules/Module/TransfiniteCoordinateFiltration.lean, line 175 | Well-ordered exhaustive invariant coordinate filtration with countable increments; ambient basis need not be countable. |
LinearMap.supportedRangeProdComplementEquiv |
def | ProjectiveModules/Module/InvariantSupportedProjection.lean, line 138 | Split nested invariant supported ranges of an idempotent; complementary increments are projective. |
LinearMap.supportedRangeComplement_countablyGenerated |
theorem | ProjectiveModules/Module/InvariantSupportedProjection.lean, line 285 | Countable coordinate differences give countably generated complements with the stated invariance and idempotence. |
LinearMap.CountableInvariantCoordinateFiltration.range_free_of_free_increments |
theorem | ProjectiveModules/Module/TransfiniteRangeBasis.lean, line 314 | An idempotent range is free when its filtration increments are free; not an unconditional free-range claim. |
Module.Projective.free_of_isUnit_compl_arbitraryRank |
theorem | ProjectiveModules/Module/ArbitraryLocalProjectiveFree.lean, line 39 | Arbitrary-rank projective right-module freeness under the proper-ideal/unit-complement hypotheses. |
Module.Projective.free_of_pid |
theorem | ProjectiveModules/Module/PID.lean, line 274 | Every projective over a commutative PID is free, using arbitrary-rank free-submodule freeness. |
LaurentPolynomial.module_free_of_finite_projective |
theorem | ProjectiveModules/Module/LaurentPolynomial.lean, line 56 | Finite projectives over one-variable Laurent polynomials over a field are free, with a separate opposite-ring endpoint. |
IsIdempotentElem.free_span_iff |
theorem | ProjectiveModules/Module/LocallyConstantRank.lean, line 121 | For a commutative semiring R and idempotent e, Module.Free R (Ideal.span {e}) iff e = 0 or e = 1. Includes the zero and unit ideals and the zero semiring; no nontriviality, domain or local hypothesis is required. |
IsIdempotentElem.not_free_span |
theorem | ProjectiveModules/Module/LocallyConstantRank.lean, line 140 | For a commutative semiring and idempotent e with e ≠ 0 and e ≠ 1, the principal ideal Ideal.span {e} is not free. Nontriviality of the ideal is derived from its nonzero generator, not assumed. |
IsIdempotentElem.smul_span |
lemma | ProjectiveModules/Module/LocallyConstantRank.lean, line 108 | Over a commutative semiring, an idempotent e acts identically on its principal ideal: e • x = x for every x : Ideal.span {e}. |
IsIdempotentElem.one_sub_smul_span |
lemma | ProjectiveModules/Module/LocallyConstantRank.lean, line 215 | Over a commutative ring, the complementary idempotent annihilates the principal ideal: (1 - e) • x = 0 for every x : Ideal.span {e}, assuming IsIdempotentElem e. |
ModuleCat.FiniteProjective.rankAtStalk_ofLocallyConstantRank |
theorem | ProjectiveModules/Module/LocallyConstantRank.lean, line 396 | Every locally constant natural-valued prime-spectrum function is realized by a finite projective over a commutative ring. |
ModuleCat.FiniteProjective.prodComplementEquiv |
def | ProjectiveModules/Module/LocallyConstantRank.lean, line 383 | Explicit finite-standard-free complement of the threshold-idempotent realization. |
Module.rankFiberRingEquiv |
def | ProjectiveModules/Module/RankFiberDecomposition.lean, line 208 | Decompose the commutative base ring along a finite projective's nonempty rank fibers. |
Module.rankFiberLinearEquiv |
def | ProjectiveModules/Module/RankFiberDecomposition.lean, line 242 | Reconstruct the finite projective from rank-fiber base changes, including the empty-spectrum zero ring. |
Module.ComponentwiseFree.nonempty_linearEquiv_of_rankAtStalk_eq |
theorem | ProjectiveModules/Module/ComponentwiseFree.lean, line 714 | Componentwise-free modules in independent universes with equal stalk ranks are linearly equivalent. |
ModuleCat.componentwiseFreeSkeletonEquiv |
def | ProjectiveModules/Module/ComponentwiseFree.lean, line 793 | Locally constant ranks classify the skeleton of componentwise-free finite projectives, not all finite projectives. |
Module.End.subsingleton_of_linearEquiv_prod |
theorem | ProjectiveModules/Module/SummandCancellation.lean, line 34 | Over a semiring, a Dedekind-finite endomorphism monoid of M forces P to be subsingleton whenever M is linearly equivalent to M × P. Neither finite generation nor freeness is needed; scalar, M and P universes are independent. |
RankCondition.card_le_of_linearEquiv_prod |
theorem | ProjectiveModules/Free/FiniteFreeSummand.lean, line 52 | Over a semiring with the rank condition, finite bases of M and N give the target basis cardinality at most the source basis cardinality if M is linearly equivalent to N × P for any semimodule P. Scalar, module, complement and basis-index universes are independent. |
IsStablyFiniteRing.subsingleton_of_linearEquiv_prod |
theorem | ProjectiveModules/Free/FiniteFreeSummand.lean, line 74 | A finite-free semimodule over a stably finite semiring cancels from an equivalence with itself times any complementary semimodule; scalar, module and complement universes are independent. |
IsStablyFiniteRing.subsingleton_of_finite_projective_linearEquiv_prod |
theorem | ProjectiveModules/Free/FiniteFreeSummand.lean, line 85 | A finite projective module over a stably finite ring cancels from an equivalence with itself times any complementary module, with independent scalar, module and complement universes. |
rankCondition_iff_le_of_fin_linearEquiv_fin_prod |
theorem | ProjectiveModules/Free/FiniteFreeSummand.lean, line 111 | For a ring, the rank condition is equivalent to n ≤ m whenever a finite coordinate module of size m is linearly equivalent to one of size n times a complementary module in the ring's universe. The converse does not assert splitting for arbitrary semirings. |
isStablyFiniteRing_iff_subsingleton_of_fin_linearEquiv_fin_prod |
theorem | ProjectiveModules/Free/FiniteFreeSummand.lean, line 132 | For a ring, stable finiteness is equivalent to every equivalence from the finite coordinate module of size n to itself times P forcing P to be subsingleton, for complements P in the ring's universe. No arbitrary-semiring converse is claimed. |
LinearMap.traceOfFiniteProjective_comp_comm |
theorem | ProjectiveModules/Module/Trace/Cyclicity.lean, line 46 | The traces of g.comp f and f.comp g agree for maps between two finite projective additive-commutative-monoid modules over a commutative semiring, with independent scalar and carrier universes. |
LinearMap.traceOfFiniteProjective_tensorProduct |
theorem | ProjectiveModules/Module/Trace/TensorProduct.lean, line 45 | Applying the contraction trace after the bilinear tensor-product map equals multiplying the two factor traces for finite projective additive-commutative-monoid modules over a commutative semiring, with independent scalar and factor universes. |
LinearMap.traceOfFiniteProjective_tensorProduct' |
theorem | ProjectiveModules/Module/Trace/TensorProduct.lean, line 73 | The contraction trace of TensorProduct.map f g is the product of the factor traces, for endomorphisms of finite projective additive-commutative-monoid modules over a commutative semiring. |
Quoted from the main results in formalization.yaml of FormalFrontier/projective-modules at commit 27f95a8b, Apache-2.0.
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.