Tensor products over algebraic closures

This file ports auxiliary results about finite intermediate fields inside an algebraic closure and tensor products over their directed union.

theorem dim_eq (K L : Type u) [Field K] [Field L] [Algebra K L] (V : Type u) [AddCommGroup V] [Module K V] [Module.Finite K V] : Module.finrank K V = Module.finrank L (TensorProduct K L V)

noncomputable def intermediateTensor (K K_bar : Type u) [Field K] [Field K_bar] [Algebra K K_bar] (A : Type u) [AddCommGroup A] [Module K A] (L : IntermediateField K K_bar) : Submodule K (TensorProduct K K_bar A)

The image of scalar extension from an intermediate field tensor product.

Equations

• intermediateTensor K K_bar A L = (LinearMap.rTensor A L.val.toLinearMap).range

noncomputable def intermediateTensor' (K K_bar : Type u) [Field K] [Field K_bar] [Algebra K K_bar] (A : Type u) [AddCommGroup A] [Module K A] (L : IntermediateField K K_bar) : Submodule (↥L) (TensorProduct K K_bar A)

The same image as intermediateTensor, regarded as a module over the intermediate field.

Equations

• intermediateTensor' K K_bar A L = (let __src := LinearMap.rTensor A L.val.toLinearMap; { toAddHom := __src.toAddHom, map_smul' := ⋯ }).range

noncomputable def intermediateTensorEquiv (K K_bar : Type u) [Field K] [Field K_bar] [Algebra K K_bar] (A : Type u) [AddCommGroup A] [Module K A] (L : IntermediateField K K_bar) : ↥(intermediateTensor K K_bar A L) ≃ₗ[K] TensorProduct K (↥L) A

The range-restricted tensor map identifies an intermediate tensor with L ⊗[K] A.

Equations

• intermediateTensorEquiv K K_bar A L = (LinearEquiv.ofBijective (LinearMap.rTensor A L.val.toLinearMap).rangeRestrict ⋯).symm

@[simp]

theorem intermediateTensorEquiv_apply_tmul (K K_bar : Type u) [Field K] [Field K_bar] [Algebra K K_bar] (A : Type u) [AddCommGroup A] [Module K A] (L : IntermediateField K K_bar) (x : ↥L) (a : A) (h : ↑x ⊗ₜ[K] a ∈ intermediateTensor K K_bar A L) : (intermediateTensorEquiv K K_bar A L) ⟨↑x ⊗ₜ[K] a, h⟩ = x ⊗ₜ[K] a

noncomputable def intermediateTensorEquiv' (K K_bar : Type u) [Field K] [Field K_bar] [Algebra K K_bar] (A : Type u) [AddCommGroup A] [Module K A] (L : IntermediateField K K_bar) : ↥(intermediateTensor' K K_bar A L) ≃ₗ[↥L] TensorProduct K (↥L) A

The L-linear version of intermediateTensorEquiv.

Equations

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

theorem mem_intermediateTensor_iff_mem_intermediateTensor' (K K_bar : Type u) [Field K] [Field K_bar] [Algebra K K_bar] (A : Type u) [AddCommGroup A] [Module K A] {L : IntermediateField K K_bar} {x : TensorProduct K K_bar A} : x ∈ intermediateTensor K K_bar A L ↔ x ∈ intermediateTensor' K K_bar A L

theorem intermediateTensor_mono (K K_bar : Type u) [Field K] [Field K_bar] [Algebra K K_bar] (A : Type u) [AddCommGroup A] [Module K A] {L1 L2 : IntermediateField K K_bar} (h : L1 ≤ L2) : intermediateTensor K K_bar A L1 ≤ intermediateTensor K K_bar A L2

@[reducible, inline]

noncomputable abbrev SetOfFinite (K K_bar : Type u) [Field K] [Field K_bar] [Algebra K K_bar] : Set (IntermediateField K K_bar)

Finite-dimensional intermediate fields of the algebraic closure.

Equations

• SetOfFinite K K_bar = {M : IntermediateField K K_bar | FiniteDimensional K ↥M}

theorem is_direct (K K_bar : Type u) [Field K] [Field K_bar] [Algebra K K_bar] (A : Type u) [AddCommGroup A] [Module K A] : DirectedOn (fun (x x_1 : Submodule K (TensorProduct K K_bar A)) => x ≤ x_1) (Set.range fun (L : ↑(SetOfFinite K K_bar)) => intermediateTensor K K_bar A ↑L)

theorem SetOfFinite_nonempty (K K_bar : Type u) [Field K] [Field K_bar] [Algebra K K_bar] (A : Type u) [AddCommGroup A] [Module K A] : (Set.range fun (L : ↑(SetOfFinite K K_bar)) => intermediateTensor K K_bar A ↑L).Nonempty

theorem inter_tensor_union (K K_bar : Type u) [Field K] [Field K_bar] [Algebra K K_bar] [IsAlgClosure K K_bar] (A : Type u) [AddCommGroup A] [Module K A] : ⨆ (L : ↑(SetOfFinite K K_bar)), intermediateTensor K K_bar A ↑L = ⊤

K_bar ⊗[K] A = union of all finite subextension of K ⊗ A

theorem algclosure_element_in (K K_bar : Type u) [Field K] [Field K_bar] [Algebra K K_bar] [IsAlgClosure K K_bar] (A : Type u) [AddCommGroup A] [Module K A] (x : TensorProduct K K_bar A) : ∃ (F : IntermediateField K K_bar), FiniteDimensional K ↥F ∧ x ∈ intermediateTensor K K_bar A F

noncomputable def subfieldOf (K K_bar : Type u) [Field K] [Field K_bar] [Algebra K K_bar] [IsAlgClosure K K_bar] (A : Type u) [AddCommGroup A] [Module K A] (x : TensorProduct K K_bar A) : IntermediateField K K_bar

A finite intermediate field whose tensor image contains a chosen tensor element.

Equations

• subfieldOf K K_bar A x = ⋯.choose

instance instFiniteDimensionalSubtypeMemIntermediateFieldSubfieldOf (K K_bar : Type u) [Field K] [Field K_bar] [Algebra K K_bar] [IsAlgClosure K K_bar] (A : Type u) [AddCommGroup A] [Module K A] (x : TensorProduct K K_bar A) : FiniteDimensional K ↥(subfieldOf K K_bar A x)

theorem mem_subfieldOf (K K_bar : Type u) [Field K] [Field K_bar] [Algebra K K_bar] [IsAlgClosure K K_bar] (A : Type u) [AddCommGroup A] [Module K A] (x : TensorProduct K K_bar A) : x ∈ intermediateTensor K K_bar A (subfieldOf K K_bar A x)

theorem mem_subfieldOf' (K K_bar : Type u) [Field K] [Field K_bar] [Algebra K K_bar] [IsAlgClosure K K_bar] (A : Type u) [AddCommGroup A] [Module K A] (x : TensorProduct K K_bar A) : x ∈ intermediateTensor' K K_bar A (subfieldOf K K_bar A x)

noncomputable def lemmaTto.ee (n : ℕ) (k k_bar A : Type u) [Field k] [Field k_bar] [Algebra k k_bar] [Ring A] [Algebra k A] (iso : TensorProduct k k_bar A ≃ₐ[k_bar] Matrix (Fin n) (Fin n) k_bar) : Module.Basis (Fin n × Fin n) k_bar (TensorProduct k k_bar A)

The basis of k_bar ⊗[k] A pulled back from the standard matrix basis.

Equations

• lemmaTto.ee n k k_bar A iso = (Matrix.stdBasis k_bar (Fin n) (Fin n)).map ↑iso.symm

@[simp]

theorem lemmaTto.ee_apply (n : ℕ) (k k_bar A : Type u) [Field k] [Field k_bar] [Algebra k k_bar] [Ring A] [Algebra k A] (iso : TensorProduct k k_bar A ≃ₐ[k_bar] Matrix (Fin n) (Fin n) k_bar) (i : Fin n × Fin n) : iso ((ee n k k_bar A iso) i) = (Matrix.stdBasis k_bar (Fin n) (Fin n)) i

noncomputable def lemmaTto.ℒℒ (n : ℕ) (k k_bar A : Type u) [Field k] [Field k_bar] [Algebra k k_bar] [IsAlgClosure k k_bar] [Ring A] [Algebra k A] (iso : TensorProduct k k_bar A ≃ₐ[k_bar] Matrix (Fin n) (Fin n) k_bar) : IntermediateField k k_bar

The finite intermediate field generated by all basis coordinates.

Equations

• lemmaTto.ℒℒ n k k_bar A iso = ⨆ (i : Fin n × Fin n), subfieldOf k k_bar A ((lemmaTto.ee n k k_bar A iso) i)

instance lemmaTto.instFiniteDimensionalSubtypeMemIntermediateFieldℒℒ (n : ℕ) (k k_bar A : Type u) [Field k] [Field k_bar] [Algebra k k_bar] [IsAlgClosure k k_bar] [Ring A] [Algebra k A] (iso : TensorProduct k k_bar A ≃ₐ[k_bar] Matrix (Fin n) (Fin n) k_bar) : FiniteDimensional k ↥(ℒℒ n k k_bar A iso)

noncomputable def lemmaTto.f (n : ℕ) (k k_bar A : Type u) [Field k] [Field k_bar] [Algebra k k_bar] [IsAlgClosure k k_bar] [Ring A] [Algebra k A] (iso : TensorProduct k k_bar A ≃ₐ[k_bar] Matrix (Fin n) (Fin n) k_bar) (i : Fin n × Fin n) : ↥(subfieldOf k k_bar A ((ee n k k_bar A iso) i)) →ₐ[k] ↥(ℒℒ n k k_bar A iso)

Inclusion of the coordinate field of a basis vector into the generated field ℒ.

Equations

• lemmaTto.f n k k_bar A iso i = IntermediateField.inclusion ⋯

noncomputable def lemmaTto.eHat' (n : ℕ) (k k_bar A : Type u) [Field k] [Field k_bar] [Algebra k k_bar] [IsAlgClosure k k_bar] [Ring A] [Algebra k A] (iso : TensorProduct k k_bar A ≃ₐ[k_bar] Matrix (Fin n) (Fin n) k_bar) (i : Fin n × Fin n) : ↥(intermediateTensor' k k_bar A (ℒℒ n k k_bar A iso))

The pulled-back basis vector, regarded in the ℒ-linear intermediate tensor submodule.

Equations

• lemmaTto.eHat' n k k_bar A iso i = ⟨(lemmaTto.ee n k k_bar A iso) i, ⋯⟩

theorem lemmaTto.eHat_linear_independent (n : ℕ) (k k_bar A : Type u) [Field k] [Field k_bar] [Algebra k k_bar] [IsAlgClosure k k_bar] [Ring A] [Algebra k A] (iso : TensorProduct k k_bar A ≃ₐ[k_bar] Matrix (Fin n) (Fin n) k_bar) : LinearIndependent (↥(ℒℒ n k k_bar A iso)) (eHat' n k k_bar A iso)

@[implicit_reducible]

noncomputable instance lemmaTto.instModuleSubtypeMemIntermediateFieldℒℒTensorProduct (n : ℕ) (k k_bar A : Type u) [Field k] [Field k_bar] [Algebra k k_bar] [IsAlgClosure k k_bar] [Ring A] [Algebra k A] (iso : TensorProduct k k_bar A ≃ₐ[k_bar] Matrix (Fin n) (Fin n) k_bar) : Module (↥(ℒℒ n k k_bar A iso)) (TensorProduct k (↥(ℒℒ n k k_bar A iso)) A)

Equations

• lemmaTto.instModuleSubtypeMemIntermediateFieldℒℒTensorProduct n k k_bar A iso = TensorProduct.leftModule

instance lemmaTto.instFiniteDimensionalSubtypeMemIntermediateFieldℒℒTensorProductSubmoduleIntermediateTensor' (n : ℕ) (k k_bar A : Type u) [Field k] [Field k_bar] [Algebra k k_bar] [IsAlgClosure k k_bar] [Ring A] [Algebra k A] [FiniteDimensional k A] (iso : TensorProduct k k_bar A ≃ₐ[k_bar] Matrix (Fin n) (Fin n) k_bar) : FiniteDimensional ↥(ℒℒ n k k_bar A iso) ↥(intermediateTensor' k k_bar A (ℒℒ n k k_bar A iso))

