English
If k contains B/Q and σ is an A ⧸ P-algebra automorphism of k, there exists an A ⧸ P-algebra automorphism τ of B/Q such that τ and σ agree after passing to k via the quotient map.
Русский
Если k содержит B/Q и σ - автоморфизм алгебры над A ⧸ P, существует автоморфизм τ алгебры над A ⧸ P на B/Q, такой что они согласованы через отображение к k.
LaTeX
$$$\\exists \\tau : (B/Q) \\simeq_{A/P} (B/Q),\\ \\forall x:\\ B/Q,\\ algebraMap_{A/P}(\\tau x) = \\sigma( algebraMap_{(B/Q)\\to k} x).$$$
Lean4
/-- For any domain `k` containing `B ⧸ Q`,
any endomorphism of `k` can be restricted to an endomorphism of `B ⧸ Q`.
-/
theorem exists_algEquiv_fixedPoint_quotient_under (σ : k ≃ₐ[A ⧸ P] k) :
∃ τ : (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q, ∀ x : B ⧸ Q, algebraMap _ _ (τ x) = σ (algebraMap (B ⧸ Q) k x) :=
by
let f : (B ⧸ Q) →ₐ[A ⧸ P] k := IsScalarTower.toAlgHom _ _ _
have hf : Function.Injective f := FaithfulSMul.algebraMap_injective _ _
obtain ⟨τ₁, h₁⟩ := Ideal.Quotient.exists_algHom_fixedPoint_quotient_under G P Q σ.toAlgHom
obtain ⟨τ₂, h₂⟩ := Ideal.Quotient.exists_algHom_fixedPoint_quotient_under G P Q σ.symm.toAlgHom
refine ⟨{ __ := τ₁, invFun := τ₂, left_inv := ?_, right_inv := ?_ }, h₁⟩
· intro x
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
obtain ⟨y, e⟩ := Ideal.Quotient.mk_surjective (τ₁ (Ideal.Quotient.mk Q x))
apply hf
dsimp [f] at h₁ h₂ ⊢
refine .trans ?_ (σ.symm_apply_apply _)
rw [← h₁, ← e, h₂]
· intro x
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
obtain ⟨y, e⟩ := Ideal.Quotient.mk_surjective (τ₂ (Ideal.Quotient.mk Q x))
apply hf
dsimp [f] at h₁ h₂ ⊢
refine .trans ?_ (σ.apply_symm_apply _)
rw [← h₂, ← e, h₁]
