finGaloisGroupFunctor_map_proj_eq_proj

English

The functor from finite Galois intermediate fields to finite groups assigns to each L the Gal(L/k).

Русский

Функтор от конечных Галуа-подполей к конечным группам сопоставляет каждому L группу Gal(L/k).

LaTeX

$$finGaloisGroupFunctor : (FiniteGaloisIntermediateField k K)ᵒᵖ ⥤ FiniteGrp$$

Lean4

theorem finGaloisGroupFunctor_map_proj_eq_proj (g : limit (asProfiniteGaloisGroupFunctor k K))
    {L₁ L₂ : FiniteGaloisIntermediateField k K} (h : L₁ ⟶ L₂) :
    (finGaloisGroupFunctor k K).map h.op (proj L₂ g) = proj L₁ g :=
  g.prop h.op

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