English
Restriction maps between Gal(L1/k) and Gal(L2/k) are group homomorphisms compatible with inclusion.
Русский
Ограничение между Gal(L1/k) и Gal(L2/k) образует гомоморфизм группы, совместимый с вложением.
LaTeX
$$finGaloisGroupMap : {L1 L2 : Opposite (FiniteGaloisIntermediateField k K)} → L1.unop.finGaloisGroup ⟶ L2.unop.finGaloisGroup$$
Lean4
theorem proj_of_le (L : FiniteGaloisIntermediateField k K) (g : limit (asProfiniteGaloisGroupFunctor k K)) (x : L)
(L' : FiniteGaloisIntermediateField k K) (h : L ≤ L') : (proj L g x).val = (proj L' g ⟨x, h x.2⟩).val :=
by
induction L with
| _ L => ?_
induction L' with
| _ L' => ?_
letI : Algebra L L' := RingHom.toAlgebra (Subsemiring.inclusion h)
letI : IsScalarTower k L L' := IsScalarTower.of_algebraMap_eq (congrFun rfl)
rw [← finGaloisGroupFunctor_map_proj_eq_proj g h.hom]
change (algebraMap L' K (algebraMap L L' (AlgEquiv.restrictNormal (proj (mk L') g) L x))) = _
rw [AlgEquiv.restrictNormal_commutes (proj (mk L') g) L]
rfl
