BrauerGroup.AlgClosedUnion

source

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)

source

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)

Equations

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

Instances For

source

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)

Equations

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

Instances For

source

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

Equations

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

Instances For

source

@[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

source

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

Equations

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

Instances For

source

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

source

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

source

@[reducible, inline]

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

Set (IntermediateField K K_bar)

Equations

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

Instances For

source

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)

source

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

source

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

source

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

source

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

Equations

subfieldOf K K_bar A x = ⋯.choose

Instances For

source

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)

source

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)

source

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)

source

noncomputable def lemma_tto.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) :

Basis (Fin n × Fin n) k_bar (TensorProduct k k_bar A)

Equations

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

Instances For

source

@[simp]

theorem lemma_tto.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

source

noncomputable def lemma_tto.ℒℒ (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

Equations

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

Instances For

source

instance lemma_tto.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)

source

noncomputable def lemma_tto.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)

Equations

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

Instances For

source

noncomputable def lemma_tto.e_hat' (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))

Equations

lemma_tto.e_hat' n k k_bar A iso i = ⟨(lemma_tto.ee n k k_bar A iso) i, ⋯⟩

Instances For

source

theorem lemma_tto.e_hat_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)) (e_hat' n k k_bar A iso)

source

noncomputable instance lemma_tto.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

lemma_tto.instModuleSubtypeMemIntermediateFieldℒℒTensorProduct n k k_bar A iso = TensorProduct.leftModule

source

instance lemma_tto.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))

source

theorem lemma_tto.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

source

noncomputable def lemma_tto.e_hat (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) :

Basis (Fin n × Fin n) ↥(ℒℒ n k k_bar A iso) ↥(intermediateTensor' k k_bar A (ℒℒ n k k_bar A iso))

Equations

lemma_tto.e_hat n k k_bar A iso = basisOfLinearIndependentOfCardEqFinrank ⋯ ⋯

Instances For

source

noncomputable def lemma_tto.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)

Equations

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

Instances For

source

instance lemma_tto.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)

source

noncomputable def lemma_tto.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

Equations

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

Instances For

source

noncomputable def lemma_tto.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

Equations

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

Instances For

source

theorem lemma_tto.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)

source

theorem lemma_tto.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 <-

source

theorem lemma_tto.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.toLinearEquiv ∘ₗ (intermediateTensor' k k_bar A (ℒℒ n k k_bar A iso)).subtype = (inclusion' n k k_bar A iso).toLinearMap ∘ₗ ↑((e_hat 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

source

theorem lemma_tto.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.toLinearEquiv ∘ₗ (inclusion n k k_bar A iso).toLinearMap

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

source

theorem lemma_tto.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

source

theorem lemma_tto.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

source

noncomputable def lemma_tto.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)

Equations

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

Instances For