English
If G is finite and G is a Galois group for L/K, then L is finite dimensional over K.
Русский
Если G конечна и является Галуа-группой для L/K, то L является конечномерным над K.
LaTeX
$$[Finite G] \\Rightarrow FiniteDimensional K L$$
Lean4
@[simp]
theorem map_comp {L₁ L₂ L₃ : (FiniteGaloisIntermediateField k K)ᵒᵖ} (f : L₁ ⟶ L₂) (g : L₂ ⟶ L₃) :
finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g :=
by
iterate 2
induction L₁ with
| _ L₁ => ?_
induction L₂ with
| _ L₂ => ?_
induction L₃ with
| _ L₃ => ?_
algebraize [Subsemiring.inclusion g.unop.le, Subsemiring.inclusion f.unop.le,
Subsemiring.inclusion (g.unop.le.trans f.unop.le)]
have : IsScalarTower k L₂ L₁ := IsScalarTower.of_algebraMap_eq' rfl
have : IsScalarTower k L₃ L₁ := IsScalarTower.of_algebraMap_eq' rfl
have : IsScalarTower k L₃ L₂ := IsScalarTower.of_algebraMap_eq' rfl
have : IsScalarTower L₃ L₂ L₁ := IsScalarTower.of_algebraMap_eq' rfl
ext : 1
apply IsScalarTower.AlgEquiv.restrictNormalHom_comp k L₃ L₂ L₁
