theorem
norm_eq_det_leftMulMatrix
{A : Type u_1}
{B : Type u_2}
[CommRing A]
[CommRing B]
[Algebra A B]
{ι : Type u_3}
[Fintype ι]
[DecidableEq ι]
(basis : Module.Basis ι A B)
(b : B)
:
theorem
trace_eq_trace_leftMulMatrix
{A : Type u_1}
{B : Type u_2}
[CommRing A]
[CommRing B]
[Algebra A B]
{ι : Type u_3}
[Fintype ι]
[DecidableEq ι]
(basis : Module.Basis ι A B)
(b : B)
:
theorem
leftMulMatrix_baseChange
{A : Type u_1}
{A' : Type u_2}
[CommRing A]
[CommRing A']
[Algebra A A']
{B : Type u_3}
[CommRing B]
[Algebra A B]
{ι : Type u_4}
[Fintype ι]
[DecidableEq ι]
(bB : Module.Basis ι A B)
(b : B)
:
(Algebra.leftMulMatrix (Module.Basis.baseChange A' bB)) (Algebra.TensorProduct.includeRight b) = (algebraMap A A').mapMatrix ((Algebra.leftMulMatrix bB) b)
theorem
norm_baseChange
{A : Type u_1}
{A' : Type u_2}
[CommRing A]
[CommRing A']
[Algebra A A']
{B : Type u_3}
[CommRing B]
[Algebra A B]
{ι : Type u_4}
[Fintype ι]
[DecidableEq ι]
(bB : Module.Basis ι A B)
(b : B)
:
theorem
trace_baseChange
{A : Type u_1}
{A' : Type u_2}
[CommRing A]
[CommRing A']
[Algebra A A']
{B : Type u_3}
[CommRing B]
[Algebra A B]
{ι : Type u_4}
[Fintype ι]
[DecidableEq ι]
(bB : Module.Basis ι A B)
(b : B)
:
(algebraMap A A') ((Algebra.trace A B) b) = (Algebra.trace A' (TensorProduct A A' B)) (Algebra.TensorProduct.includeRight b)
theorem
free_norm_trace_baseChange
{A : Type u_1}
{A' : Type u_2}
[CommRing A]
[CommRing A']
[Algebra A A']
{B : Type u_3}
[CommRing B]
[Algebra A B]
{ι : Type u_4}
[Fintype ι]
[DecidableEq ι]
(bB : Module.Basis ι A B)
:
Nonempty (Module.Basis ι A' (TensorProduct A A' B)) ∧ (∀ (b : B), (algebraMap A A') ((Algebra.norm A) b) = (Algebra.norm A') (Algebra.TensorProduct.includeRight b)) ∧ ∀ (b : B),
(algebraMap A A') ((Algebra.trace A B) b) = (Algebra.trace A' (TensorProduct A A' B)) (Algebra.TensorProduct.includeRight b)
theorem
norm_eq_prod_embeddings'
{K : Type u_1}
{L : Type u_2}
[Field K]
[Field L]
[Algebra K L]
(E : Type u_3)
[Field E]
[Algebra K E]
[FiniteDimensional K L]
[Algebra.IsSeparable K L]
[IsAlgClosed E]
(x : L)
:
theorem
trace_eq_sum_embeddings'
{K : Type u_1}
{L : Type u_2}
[Field K]
[Field L]
[Algebra K L]
(E : Type u_3)
[Field E]
[Algebra K E]
[FiniteDimensional K L]
[Algebra.IsSeparable K L]
[IsAlgClosed E]
(x : L)
:
theorem
norm_eq_prod_roots_pow
{K : Type u_1}
{L : Type u_2}
[Field K]
[Field L]
[Algebra K L]
(F : Type u_3)
[Field F]
[Algebra K F]
{x : L}
(hF : (Polynomial.map (algebraMap K F) (minpoly K x)).Splits)
:
theorem
trace_eq_smul_sum_roots
{K : Type u_1}
{L : Type u_2}
[Field K]
[Field L]
[Algebra K L]
{F : Type u_3}
[Field F]
[Algebra K F]
[FiniteDimensional K L]
{x : L}
(hF : (Polynomial.map (algebraMap K F) (minpoly K x)).Splits)
:
theorem
norm_eq_neg_one_pow_mul_coeff_zero
{K : Type u_1}
{L : Type u_2}
[Field K]
[Field L]
[Algebra K L]
[FiniteDimensional K L]
(x : L)
:
(Algebra.norm K) x = (-1) ^ ((minpoly K x).natDegree * Module.finrank (↥K⟮x⟯) L) * (minpoly K x).coeff 0 ^ Module.finrank (↥K⟮x⟯) L
theorem
trace_eq_neg_finrank_mul_nextCoeff
{K : Type u_1}
{L : Type u_2}
[Field K]
[Field L]
[Algebra K L]
[FiniteDimensional K L]
(x : L)
:
theorem
norm_mem_of_isIntegral
{A : Type u_1}
[CommRing A]
[IsIntegrallyClosed A]
{K : Type u_2}
[Field K]
[Algebra A K]
[IsFractionRing A K]
{L : Type u_3}
[Field L]
[Algebra K L]
[Algebra A L]
[IsScalarTower A K L]
{x : L}
(hx : IsIntegral A x)
:
∃ (a : A), (algebraMap A K) a = (Algebra.norm K) x
theorem
trace_mem_of_isIntegral
{A : Type u_1}
[CommRing A]
[IsIntegrallyClosed A]
{K : Type u_2}
[Field K]
[Algebra A K]
[IsFractionRing A K]
{L : Type u_3}
[Field L]
[Algebra K L]
[FiniteDimensional K L]
[Algebra A L]
[IsScalarTower A K L]
{x : L}
(hx : IsIntegral A x)
:
∃ (a : A), (algebraMap A K) a = (Algebra.trace K L) x
theorem
norm_tower
{A : Type u_1}
{B : Type u_2}
{C : Type u_3}
[CommRing A]
[CommRing B]
[Ring C]
[Algebra A B]
[Algebra A C]
[Algebra B C]
[IsScalarTower A B C]
[Module.Free A B]
[Module.Free B C]
(x : C)
:
theorem
trace_tower
{A : Type u_1}
{B : Type u_2}
{C : Type u_3}
[CommRing A]
[CommRing B]
[CommRing C]
[Algebra A B]
[Algebra A C]
[Algebra B C]
[IsScalarTower A B C]
[Module.Free A B]
[Module.Finite A B]
[Module.Free B C]
[Module.Finite B C]
(x : C)
: