English
The action of galLift on an algebra map is compatible with applying σ to the base element.
Русский
Действие galLift на алгебраическую карту совместимо с применением σ к базовому элементу.
LaTeX
$$$\text{galLift }(σ) (\text{algebraMap}_{B}^{L} x) = \text{algebraMap}_{B_2}^{L_2}(σ x)$$$
Lean4
/-- A generalization of the lift `End(B/A) → End(L/K)` in an ALKB setup.
This is inverse to the restriction. See `galRestrictHom`. -/
noncomputable def galLift (σ : B →ₐ[A] B₂) : L →ₐ[K] L₂ :=
haveI := (IsFractionRing.injective A K).isDomain
haveI := NoZeroSMulDivisors.trans_faithfulSMul A K L₂
haveI := IsIntegralClosure.isLocalization A K L B
haveI H : ∀ (y : Algebra.algebraMapSubmonoid B A⁰), IsUnit (((algebraMap B₂ L₂).comp σ) (y : B)) :=
by
rintro ⟨_, x, hx, rfl⟩
simpa only [RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply, AlgHom.commutes, isUnit_iff_ne_zero, ne_eq,
map_eq_zero_iff _ (FaithfulSMul.algebraMap_injective _ _), ← IsScalarTower.algebraMap_apply] using
nonZeroDivisors.ne_zero hx
haveI H_eq : (IsLocalization.lift (S := L) H).comp (algebraMap K L) = (algebraMap K L₂) :=
by
apply IsLocalization.ringHom_ext A⁰
ext
simp only [RingHom.coe_comp, Function.comp_apply, ← IsScalarTower.algebraMap_apply A K L,
← IsScalarTower.algebraMap_apply A K L₂, IsScalarTower.algebraMap_apply A B L,
IsScalarTower.algebraMap_apply A B₂ L₂, IsLocalization.lift_eq, RingHom.coe_coe, AlgHom.commutes]
{ IsLocalization.lift (S := L) H with commutes' := DFunLike.congr_fun H_eq }