theorem lemmaTto.dim_ℒ_eq (n : ℕ) (k k_bar A : Type u) [Field k] [Field k_bar] [Algebra k k_bar] [IsAlgClosure k k_bar] [Ring A] [Algebra k A] [FiniteDimensional k A] (iso : TensorProduct k k_bar A ≃ₐ[k_bar] Matrix (Fin n) (Fin n) k_bar) : Module.finrank ↥(ℒℒ n k k_bar A iso) ↥(intermediateTensor' k k_bar A (ℒℒ n k k_bar A iso)) = n ^ 2

noncomputable def lemmaTto.eHat (n : ℕ) [NeZero n] (k k_bar A : Type u) [Field k] [Field k_bar] [Algebra k k_bar] [IsAlgClosure k k_bar] [Ring A] [Algebra k A] [FiniteDimensional k A] (iso : TensorProduct k k_bar A ≃ₐ[k_bar] Matrix (Fin n) (Fin n) k_bar) : Module.Basis (Fin n × Fin n) ↥(ℒℒ n k k_bar A iso) ↥(intermediateTensor' k k_bar A (ℒℒ n k k_bar A iso))

The basis of the intermediate tensor submodule over ℒ.

Equations

• lemmaTto.eHat n k k_bar A iso = basisOfLinearIndependentOfCardEqFinrank ⋯ ⋯

noncomputable def lemmaTto.isoRestrict' (n : ℕ) [NeZero n] (k k_bar A : Type u) [Field k] [Field k_bar] [Algebra k k_bar] [IsAlgClosure k k_bar] [Ring A] [Algebra k A] [FiniteDimensional k A] (iso : TensorProduct k k_bar A ≃ₐ[k_bar] Matrix (Fin n) (Fin n) k_bar) : TensorProduct k (↥(ℒℒ n k k_bar A iso)) A ≃ₗ[↥(ℒℒ n k k_bar A iso)] Matrix (Fin n) (Fin n) ↥(ℒℒ n k k_bar A iso)

The restricted linear equivalence over the finite intermediate field ℒ.

Equations

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

instance lemmaTto.instSMulCommClassSubtypeMemIntermediateFieldℒℒ (n : ℕ) (k k_bar A : Type u) [Field k] [Field k_bar] [Algebra k k_bar] [IsAlgClosure k k_bar] [Ring A] [Algebra k A] (iso : TensorProduct k k_bar A ≃ₐ[k_bar] Matrix (Fin n) (Fin n) k_bar) : SMulCommClass k ↥(ℒℒ n k k_bar A iso) ↥(ℒℒ n k k_bar A iso)

noncomputable def lemmaTto.inclusion (n : ℕ) (k k_bar A : Type u) [Field k] [Field k_bar] [Algebra k k_bar] [IsAlgClosure k k_bar] [Ring A] [Algebra k A] (iso : TensorProduct k k_bar A ≃ₐ[k_bar] Matrix (Fin n) (Fin n) k_bar) : TensorProduct k (↥(ℒℒ n k k_bar A iso)) A →ₐ[↥(ℒℒ n k k_bar A iso)] TensorProduct k k_bar A

Scalar-extension inclusion from the restricted tensor product into the algebraic closure.

Equations

• lemmaTto.inclusion n k k_bar A iso = Algebra.TensorProduct.map (Algebra.ofId (↥(lemmaTto.ℒℒ n k k_bar A iso)) k_bar) (AlgHom.id k A)

noncomputable def lemmaTto.inclusion' (n : ℕ) (k k_bar A : Type u) [Field k] [Field k_bar] [Algebra k k_bar] [IsAlgClosure k k_bar] [Ring A] [Algebra k A] (iso : TensorProduct k k_bar A ≃ₐ[k_bar] Matrix (Fin n) (Fin n) k_bar) : Matrix (Fin n) (Fin n) ↥(ℒℒ n k k_bar A iso) →ₐ[↥(ℒℒ n k k_bar A iso)] Matrix (Fin n) (Fin n) k_bar

Entrywise matrix inclusion from ℒ to the algebraic closure.

Equations

• lemmaTto.inclusion' n k k_bar A iso = (Algebra.ofId (↥(lemmaTto.ℒℒ n k k_bar A iso)) k_bar).mapMatrix

theorem lemmaTto.inclusion'_injective (n : ℕ) (k k_bar A : Type u) [Field k] [Field k_bar] [Algebra k k_bar] [IsAlgClosure k k_bar] [Ring A] [Algebra k A] (iso : TensorProduct k k_bar A ≃ₐ[k_bar] Matrix (Fin n) (Fin n) k_bar) : Function.Injective ⇑(inclusion' n k k_bar A iso)

theorem lemmaTto.comm_triangle (n : ℕ) (k k_bar A : Type u) [Field k] [Field k_bar] [Algebra k k_bar] [IsAlgClosure k k_bar] [Ring A] [Algebra k A] (iso : TensorProduct k k_bar A ≃ₐ[k_bar] Matrix (Fin n) (Fin n) k_bar) : (intermediateTensor' k k_bar A (ℒℒ n k k_bar A iso)).subtype ∘ₗ ↑(intermediateTensorEquiv' k k_bar A (ℒℒ n k k_bar A iso)).symm = (inclusion n k k_bar A iso).toLinearMap

ℒ ⊗_k A ------> intermidateTensor | / | inclusion / v / k⁻ ⊗_k A <-

theorem lemmaTto.comm_square' (n : ℕ) [NeZero n] (k k_bar A : Type u) [Field k] [Field k_bar] [Algebra k k_bar] [IsAlgClosure k k_bar] [Ring A] [Algebra k A] [FiniteDimensional k A] (iso : TensorProduct k k_bar A ≃ₐ[k_bar] Matrix (Fin n) (Fin n) k_bar) : ↑↥(ℒℒ n k k_bar A iso) ↑↑iso ∘ₗ (intermediateTensor' k k_bar A (ℒℒ n k k_bar A iso)).subtype = (inclusion' n k k_bar A iso).toLinearMap ∘ₗ ↑((eHat n k k_bar A iso).equiv (Matrix.stdBasis (↥(ℒℒ n k k_bar A iso)) (Fin n) (Fin n)) (Equiv.refl (Fin n × Fin n)))

intermidateTensor ----> M_n(ℒ) | val | inclusion' v v k⁻ ⊗_k A ----------> M_n(k⁻) iso

theorem lemmaTto.comm_square (n : ℕ) [NeZero n] (k k_bar A : Type u) [Field k] [Field k_bar] [Algebra k k_bar] [IsAlgClosure k k_bar] [Ring A] [Algebra k A] [FiniteDimensional k A] (iso : TensorProduct k k_bar A ≃ₐ[k_bar] Matrix (Fin n) (Fin n) k_bar) : (inclusion' n k k_bar A iso).toLinearMap ∘ₗ ↑(isoRestrict' n k k_bar A iso) = ↑↥(ℒℒ n k k_bar A iso) ↑↑iso ∘ₗ (inclusion n k k_bar A iso).toLinearMap

This shows the following diagram commutes: isoRestrict ℒ ⊗_k A -----> M_n(ℒ) | inclusion | inclusion' v v k⁻ ⊗_k A -----> M_n(k⁻) iso

theorem lemmaTto.isoRestrict_map_one (n : ℕ) [NeZero n] (k k_bar A : Type u) [Field k] [Field k_bar] [Algebra k k_bar] [IsAlgClosure k k_bar] [Ring A] [Algebra k A] [FiniteDimensional k A] (iso : TensorProduct k k_bar A ≃ₐ[k_bar] Matrix (Fin n) (Fin n) k_bar) : (isoRestrict' n k k_bar A iso) 1 = 1

theorem lemmaTto.isoRestrict_map_mul (n : ℕ) [NeZero n] (k k_bar A : Type u) [Field k] [Field k_bar] [Algebra k k_bar] [IsAlgClosure k k_bar] [Ring A] [Algebra k A] [FiniteDimensional k A] (iso : TensorProduct k k_bar A ≃ₐ[k_bar] Matrix (Fin n) (Fin n) k_bar) (x y : TensorProduct k (↥(ℒℒ n k k_bar A iso)) A) : (isoRestrict' n k k_bar A iso) (x * y) = (isoRestrict' n k k_bar A iso) x * (isoRestrict' n k k_bar A iso) y

noncomputable def lemmaTto.isoRestrict (n : ℕ) [NeZero n] (k k_bar A : Type u) [Field k] [Field k_bar] [Algebra k k_bar] [IsAlgClosure k k_bar] [Ring A] [Algebra k A] [FiniteDimensional k A] (iso : TensorProduct k k_bar A ≃ₐ[k_bar] Matrix (Fin n) (Fin n) k_bar) : TensorProduct k (↥(ℒℒ n k k_bar A iso)) A ≃ₐ[↥(ℒℒ n k k_bar A iso)] Matrix (Fin n) (Fin n) ↥(ℒℒ n k k_bar A iso)

The restricted algebra equivalence over the finite intermediate field ℒ.

Equations

• lemmaTto.isoRestrict n k k_bar A iso = AlgEquiv.ofLinearEquiv (lemmaTto.isoRestrict' n k k_bar A iso) ⋯ ⋯