English
For appropriate rings and algebras, galRestrict' is equal to the composition of a canonical isomorphism and the restriction/codRestrict maps through integral closures.
Русский
Для подходящих колец и алгебр galRestrict' совпадает с композицией канонического изоморфизма и ограничений через интегральное замыкание.
LaTeX
$$galRestrict'(A,B,B₂,f) = IsIntegralClosure.equiv(A, ...).toAlgHom ∘ (restrictScalars A f) ∘ (codRestrict (integralClosure A L₂)) ∘ (...)$$
Lean4
/-- A generalization of `galRestrictHom` beyond endomorphisms. -/
noncomputable def galRestrict' (f : L →ₐ[K] L₂) : (B →ₐ[A] B₂) :=
(IsIntegralClosure.equiv A (integralClosure A L₂) L₂ B₂).toAlgHom.comp
(((f.restrictScalars A).comp (IsScalarTower.toAlgHom A B L)).codRestrict (integralClosure A L₂)
(fun x ↦ IsIntegral.map _ (IsIntegralClosure.isIntegral A L x)))
