English
Construct a noncomputable AlgEquiv from an AlgEquiv between B and B₂ using galLift, with compatibility through algebraic conditions.
Русский
Построение невычислимого AlgEquiv из AlgEquiv между B и B₂ с использованием galLift и совместимостью с алгебраическими условиями.
LaTeX
$$galLiftEquiv (A) (K) (L) (L₂) (B) (B₂) : AlgEquiv A B B₂ → AlgEquiv K L L₂$$
Lean4
/-- The restriction `End(L/K) → End(B/A)` in an AKLB setup.
Also see `galRestrict` for the `AlgEquiv` version. -/
@[simps -isSimp]
noncomputable def galRestrictHom : (L →ₐ[K] L) ≃* (B →ₐ[A] B)
where
toFun f := galRestrict' A B B f
map_mul' σ₁ σ₂ := galRestrict'_comp _ _ _ _ σ₂ σ₁
invFun := galLift K L L
left_inv σ := galLift_galRestrict' _ _ _ σ
right_inv σ := galRestrict'_galLift _ _ _ σ
