Other results
Results named in the rest of Tau Ceti's TauCeti.Algebra modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.
TheoremAbel's inequality, comparison form#
If the partial sums of f are dominated by those of
g up to N, and w is nonnegative and antitone on the first N indices, then
∑_{i < N} w i * f i ≤ ∑_{i < N} w i * g i. Only the last weight is required
to be nonnegative explicitly; the other signs follow from the successive comparisons
when N > 0.
TauCeti.sum_range_mul_le_sum_range_mul.{u_1} {R : Type u_1} [Ring R] [Preorder R]
[IsOrderedAddMonoid R] [PosMulMono R] {f g w : ℕ → R} {N : ℕ}
(hfg : ∀ k ≤ N, ∑ i ∈ Finset.range k, f i ≤ ∑ i ∈ Finset.range k, g i)
(hw : ∀ (i : ℕ), i + 1 < N → w (i + 1) ≤ w i) (hw0 : 0 ≤ w (N - 1)) :
∑ i ∈ Finset.range N, w i * f i ≤ ∑ i ∈ Finset.range N, w i * g i
DefinitionThe basis theorem#
the elements T_w, w : W, form a basis of the type-A Hecke algebra
over every commutative ring and for every unit parameter.
TauCeti.TypeAHeckeAlgebra.basisTw.{u_1, u_2} {R : Type u_1} [CommRing R] (q : Rˣ) {n : ℕ}
{W : Type u_2} [Group W] (cs : CoxeterSystem (CoxeterMatrix.A (n - 1)) W) :
Module.Basis W R (TauCeti.TypeAHeckeAlgebra R q n)
Uses 1 · Used by 1
TheoremThe Conway–Sloane exponent identity#
Twice ∑_{j < max k} binom(Nⱼ + 1, 2), where
Nⱼ = #{i ∈ s | j < kᵢ}, plus ∑_{i, i' ∈ s} (k_{i'} - kᵢ) (truncated subtraction) is
(#s + 1) ∑_{i ∈ s} kᵢ. The first sum is the exponent of p in the local density of the
diagonal Jordan form diag(uᵢ pᵏⁱ) at an odd prime, the second is the exponent of √p in the
cross terms of its Conway–Sloane p-mass.
Finset.two_mul_sum_range_choose_add_sum_sum_tsub.{u_1} {ι : Type u_1} (s : Finset ι) (k : ι → ℕ) :
2 * ∑ j ∈ Finset.range (s.sup k), ({i ∈ s | j < k i}.card + 1).choose 2 +
∑ i ∈ s, ∑ i' ∈ s, (k i' - k i) =
(s.card + 1) * ∑ i ∈ s, k i
TheoremDedekind's modular law#
if the join H ⊔ N is the sum set H + N (for
example when H normalizes N) and N ≤ K, then (K ⊓ H) ⊔ N = K ⊓ (H ⊔ N).
AddSubgroup.inf_sup_assoc_of_le.{u_1} {G : Type u_1} [AddGroup G] {H K N : AddSubgroup G}
(hHN : ↑(H ⊔ N) = ↑H + ↑N) (h : N ≤ K) : K ⊓ H ⊔ N = K ⊓ (H ⊔ N)
Lean
Formalized in Tau Ceti as AddSubgroup.inf_sup_assoc_of_le.
Other forms
Dedekind's modular law. Formalized in Tau Ceti as Subgroup.inf_sup_assoc_of_le.
Subgroup.inf_sup_assoc_of_le.{u_1} {G : Type u_1} [Group G] {H K N : Subgroup G}
(hHN : ↑(H ⊔ N) = ↑H * ↑N) (h : N ≤ K) : K ⊓ H ⊔ N = K ⊓ (H ⊔ N)
Sources
TheoremHermite's identity in truncated ceiling-division form#
for 0 < n, the ceilings of
(r - i) / n over a complete block 0 ≤ i < n of shifts add up to r. The subtraction is
truncated, so the terms with r ≤ i vanish. Compare the floor form Int.sum_range_add_ediv.
Nat.sum_range_sub_ceilDiv (r : ℕ) {n : ℕ} (hn : 0 < n) : ∑ i ∈ Finset.range n, (r - i) ⌈/⌉ n = r
Used by 1
TheoremHilbert's finiteness theorem#
For a finite-dimensional comodule V over a linearly
reductive commutative bialgebra, the invariants of the symmetric algebra Sym V form a finitely
generated algebra.
TauCeti.ComoduleAlgebra.fg_coinvariants_symmetricAlgebra.{u, v, u_1} {k : Type u} [Field k]
{H : Type v} [CommSemiring H] [Bialgebra k H] (hH : TauCeti.Coalgebra.IsLinearlyReductive k H)
(V : Type u_1) [AddCommMonoid V] [_root_.Module k V] [TauCeti.Comodule k H V]
[Module.Finite k V] : (TauCeti.ComoduleAlgebra.coinvariants k H (SymmetricAlgebra k V)).FG
Lean
Formalized in Tau Ceti as TauCeti.ComoduleAlgebra.fg_coinvariants_symmetricAlgebra.
Sources
Used by 1
TheoremMultinomial theorem for square-zero elements#
If the x i commute pairwise and square to
zero on s, then (∑ i ∈ s, x i) ^ n is n ! times the sum, over the n-element subsets t of
s, of the products of the x i with i ∈ t.
Finset.sum_pow_of_commute_of_mul_self_eq_zero.{u_1, u_2} {R : Type u_1} [Semiring R] {ι : Type u_2}
(s : Finset ι) (x : ι → R) (hc : (↑s).Pairwise (Function.onFun Commute x))
(hx : ∀ i ∈ s, x i * x i = 0) (n : ℕ) :
(∑ i ∈ s, x i) ^ n = n.factorial • ∑ t, (↑t).noncommProd x ⋯
TheoremNakayama's lemma for R[G]^ι#
An R[G]-linear endomorphism of R[G]^ι that is onto
modulo the maximal ideal is bijective.
TauCeti.MonoidAlgebra.bijective_of_forall_exists_mapRingHom_residue_eq.{u_1, u_2, u_3}
{R : Type u_1} [CommRing R] [IsLocalRing R] {G : Type u_2} [Monoid G] [Finite G] {ι : Type u_3}
[Finite ι] (θ : (ι → MonoidAlgebra R G) →ₗ[MonoidAlgebra R G] ι → MonoidAlgebra R G)
(h :
∀ (y : ι → MonoidAlgebra R G),
∃ x,
∀ (i : ι),
(MonoidAlgebra.mapRingHom G (IsLocalRing.residue R)) (θ x i) =
(MonoidAlgebra.mapRingHom G (IsLocalRing.residue R)) (y i)) :
Function.Bijective ⇑θ
Lean
Formalized in Tau Ceti as TauCeti.MonoidAlgebra.bijective_of_forall_exists_mapRingHom_residue_eq.
Sources
TheoremNewton's formula for the determinant#
when 2 and 3 are invertible,
det A = (T(A)³ - 3 T(A) T(A ∘ A) + 2 T(A ∘ (A ∘ A))) / 6.
TauCeti.AlbertAlgebra.det_eq_invOf_two_mul_invOf_three_mul.{u_1} {R : Type u_1} [CommRing R]
[Invertible 2] [Invertible 3] (A : TauCeti.AlbertAlgebra R) :
A.det =
⅟2 * ⅟3 *
(TauCeti.AlbertAlgebra.trace A ^ 3 -
3 * TauCeti.AlbertAlgebra.trace A * TauCeti.AlbertAlgebra.trace (A * A) +
2 * TauCeti.AlbertAlgebra.trace (A * (A * A)))
Lean
Formalized in Tau Ceti as TauCeti.AlbertAlgebra.det_eq_invOf_two_mul_invOf_three_mul.
Other forms
Newton's formula for the determinant, without division. Formalized in Tau Ceti as TauCeti.AlbertAlgebra.six_mul_det.
TauCeti.AlbertAlgebra.six_mul_det.{u_1} {R : Type u_1} [CommRing R] [Invertible 2]
(A : TauCeti.AlbertAlgebra R) :
6 * A.det =
TauCeti.AlbertAlgebra.trace A ^ 3 -
3 * TauCeti.AlbertAlgebra.trace A * TauCeti.AlbertAlgebra.trace (A * A) +
2 * TauCeti.AlbertAlgebra.trace (A * (A * A))
Sources
TheoremOcneanu's theorem#
Every Markov trace with parameter z is the Ocneanu trace.
TauCeti.InfiniteTypeAHeckeAlgebra.IsMarkovTrace.eq_ocneanuTrace.{u_1} {R : Type u_1} [CommRing R]
{q : Rˣ} {z : R} {τ : TauCeti.InfiniteTypeAHeckeAlgebra R q →ₗ[R] R}
(hτ : TauCeti.InfiniteTypeAHeckeAlgebra.IsMarkovTrace z τ) :
τ = TauCeti.InfiniteTypeAHeckeAlgebra.ocneanuTrace R q z
Lean
Formalized in Tau Ceti as TauCeti.InfiniteTypeAHeckeAlgebra.IsMarkovTrace.eq_ocneanuTrace.
Other forms
Ocneanu's theorem. Formalized in Tau Ceti as TauCeti.InfiniteTypeAHeckeAlgebra.existsUnique_isMarkovTrace.
TauCeti.InfiniteTypeAHeckeAlgebra.existsUnique_isMarkovTrace.{u_1} {R : Type u_1} [CommRing R]
{q : Rˣ} (z : R) : ∃! τ, TauCeti.InfiniteTypeAHeckeAlgebra.IsMarkovTrace z τ
Sources
Uses 4
TheoremSiegel's identity#
For θ₁ ≠ θ₀ and x - θ₂ y ≠ 0 in a field,
(θ₁ - θ₂) / (θ₁ - θ₀) · (x - θ₀ y) / (x - θ₂ y) + (θ₂ - θ₀) / (θ₁ - θ₀) · (x - θ₁ y) / (x - θ₂ y)
equals 1. Applied to the linear factors of a binary form, it turns a Thue equation into unit
equations.
TauCeti.siegel_identity.{u_1} {F : Type u_1} [Field F] {θ₀ θ₁ θ₂ x y : F} (h : θ₁ ≠ θ₀)
(hxy : x - θ₂ * y ≠ 0) :
(θ₁ - θ₂) / (θ₁ - θ₀) * ((x - θ₀ * y) / (x - θ₂ * y)) +
(θ₂ - θ₀) / (θ₁ - θ₀) * ((x - θ₁ * y) / (x - θ₂ * y)) =
1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.