Other results
Results named in the rest of Tau Ceti's TauCeti.LinearAlgebra modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.
TheoremThe Cauchy–Binet formula#
The determinant of the p × p matrix of pairwise products
∑ₖ x i k * y j k is the sum over the p-element subsets s of ι of the products of the
Plücker coordinates of x and y at s. For p > #ι both sides vanish.
TauCeti.det_mul_transpose_eq_sum_plucker_mul.{u_1, u_3} {R : Type u_1} {ι : Type u_3} [CommRing R]
[LinearOrder ι] {p : ℕ} [Fintype ι] (x y : Fin p → ι → R) :
(Matrix.of x * (Matrix.of y).transpose).det = ∑ s, TauCeti.plucker x s * TauCeti.plucker y s
Lean
Formalized in Tau Ceti as TauCeti.det_mul_transpose_eq_sum_plucker_mul.
Other forms
The Cauchy–Binet formula for a Gram determinant. Formalized in Tau Ceti as Matrix.det_mul_transpose_eq_sum_plucker_sq.
Matrix.det_mul_transpose_eq_sum_plucker_sq.{u_1, u_3} {R : Type u_1} {ι : Type u_3} [CommRing R]
[LinearOrder ι] {p : ℕ} [Fintype ι] (A : Matrix (Fin p) ι R) :
(A * A.transpose).det = ∑ s, TauCeti.plucker A.row s ^ 2
The Cauchy–Binet formula, Hermitian form. Formalized in Tau Ceti as TauCeti.det_mul_conjTranspose_eq_sum_plucker_mul_star.
TauCeti.det_mul_conjTranspose_eq_sum_plucker_mul_star.{u_1, u_3} {R : Type u_1} {ι : Type u_3}
[CommRing R] [LinearOrder ι] {p : ℕ} [StarRing R] [Fintype ι] (x : Fin p → ι → R) :
(Matrix.of x * (Matrix.of x).conjTranspose).det =
∑ s, TauCeti.plucker x s * star (TauCeti.plucker x s)
Sources
TheoremCayley–Hamilton on a finite projective module#
For some n bounding the degree of the
reversed characteristic polynomial Q of f, the reflection X ^ n · Q(1/X) of Q kills f;
it is monic (monic_reflect_projectiveCharpolyRev).
LinearMap.exists_aeval_reflect_projectiveCharpolyRev_eq_zero.{u_1, u_2} {R : Type u_1}
{M : Type u_2} [CommRing R] [AddCommGroup M] [_root_.Module R M] [Module.Finite R M]
[Module.Projective R M] (f : Module.End R M) :
∃ n,
(LinearMap.projectiveCharpolyRev f).natDegree ≤ n ∧
(Polynomial.aeval f) (Polynomial.reflect n (LinearMap.projectiveCharpolyRev f)) = 0
Lean
Formalized in Tau Ceti as LinearMap.exists_aeval_reflect_projectiveCharpolyRev_eq_zero.
Sources
TheoremThe Choie–Zagier criterion (Popa–Zagier, Lemma 1)#
for σ ^ 2 = 1 and υ ^ 3 = 1 with
2 and 3 invertible and ker (1 + σ), ker (1 + υ + υ²) disjoint, a vector x lies in
range (1 + σ) ⊔ range (1 + υ + υ²) exactly when (1 - σ) x ∈ range (1 - υ σ).
TauCeti.End.one_sub_apply_mem_range_one_sub_mul_iff.{u_1, u_2} {R : Type u_1} {M : Type u_2}
[Semiring R] [AddCommGroup M] [_root_.Module R M] {σ υ : Module.End R M} [Invertible 2]
[Invertible 3] (hσ : σ ^ 2 = 1) (hυ : υ ^ 3 = 1)
(hacyc : Disjoint (1 + σ).ker (1 + υ + υ ^ 2).ker) {x : M} :
(1 - σ) x ∈ (1 - υ * σ).range ↔ x ∈ (1 + σ).range ⊔ (1 + υ + υ ^ 2).range
Lean
Formalized in Tau Ceti as TauCeti.End.one_sub_apply_mem_range_one_sub_mul_iff.
Other forms
The Choie–Zagier criterion, forward direction (Popa–Zagier, Lemma 1, ⇒). Formalized in Tau Ceti as TauCeti.End.one_sub_apply_mem_range_one_sub_mul_of_mem_sup.
TauCeti.End.one_sub_apply_mem_range_one_sub_mul_of_mem_sup.{u_1, u_2} {R : Type u_1} {M : Type u_2}
[Semiring R] [AddCommGroup M] [_root_.Module R M] {σ υ : Module.End R M} (hσ : σ ^ 2 = 1)
(hυ : υ ^ 3 = 1) {x : M} (hx : x ∈ (1 + σ).range ⊔ (1 + υ + υ ^ 2).range) :
(1 - σ) x ∈ (1 - υ * σ).range
Sources
Used by 1
TheoremDedekind's bound#
A finite monoid G has at most #G homomorphisms into a domain M,
since they are linearly independent in the M-module G → M of rank #G.
TauCeti.natCard_monoidHom_le.{u_1, u_2} (G : Type u_1) (M : Type u_2) [MulOneClass G] [Finite G]
[CommRing M] [IsDomain M] : Nat.card (G →* M) ≤ Nat.card G
TheoremEichler's theorem#
For a reflexive positive definite integral form, a set of submodules
consists of pairwise orthogonal orthogonally indecomposable submodules spanning M exactly when
it is the set of orthogonal components. In particular such a decomposition exists and is unique.
LinearMap.BilinForm.eq_orthComponents_iff.{u_3} {M : Type u_3} [AddCommGroup M]
{B : LinearMap.BilinForm ℤ M} (hB : B.IsRefl)
(hpos : (LinearMap.BilinMap.toQuadraticMap B).PosDef) {S : Set (Submodule ℤ M)} :
S = B.orthComponents ↔
(∀ N ∈ S, B.IsOrthIndecomposable N) ∧ (S.Pairwise fun N N' => N ≤ B.orthogonal N') ∧ sSup S = ⊤
TheoremEuler's identity, twisted by an endomorphism#
If an algebra map φ turns f into
multiplication by c on generators, φ (ι (f x)) = c * φ (ι x), then on a homogeneous element of
degree n it turns the derivation induced by f into multiplication by n * c. For f = 1 and
φ the identity this is Euler's identity D p = n • p for the Euler derivation D.
AlgHom.apply_derivationOfEnd_eq_mul_of_mem_homogeneousSubmodule.{u, v, u_1} {R : Type u}
{M : Type v} [CommRing R] [AddCommGroup M] [_root_.Module R M] {A : Type u_1} [CommSemiring A]
[Algebra R A] (φ : SymmetricAlgebra R M →ₐ[R] A) {f : Module.End R M} {c : A}
(h : ∀ (x : M), φ ((SymmetricAlgebra.ι R M) (f x)) = c * φ ((SymmetricAlgebra.ι R M) x)) {n : ℕ}
{p : SymmetricAlgebra R M} (hp : p ∈ TauCeti.SymmetricAlgebra.homogeneousSubmodule R M n) :
φ (((SymmetricAlgebra.derivationOfEnd R M) f) p) = ↑n * c * φ p
Lean
Formalized in Tau Ceti as AlgHom.apply_derivationOfEnd_eq_mul_of_mem_homogeneousSubmodule.
Sources
TheoremExactness in Popa–Zagier's §3 Theorem 2#
for σ ^ 2 = σ' ^ 2 = 1 and υ ^ 3 = υ' ^ 3 = 1,
with σ and υ commuting with σ' and υ', 2 and 3 invertible and ker (1 + σ'),
ker (1 + υ' + υ'²) disjoint: if ξ ∈ range (1 - σ') ⊔ range (1 - υ'),
(1 + σ') ξ ∈ range (1 + υ + υ²) and (1 + υ' + υ'²) ξ ∈ range (1 + σ), then
ξ ∈ range ((1 + σ) (1 - σ')) ⊔ range ((1 + υ + υ²) (1 - υ')).
For the left multiplications σ, υ and the right multiplications σ', υ' by S, U on ℛ, the
hypotheses on ξ say that ξ ∈ ℛ (1 - S) + ℛ (1 - U), the elements whose right coset sums vanish,
and that ξ lies in their ℬ = {ξ | ξ π_S ∈ π_U ℛ, ξ π_U ∈ π_S ℛ} (6); the conclusion is
ξ ∈ 𝒥 = π_S ℛ (1 - π_S) + π_U ℛ (1 - π_U) (7).
TauCeti.End.mem_sup_range_one_add_mul_one_sub.{u_1, u_2} {R : Type u_1} {M : Type u_2} [Semiring R]
[AddCommGroup M] [_root_.Module R M] {σ υ : Module.End R M} [Invertible 2] [Invertible 3]
{σ' υ' : Module.End R M} (hσ : σ ^ 2 = 1) (hυ : υ ^ 3 = 1) (hσ' : σ' ^ 2 = 1) (hυ' : υ' ^ 3 = 1)
(hσσ' : Commute σ σ') (hσυ' : Commute σ υ') (hυσ' : Commute υ σ') (hυυ' : Commute υ υ')
(hacyc : Disjoint (1 + σ').ker (1 + υ' + υ' ^ 2).ker) {ξ : M}
(hξ : ξ ∈ (1 - σ').range ⊔ (1 - υ').range) (hσ'ξ : (1 + σ') ξ ∈ (1 + υ + υ ^ 2).range)
(hυ'ξ : (1 + υ' + υ' ^ 2) ξ ∈ (1 + σ).range) :
ξ ∈ ((1 + σ) * (1 - σ')).range ⊔ ((1 + υ + υ ^ 2) * (1 - υ')).range
TheoremThe graded Jacobi identity for the Gerstenhaber bracket, in Leibniz form#
bracketing with
F of degree p is a graded derivation of the bracket of g of degree q and h of
degree r,
[F, [g, h]] = [[F, g], h] + (-1)^(p * q) • [g, [F, h]].
TauCeti.ReducedTensorWords.leibniz_gerstenhaberBracket.{uR, uM} {R : Type uR} {M : Type uM}
[CommRing R] [AddCommGroup M] [_root_.Module R M] {G : TauCeti.InternalGrading R M ℤ}
{F g h : TauCeti.ReducedTensorWords R M →ₗ[R] M} {p q r : ℤ}
(hF : TauCeti.LinearMap.IsHomogeneous F (TauCeti.ReducedTensorWords.gradedPiece G) (G.piece ℤ) p)
(hg : TauCeti.LinearMap.IsHomogeneous g (TauCeti.ReducedTensorWords.gradedPiece G) (G.piece ℤ) q)
(hh :
TauCeti.LinearMap.IsHomogeneous h (TauCeti.ReducedTensorWords.gradedPiece G) (G.piece ℤ) r) :
TauCeti.ReducedTensorWords.gerstenhaberBracket G p (q + r) F
(TauCeti.ReducedTensorWords.gerstenhaberBracket G q r g h) =
TauCeti.ReducedTensorWords.gerstenhaberBracket G (p + q) r
(TauCeti.ReducedTensorWords.gerstenhaberBracket G p q F g) h +
TauCeti.negOnePowCast R (p * q) •
TauCeti.ReducedTensorWords.gerstenhaberBracket G q (p + r) g
(TauCeti.ReducedTensorWords.gerstenhaberBracket G p r F h)
Lean
Formalized in Tau Ceti as TauCeti.ReducedTensorWords.leibniz_gerstenhaberBracket.
Sources
TheoremHermite's inequality#
A symmetric positive definite integral bilinear form B on a free
ℤ-module of rank n ≥ 1 takes on some nonzero vector x a value with
3 ^ (n choose 2) · B(x, x) ^ n ≤ 4 ^ (n choose 2) · det B, where det B is the Gram determinant
of B in any basis. Equivalently B(x, x) ≤ (4 / 3) ^ ((n - 1) / 2) · (det B) ^ (1 / n).
LinearMap.BilinForm.exists_ne_zero_three_pow_mul_pow_le_four_pow_mul_det.{u_1, u_2} {M : Type u_1}
[AddCommGroup M] [Nontrivial M] {ι : Type u_2} [Fintype ι] [DecidableEq ι]
(B : LinearMap.BilinForm ℤ M) (hB : B.IsSymm)
(hpos : (LinearMap.BilinMap.toQuadraticMap B).PosDef) (b : Module.Basis ι ℤ M) :
∃ x,
x ≠ 0 ∧
3 ^ (Fintype.card ι).choose 2 * (B x) x ^ Fintype.card ι ≤
4 ^ (Fintype.card ι).choose 2 * ((LinearMap.BilinForm.toMatrix b) B).det
Lean
Formalized in Tau Ceti as LinearMap.BilinForm.exists_ne_zero_three_pow_mul_pow_le_four_pow_mul_det.
Sources
TheoremIwasawa's theorem for PSL#
On at least two coordinates, the projective special linear group is simple as soon as the special linear group is perfect.
Matrix.ProjectiveSpecialLinearGroup.isSimpleGroup_of_commutator_eq_top.{u_1, u_2} {ι : Type u_1}
{F : Type u_2} [Fintype ι] [DecidableEq ι] [Field F] [Nontrivial ι]
(h : commutator (Matrix.SpecialLinearGroup ι F) = ⊤) :
IsSimpleGroup (Matrix.ProjectiveSpecialLinearGroup ι F)
Lean
Formalized in Tau Ceti as Matrix.ProjectiveSpecialLinearGroup.isSimpleGroup_of_commutator_eq_top.
Sources
TheoremJacobi's formula for a determinant, in row form#
Rescale one row of a matrix entry by entry along a fixed vector of factors, and sum the resulting determinants over the rows: the answer is the determinant multiplied by the total of the factors.
Matrix.sum_det_updateRow_mul_row.{u_1, u_2} {ι : Type u_1} [DecidableEq ι] [Fintype ι]
{R : Type u_2} [CommRing R] (A : Matrix ι ι R) (d : ι → R) :
∑ k, (A.updateRow k fun j => d j * A k j).det = (∑ j, d j) * A.det
Used by 1
TheoremThe Jacobian criterion#
Over a domain R of characteristic zero, if every generator
ι (b j) is algebraic over the subalgebra generated by the family f, then the Jacobian of f
is nonzero. This applies to a system of basic invariants of a finite group, over which the
polynomial algebra is integral.
SymmetricAlgebra.jacobian_ne_zero.{u_1, u_2, u_3} {R : Type u_1} {M : Type u_2} [CommRing R]
[AddCommGroup M] [_root_.Module R M] {n : Type u_3} [Fintype n] [DecidableEq n]
(b : Module.Basis n R M) [IsDomain R] [CharZero R] {f : n → SymmetricAlgebra R M}
(hf :
∀ (j : n), IsAlgebraic (↥(Algebra.adjoin R (Set.range f))) ((SymmetricAlgebra.ι R M) (b j))) :
SymmetricAlgebra.jacobian b f ≠ 0
TheoremJacobson's lemma on commutators#
In characteristic zero, if A commutes with ⁅A, B⁆,
then ⁅A, B⁆ is nilpotent: each of its positive powers is a commutator with A, hence
traceless.
LinearMap.isNilpotent_lie_of_lie_lie_eq_zero.{u_1, u_2} {K : Type u_1} {M : Type u_2} [Field K]
[AddCommGroup M] [_root_.Module K M] [FiniteDimensional K M] [CharZero K] {A B : Module.End K M}
(h : ⁅A, ⁅A, B⁆⁆ = 0) : IsNilpotent ⁅A, B⁆
Used by 2
TheoremKolchin's common fixed vector theorem#
If every element of a monoid acts unipotently on a nonzero finite-dimensional vector space over a field, then the monoid fixes a nonzero vector.
Representation.exists_common_fixed_vector_of_isUnipotent.{u, v, w} {K : Type u} {G : Type w}
{V : Type v} [Field K] [Monoid G] [AddCommGroup V] [_root_.Module K V] [FiniteDimensional K V]
[Nontrivial V] (ρ : Representation K G V) (hunipotent : ∀ (g : G), IsNilpotent (ρ g - 1)) :
∃ v, v ≠ 0 ∧ ∀ (g : G), (ρ g) v = v
Lean
Formalized in Tau Ceti as Representation.exists_common_fixed_vector_of_isUnipotent.
Sources
TheoremLaplace's identity (Bombieri–Gubler (7.16))#
the wedge of p forms takes the value
det (l a (y b)) on the Plücker vector of p vectors y.
TauCeti.wedgeForm_plucker.{u_1, u_2} {R : Type u_1} [CommRing R] {ι : Type u_2} [LinearOrder ι]
{p : ℕ} [Fintype ι] (l : Fin p → Module.Dual R (ι → R)) (y : Fin p → ι → R) :
(TauCeti.wedgeForm l) (TauCeti.plucker y) = (Matrix.of fun a b => (l a) (y b)).det
Uses 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.