restrictNormal_commutes — Mathlib

English

For any x in E, the restricted image under ϕ coincides with the image of x under the base-level map, i.e. the restriction commutes with the base embedding.

Русский

Для любого элемента x∈E ограничение совпадает с базовым отображением; ограничение коммутирует с вложением на основание.

LaTeX

$$$\forall x\in E:\ algebraMap E K_2 (\rho x) = \rho'(algebraMap E K_1 x)$$$

Lean4

@[simp]
theorem restrictNormal_commutes [Normal F E] (x : E) : algebraMap E K₂ (ϕ.restrictNormal E x) = ϕ (algebraMap E K₁ x) :=
  Subtype.ext_iff.mp
    (AlgEquiv.apply_symm_apply (AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F E K₂))
      (ϕ.restrictNormalAux E ⟨IsScalarTower.toAlgHom F E K₁ x, x, rfl⟩))

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