noncomputable def φ_m {K : Type u_1} {F : Type u_2} {E : Type u_3} [Field K] [Field F] [Field E] [Algebra K F] [Algebra K E] (n : ℕ) (φ : F →ₐ[K] E) : Matrix (Fin n) (Fin n) F →ₐ[K] Matrix (Fin n) (Fin n) E

Equations

• φ_m n φ = { toFun := fun (M : Matrix (Fin n) (Fin n) F) (i j : Fin n) => φ (M i j), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem φ_m_apply {K : Type u_1} {F : Type u_2} {E : Type u_3} [Field K] [Field F] [Field E] [Algebra K F] [Algebra K E] (n : ℕ) (φ : F →ₐ[K] E) (M : Matrix (Fin n) (Fin n) F) (i j : Fin n) : (φ_m n φ) M i j = φ (M i j)

theorem φ_m_inj {K : Type u_1} {F : Type u_2} {E : Type u_3} [Field K] [Field F] [Field E] [Algebra K F] [Algebra K E] (n : ℕ) (φ : F →ₐ[K] E) : Function.Injective ⇑(φ_m n φ)

@[reducible, inline]

noncomputable abbrev e1Aux {K : Type u_1} {F : Type u_2} {E : Type u_3} [Field K] [Field F] [Field E] [Algebra K F] [Algebra K E] (n : ℕ) (φ : F →ₐ[K] E) : Matrix (Fin n) (Fin n) ↥φ.range ≃ₐ[K] ↥(φ_m n φ).range

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev e1 (K : Type u_1) (F : Type u_2) (E : Type u_3) [Field K] [Field F] [Field E] [Algebra K F] [Algebra K E] (n : ℕ) (φ : F →ₐ[K] E) : Matrix (Fin n) (Fin n) F ≃ₐ[K] ↥(φ_m n φ).range

Equations

• e1 K F E n φ = AlgEquiv.ofBijective (φ_m n φ).rangeRestrict ⋯

@[reducible, inline]

noncomputable abbrev e1' (K : Type u_1) (F : Type u_2) (E : Type u_3) (A : Type u_6) [Field K] [Field F] [Field E] [Algebra K F] [Algebra K E] [Ring A] [Algebra K A] (n : ℕ) (e : TensorProduct K F A ≃ₐ[F] Matrix (Fin n) (Fin n) F) (φ : F →ₐ[K] E) : TensorProduct K (↥φ.range) A ≃ₐ[K] Matrix (Fin n) (Fin n) ↥φ.range

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev e1'' {K : Type u_1} {F : Type u_2} {E : Type u_3} (A : Type u_6) [Field K] [Field F] [Field E] [Algebra K F] [Algebra K E] [Ring A] [Algebra K A] (n : ℕ) (e : TensorProduct K F A ≃ₐ[F] Matrix (Fin n) (Fin n) F) (φ : F →ₐ[K] E) : TensorProduct K (↥φ.range) A ≃ₐ[↥φ.range] Matrix (Fin n) (Fin n) ↥φ.range

Equations

• e1'' A n e φ = { toEquiv := (e1' K F E A n e φ).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[reducible, inline]

noncomputable abbrev g {K : Type u_1} {F : Type u_2} {E : Type u_3} {A : Type u_6} [Field K] [Field F] [Field E] [Algebra K F] [Algebra K E] [Ring A] [Algebra K A] {n : ℕ} (e : TensorProduct K F A ≃ₐ[F] Matrix (Fin n) (Fin n) F) (φ : F →ₐ[K] E) : TensorProduct K E A ≃ₐ[E] Matrix (Fin n) (Fin n) E

Equations

• One or more equations did not get rendered due to their size.

theorem mat_over_extension {K : Type u_1} {F : Type u_2} {E : Type u_3} (A : Type u_6) [Field K] [Field F] [Field E] [Algebra K F] [Algebra K E] [Ring A] [Algebra K A] (n : ℕ) (e : TensorProduct K F A ≃ₐ[F] Matrix (Fin n) (Fin n) F) (φ : F →ₐ[K] E) (a : A) : ∃ (g : TensorProduct K E A ≃ₐ[E] Matrix (Fin n) (Fin n) E), g (1 ⊗ₜ[K] a) = φ.mapMatrix (e (1 ⊗ₜ[K] a))

noncomputable def ReducedCharPoly {K : Type u_1} {F : Type u_2} {A : Type u_6} [Field K] [Field F] [Algebra K F] [Ring A] [Algebra K A] {n : ℕ} (e : TensorProduct K F A ≃ₐ[F] Matrix (Fin n) (Fin n) F) (a : A) : Polynomial F

Equations

• ReducedCharPoly e a = (e (1 ⊗ₜ[K] a)).charpoly

theorem ReducedCharPoly.over_extension (K : Type u_1) (F : Type u_2) (E : Type u_3) (A : Type u_6) [Field K] [Field F] [Field E] [Algebra K F] [Algebra K E] [Ring A] [Algebra K A] (n : ℕ) (e : TensorProduct K F A ≃ₐ[F] Matrix (Fin n) (Fin n) F) (φ : F →ₐ[K] E) (a : A) : ∃ (g : TensorProduct K E A ≃ₐ[E] Matrix (Fin n) (Fin n) E), ReducedCharPoly g a = (Polynomial.mapAlgHom φ) (ReducedCharPoly e a)

theorem eq_pow_reducedCharpoly (K F F_bar A : Type u) [Field K] [Field F] [Field F_bar] [Algebra K F] [Algebra F F_bar] [hF_bar : IsAlgClosure F F_bar] [Ring A] [Algebra K A] [Algebra.IsCentral K A] [IsSimpleRing A] (n m : ℕ) (e : TensorProduct K F A ≃ₐ[F] Matrix (Fin n) (Fin n) F) (g : TensorProduct K F A →ₐ[F] Matrix (Fin m) (Fin m) F) [NeZero m] (a : A) : ∃ (r : ℕ), NeZero r ∧ m = r * n ∧ (g (1 ⊗ₜ[K] a)).charpoly = ReducedCharPoly e a ^ r

theorem eq_polys (K F F_bar A : Type u) [Field K] [Field F] [Field F_bar] [Algebra K F] [Algebra F F_bar] [hF_bar : IsAlgClosure F F_bar] [Ring A] [Algebra K A] [Algebra.IsCentral K A] [IsSimpleRing A] (n : ℕ) [NeZero n] (f1 f2 : TensorProduct K F A ≃ₐ[F] Matrix (Fin n) (Fin n) F) (a : A) : ReducedCharPoly f1 a = ReducedCharPoly f2 a

theorem fixedpoints (K F : Type u) [Field K] [Field F] [Algebra K F] [IsGalois K F] [FiniteDimensional K F] (x : F) : (∀ (φ : Gal(F/K)), φ x = x) → x ∈ (Algebra.ofId K F).range

theorem mem_Kx (K F F_bar A : Type u) [Field K] [Field F] [Field F_bar] [Algebra K F] [Algebra F F_bar] [hF_bar : IsAlgClosure F F_bar] [Ring A] [Algebra K A] [Algebra.IsCentral K A] [IsSimpleRing A] (n : ℕ) [NeZero n] (e : TensorProduct K F A ≃ₐ[F] Matrix (Fin n) (Fin n) F) [IsGalois K F] [FiniteDimensional K F] (a : A) : ∃ (f : Polynomial K), ReducedCharPoly e a = (Polynomial.mapAlgHom (Algebra.ofId K F)) f

@[implicit_reducible]

noncomputable def algClosure_ext (L : Type u_1) (F : Type u_2) (F_bar : Type u_3) [Field F] [Field L] [Field F_bar] [Algebra F L] [Algebra F F_bar] [FiniteDimensional F L] [IsAlgClosure F F_bar] : Algebra L F_bar

Equations

• algClosure_ext L F F_bar = (↑IsAlgClosed.lift).toAlgebra

theorem unique_onver_split (K F F_bar A : Type u) [Field K] [Field F] [Field F_bar] [Algebra K F] [Algebra F F_bar] [hF_bar : IsAlgClosure F F_bar] [Ring A] [Algebra K A] [Algebra.IsCentral K A] [IsSimpleRing A] (n : ℕ) [NeZero n] (e : TensorProduct K F A ≃ₐ[F] Matrix (Fin n) (Fin n) F) [IsGalois K F] [FiniteDimensional K F] (L L_bar : Type u) [Field L] [Field L_bar] [Algebra K L] [Algebra L L_bar] [FiniteDimensional K L] [IsGalois K L] [hL : IsAlgClosure L L_bar] (e' : TensorProduct K L A ≃ₐ[L] Matrix (Fin n) (Fin n) L) (a : A) : ∃ (f : Polynomial K) (g : Polynomial K), ReducedCharPoly e a = (Polynomial.mapAlgHom (Algebra.ofId K F)) f ∧ ReducedCharPoly e' a = (Polynomial.mapAlgHom (Algebra.ofId K L)) g ∧ f = g

theorem invariant_extend_scalars (K F A : Type u) [Field K] [Field F] [Algebra K F] [Ring A] [Algebra K A] [Algebra.IsCentral K A] [IsSimpleRing A] (n : ℕ) [NeZero n] (e : TensorProduct K F A ≃ₐ[F] Matrix (Fin n) (Fin n) F) (L L_bar : Type u) [Field L] [Field L_bar] [Algebra F L] [Algebra K L] [Algebra L L_bar] [IsAlgClosure L L_bar] (e0 : TensorProduct F L (TensorProduct K F A) ≃ₐ[L] Matrix (Fin n) (Fin n) L) [IsScalarTower K F L] (a : A) : (Polynomial.mapAlgHom (Algebra.ofId F L)) (ReducedCharPoly e a) = ReducedCharPoly e0 (1 ⊗ₜ[K] a)

theorem invariant_algEquiv (K F : Type u) [Field K] [Field F] [Algebra K F] (n : ℕ) (A1 A2 L : Type u) [Field L] [Algebra K L] [Ring A1] [Ring A2] [Algebra K A1] [Algebra K A2] [Algebra.IsCentral K A1] [Algebra.IsCentral K A2] [IsSimpleRing A1] [IsSimpleRing A2] (e1 : TensorProduct K F A1 ≃ₐ[F] Matrix (Fin n) (Fin n) F) (f : A1 ≃ₐ[K] A2) (a : A1) : ReducedCharPoly e1 a = ReducedCharPoly ((Algebra.TensorProduct.congr AlgEquiv.refl f.symm).trans e1) (f a)

def reducedNorm {K F A : Type u} [Field K] [Field F] [Algebra K F] [Ring A] [Algebra K A] {n : ℕ} (e : TensorProduct K F A ≃ₐ[F] Matrix (Fin n) (Fin n) F) (a : A) : F

Equations

• reducedNorm e a = (e (1 ⊗ₜ[K] a)).det

def reducedTrace {K F A : Type u} [Field K] [Field F] [Algebra K F] [Ring A] [Algebra K A] {n : ℕ} (e : TensorProduct K F A ≃ₐ[F] Matrix (Fin n) (Fin n) F) (a : A) : F

Equations

• reducedTrace e a = (e (1 ⊗ₜ[K] a)).trace

theorem equalMatrixCharpoly (K : Type u) [Field K] (n : ℕ) (M : Matrix (Fin n) (Fin n) K) : ReducedCharPoly (Algebra.TensorProduct.lid K (Matrix (Fin n) (Fin n) K)) M = M.charpoly

theorem reducedNorm_mul (K F A : Type u) [Field K] [Field F] [Algebra K F] [Ring A] [Algebra K A] (n : ℕ) (e : TensorProduct K F A ≃ₐ[F] Matrix (Fin n) (Fin n) F) (a b : A) : reducedNorm e (a * b) = reducedNorm e a * reducedNorm e b

theorem reducedTrace_smul (K F A : Type u) [Field K] [Field F] [Algebra K F] [Ring A] [Algebra K A] (n : ℕ) (e : TensorProduct K F A ≃ₐ[F] Matrix (Fin n) (Fin n) F) (a : A) (r : K) : reducedTrace e (r • a) = r • reducedTrace e a

theorem reducedTrace_mul_comm (K F A : Type u) [Field K] [Field F] [Algebra K F] [Ring A] [Algebra K A] (n : ℕ) (e : TensorProduct K F A ≃ₐ[F] Matrix (Fin n) (Fin n) F) (a b : A) : reducedTrace e (a * b) = reducedTrace e (b * a)

theorem reducedNorm_algebraMap (K F A : Type u) [Field K] [Field F] [Algebra K F] [Ring A] [Algebra K A] (n : ℕ) (e : TensorProduct K F A ≃ₐ[F] Matrix (Fin n) (Fin n) F) (k : K) : reducedNorm e ((algebraMap K A) k) = (algebraMap K F) k ^ n

theorem reducedTrace_algebraMap (K F A : Type u) [Field K] [Field F] [Algebra K F] [Ring A] [Algebra K A] (n : ℕ) (e : TensorProduct K F A ≃ₐ[F] Matrix (Fin n) (Fin n) F) (k : K) : reducedTrace e ((algebraMap K A) k) = n • (algebraMap K F) k

def reducedNormHom (K F A : Type u) [Field K] [Field F] [Algebra K F] [Ring A] [Algebra K A] (n : ℕ) [NeZero n] (e : TensorProduct K F A ≃ₐ[F] Matrix (Fin n) (Fin n) F) : A →*₀ F

Equations

• reducedNormHom K F A n e = { toFun := reducedNorm e, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem reducedNormHom_apply (K F A : Type u) [Field K] [Field F] [Algebra K F] [Ring A] [Algebra K A] (n : ℕ) [NeZero n] (e : TensorProduct K F A ≃ₐ[F] Matrix (Fin n) (Fin n) F) (a : A) : (reducedNormHom K F A n e) a = reducedNorm e a

def reducedTraceLinearMap (K F A : Type u) [Field K] [Field F] [Algebra K F] [Ring A] [Algebra K A] (n : ℕ) (e : TensorProduct K F A ≃ₐ[F] Matrix (Fin n) (Fin n) F) : A →ₗ[K] F

Equations

• reducedTraceLinearMap K F A n e = { toFun := reducedTrace e, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem reducedTraceLinearMap_apply (K F A : Type u) [Field K] [Field F] [Algebra K F] [Ring A] [Algebra K A] (n : ℕ) (e : TensorProduct K F A ≃ₐ[F] Matrix (Fin n) (Fin n) F) (a : A) : (reducedTraceLinearMap K F A n e) a = reducedTrace e a

theorem reducedNorm_ne_zero_iff (K F A : Type u) [Field K] [Field F] [Algebra K F] [Ring A] [Algebra K A] [Algebra.IsCentral K A] [IsSimpleRing A] (n : ℕ) [NeZero n] (e : TensorProduct K F A ≃ₐ[F] Matrix (Fin n) (Fin n) F) (a : A) : reducedNorm e a ≠ 0 ↔ IsUnit a

theorem inv_under_extend (K F A : Type u) [Field K] [Field F] [Algebra K F] [Ring A] [Algebra K A] [Algebra.IsCentral K A] [IsSimpleRing A] (n : ℕ) [NeZero n] (e : TensorProduct K F A ≃ₐ[F] Matrix (Fin n) (Fin n) F) (L L_bar : Type u) [Field L] [Field L_bar] [Algebra F L] [Algebra K L] [Algebra L L_bar] [IsAlgClosure L L_bar] (e0 : TensorProduct F L (TensorProduct K F A) ≃ₐ[L] Matrix (Fin n) (Fin n) L) [IsScalarTower K F L] (a : A) : reducedNorm e0 (1 ⊗ₜ[K] a) = (algebraMap F L) (reducedNorm e a)

theorem inv_under_algEquiv (K F : Type u) [Field K] [Field F] [Algebra K F] (n : ℕ) [NeZero n] (A1 A2 L : Type u) [Field L] [Algebra K L] [Ring A1] [Ring A2] [Algebra K A1] [Algebra K A2] [Algebra.IsCentral K A1] [Algebra.IsCentral K A2] [IsSimpleRing A1] [IsSimpleRing A2] (e1 : TensorProduct K F A1 ≃ₐ[F] Matrix (Fin n) (Fin n) F) (f : A1 ≃ₐ[K] A2) (a : A1) : reducedNorm e1 a = reducedNorm ((Algebra.TensorProduct.congr AlgEquiv.refl f.symm).trans e1) (f a)