English
For fields k,K and central K-algebra D with IsCentral K D, the base-field map is bijective: algebraMap k K is bijective.
Русский
Для полей k,K и центральной K-алгебры D, где IsCentral K D, отображение алгебрации алгебр от k к K биективно.
LaTeX
$$$\\text{Function.Bijective} (\\operatorname{algebraMap} k K)$$$
Lean4
theorem baseField_essentially_unique (k K D : Type*) [Field k] [Field K] [Ring D] [Nontrivial D] [Algebra k K]
[Algebra K D] [Algebra k D] [IsScalarTower k K D] [IsCentral k D] : Function.Bijective (algebraMap k K) :=
by
haveI : IsCentral K D :=
{
out := fun x ↦
show x ∈ Subalgebra.center k D → _
by
simp only [center_eq_bot, mem_bot, Set.mem_range, forall_exists_index]
rintro x rfl
exact ⟨algebraMap k K x, by simp [algebraMap_eq_smul_one, smul_assoc]⟩ }
refine ⟨FaithfulSMul.algebraMap_injective k K, fun x => ?_⟩
have H : algebraMap K D x ∈ (Subalgebra.center K D : Set D) := Subalgebra.algebraMap_mem _ _
rw [show (Subalgebra.center K D : Set D) = Subalgebra.center k D by rfl] at H
simp only [center_eq_bot, coe_bot, Set.mem_range] at H
obtain ⟨x', H⟩ := H
exact ⟨x', (algebraMap K D).injective <| by simp [← H, algebraMap_eq_smul_one]⟩
