galLiftEquiv — Mathlib

English

There exists an equivalent lifting between B and B₂ that yields a natural isomorphism between L and L₂ via an AlgEquiv.

Русский

Существует эквивалентный подъем между B и B₂, задающий натуральное изоморфизм между L и L₂ через AlgEquiv.

LaTeX

$$galLiftEquiv (A) (K) (L) (L₂) (B) (B₂) : AlgEquiv A B B₂ → AlgEquiv K L L₂$$

Lean4

/-- A version of `galLift` for `AlgEquiv`.
-/
@[simps! -fullyApplied apply symm_apply]
noncomputable def galLiftEquiv [Algebra.IsAlgebraic K L₂] (σ : B ≃ₐ[A] B₂) : L ≃ₐ[K] L₂ :=
  AlgEquiv.ofAlgHom (galLift K L L₂ σ.toAlgHom) (galLift K L₂ L σ.symm.toAlgHom) (by simp [← galLift_comp])
    (by simp [← galLift_comp])

Похожие утверждения