galRestrict — Mathlib

English

Applying galRestrict to σ and x yields the same value as galRestrictHom.

Русский

Применение galRestrict к σ и x даёт такое же значение, как и galRestrictHom.

LaTeX

$$galRestrict_apply (σ : L ≃ₐ[K] L) (x : B) : galRestrict A K L B σ x = galRestrictHom A K L B σ x$$

Lean4

/-- The restriction `Aut(L/K) → Aut(B/A)` in an AKLB setup. -/
noncomputable def galRestrict : (L ≃ₐ[K] L) ≃* (B ≃ₐ[A] B) :=
  (AlgEquiv.algHomUnitsEquiv K L).symm.trans
    ((Units.mapEquiv <| galRestrictHom A K L B).trans (AlgEquiv.algHomUnitsEquiv A B))

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