Main results 201 to 210
| Declaration | Kind | Where | Note |
|---|---|---|---|
LinearMap.traceOfFiniteProjective_pi |
theorem | ProjectiveModules/Module/Trace/Pi.lean, line 52 | The contraction trace of an arbitrary endomorphism of a finite dependent product is the finsum of the traces of its diagonal projection-endomorphism-single composites. The factors are finite projective additive-commutative-monoid modules over a commutative semiring. Only root index finiteness is assumed; scalar, index and carrier universes are independent, without an enumeration, basis, additive inverses or an additional output-projectivity premise. |
OrthogonalIdempotents.conjugationCoeff |
def | ProjectiveModules/RingTheory/IdempotentConjugation.lean, line 50 | Over any ring and finite index type, the coefficient is (sum i, b i * a i) + (1 - sum i, b i) * (1 - sum i, a i). No orthogonality or ideal hypothesis is needed for its definition. It intertwines corresponding members of two orthogonal families; it reduces to the diagonal sum when a sums to one, to the two-idempotent expression for a singleton, and to one for an empty index. |
OrthogonalIdempotents.conjugatingUnit |
def | ProjectiveModules/RingTheory/IdempotentConjugation.lean, line 134 | For an orthogonal family a, a two-sided ideal I contained in the Jacobson radical, and b i - a i in I for every i, construct a unit whose value is conjugationCoeff a b. The value is congruent to one modulo I. Orthogonality of b is not needed for this construction. |
OrthogonalIdempotents.conjugatingUnit_mul_inv |
theorem | ProjectiveModules/RingTheory/IdempotentConjugation.lean, line 154 | If b is also orthogonal, this one unit simultaneously conjugates every a i to b i. Neither family must sum to one. Noncommutative and zero rings and empty indices are allowed; the empty-family unit is one. Scalar and index universes are independent. |
OrthogonalIdempotents.exists_conjugatingUnit_of_ker_le_jacobson |
theorem | ProjectiveModules/RingTheory/IdempotentConjugation.lean, line 206 | Given any ring homomorphism whose kernel lies in the source Jacobson radical, two equal-image finite orthogonal families are conjugate by a unit with the specified coefficient as its value, mapping to one and congruent to one modulo the kernel. No surjectivity is required; source, target and index universes are independent. |
OrthogonalIdempotents.exists_conjugatingUnit_of_isNilpotent_ker |
theorem | ProjectiveModules/RingTheory/IdempotentConjugation.lean, line 226 | The same equal-image conjugacy conclusion holds when every element of the whole kernel is nilpotent. No common nilpotence exponent, surjectivity, completeness of the families, commutativity or nontriviality assumption is imposed. |
RingHom.map_conjugationCoeff |
theorem | ProjectiveModules/RingTheory/IdempotentConjugationNaturality.lean, line 40 | Any unital f : R →+* S sends conjugationCoeff a b to conjugationCoeff (f ∘ a) (f ∘ b), for arbitrary finite families a b : ι → R. No orthogonality, ideals or congruences are required. This is a simp law over possibly noncommutative or zero rings, with empty indices allowed and independent scalar and index universes. |
OrthogonalIdempotents.map_conjugatingUnit |
theorem | ProjectiveModules/RingTheory/IdempotentConjugationNaturality.lean, line 58 | For an orthogonal finite family a and any unital f : R →+* S, Units.map f.toMonoidHom of the source constructed unit equals the target constructed unit in Sˣ. The source uses a two-sided ideal I ≤ Ring.jacobson R and b i - a i ∈ I for every i; the target uses its own two-sided ideal J ≤ Ring.jacobson S and f (b i) - f (a i) ∈ J for every i. Orthogonality of the image of a is derived by OrthogonalIdempotents.map, not an extra hypothesis. No ideal-image containment, radical preservation, injectivity or surjectivity is assumed. The target data name the target construction; they are not needed merely to map a source unit. The family b need not be idempotent or orthogonal, so this is construction transport, not simultaneous conjugacy in that generality. Neither family must sum to one; noncommutative and zero rings, empty indices and independent scalar and index universes are allowed. This is not a simp law, since the target ideal data occur only on the right. |
OrthogonalIdempotents.conjugationCoeff_comp_equiv |
theorem | ProjectiveModules/RingTheory/IdempotentConjugationNaturality.lean, line 77 | For arbitrary finite families a b : ι → R and any e : κ ≃ ι, conjugationCoeff (a ∘ e) (b ∘ e) = conjugationCoeff a b. Both families are reindexed together. This simp law requires no orthogonality, ideal or congruence data, over possibly noncommutative or zero rings, with empty indices and independent ring and both index universes allowed. |
OrthogonalIdempotents.conjugatingUnit_comp_equiv |
theorem | ProjectiveModules/RingTheory/IdempotentConjugationNaturality.lean, line 93 | For an orthogonal finite family a, a two-sided ideal I ≤ Ring.jacobson R, b i - a i ∈ I for every i, and any e : κ ≃ ι, jointly reindexing a and b leaves the constructed unit unchanged in Rˣ. The reindexed construction uses the same ideal and the congruence at e k; orthogonality is transported by OrthogonalIdempotents.equiv. No idempotence or orthogonality of b, sum-to-one, commutativity or nontriviality hypothesis is required. Empty finite indices and independent ring and both index universes are included. This is a construction identity, not simultaneous conjugacy for arbitrary b. |
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.