liftAlgEquiv — Mathlib

English

There is an algebra isomorphism between F and lift F, given by lifting elements of F into its lift.

Русский

Существует алгебраическое изоморфизм между F и lift F, задаваемый подъёмом элементов F в их подъем.

LaTeX

$$$\\text{liftAlgEquiv} : F \\simeq_A^K \\operatorname{lift}F$$$

Lean4

/-- The algEquiv between an intermediate field and its lift. -/
def liftAlgEquiv {E : IntermediateField K L} (F : IntermediateField K E) : ↥F ≃ₐ[K] lift F
    where
  toFun x := ⟨x.1.1, (mem_lift x.1).mpr x.2⟩
  invFun x := ⟨⟨x.1, lift_le F x.2⟩, (mem_lift ⟨x.1, lift_le F x.2⟩).mp x.2⟩
  left_inv := congrFun rfl
  right_inv := congrFun rfl
  map_mul' _ _ := rfl
  map_add' _ _ := rfl
  commutes' _ := rfl

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