proj_adjoin_singleton_val — Mathlib

English

The identity morphism maps to the identity in the corresponding Gal(L/k).

Русский

Идентичность отображает тождественный Галуа-образ.

LaTeX

$$map_id (L) : finGaloisGroupMap (𝟙 L) = 𝟙 L.unop.finGaloisGroup$$

Lean4

theorem proj_adjoin_singleton_val [IsGalois k K] (g : limit (asProfiniteGaloisGroupFunctor k K)) (x : K)
    (y : adjoin k { x }) (L : FiniteGaloisIntermediateField k K) (h : x ∈ L.toIntermediateField) :
    (proj (adjoin k { x }) g y).val = (proj L g ⟨y, adjoin_simple_le_iff.mpr h y.2⟩).val :=
  proj_of_le _ g y _ _

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