sum_embeddings_eq_finrank_mul — Mathlib

English

Another formalization of trace invariance under algebraic and ring equivalences with compatibility conditions.

Русский

Еще одна формализация сохранения следа при алгебрических и кольцевых эквивалентах с условием совместимости.

LaTeX

$$Same structural statement as 185525/185526$$

Lean4

theorem sum_embeddings_eq_finrank_mul [FiniteDimensional K F] [Algebra.IsSeparable K F] (pb : PowerBasis K L) :
    ∑ σ : F →ₐ[K] E, σ (algebraMap L F pb.gen) =
      finrank L F • (@Finset.univ _ (PowerBasis.AlgHom.fintype pb)).sum fun σ : L →ₐ[K] E => σ pb.gen :=
  by
  haveI : FiniteDimensional L F := FiniteDimensional.right K L F
  haveI : Algebra.IsSeparable L F := Algebra.isSeparable_tower_top_of_isSeparable K L F
  letI : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
  rw [Fintype.sum_equiv algHomEquivSigma (fun σ : F →ₐ[K] E => _) fun σ => σ.1 pb.gen, ← Finset.univ_sigma_univ,
    Finset.sum_sigma, ← Finset.sum_nsmul]
  · refine Finset.sum_congr rfl fun σ _ => ?_
    letI : Algebra L E := σ.toRingHom.toAlgebra
    simp_rw [Finset.sum_const, Finset.card_univ, ← AlgHom.card L F E]
  · intro σ
    simp only [algHomEquivSigma, Equiv.coe_fn_mk, AlgHom.restrictDomain, AlgHom.comp_apply, IsScalarTower.coe_toAlgHom']

Похожие утверждения