English
In the AKLB framework, the action of the automorphism group Aut(B/A) on B yields an invariant A-substructure: Algebra.IsInvariant A B (AlgEquiv K L L).
Русский
В рамках AKLB действие группы автоморфизмов Aut(B/A) на B оставляет инвариантную подструктуру над A.
LaTeX
$$$\text{Algebra.IsInvariant } A B (\text{AlgEquiv } K L L).$$$
Lean4
/-- In the AKLB setup, every fixed point of `B` lies in the image of `A`. -/
theorem isInvariant_of_isGalois [FiniteDimensional K L] [h : IsGalois K L] :
letI := IsIntegralClosure.MulSemiringAction A K L B
Algebra.IsInvariant A B (L ≃ₐ[K] L) :=
by
replace h := ((IsGalois.tfae (F := K) (E := L)).out 0 1).mp h
letI := IsIntegralClosure.MulSemiringAction A K L B
refine ⟨fun b hb ↦ ?_⟩
replace hb : algebraMap B L b ∈ IntermediateField.fixedField (⊤ : Subgroup (L ≃ₐ[K] L)) :=
by
rintro ⟨g, -⟩
exact (algebraMap_galRestrict_apply A g b).symm.trans (congrArg (algebraMap B L) (hb g))
rw [h, IntermediateField.mem_bot] at hb
obtain ⟨k, hk⟩ := hb
have hb : IsIntegral A b := IsIntegralClosure.isIntegral A L b
rw [← isIntegral_algebraMap_iff (FaithfulSMul.algebraMap_injective B L), ← hk,
isIntegral_algebraMap_iff (FaithfulSMul.algebraMap_injective K L)] at hb
obtain ⟨a, rfl⟩ := IsIntegrallyClosed.algebraMap_eq_of_integral hb
rw [← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply A B L,
(FaithfulSMul.algebraMap_injective B L).eq_iff] at hk
exact ⟨a, hk⟩
