English
For a field extension L/K, galGroupBasis is the group filter basis on Aut_K(L) whose sets are Gal(L/E) for finite E/K.
Русский
Для расширения L/K галGroupBasis — это групповая фильтр-база над Aut_K(L), картина Gal(L/E) для конечных E/K.
LaTeX
$$$galGroupBasis(K,L): GroupFilterBasis(Aut_K(L))$ with sets $Gal(L/E)$, $E/K$ finite$$
Lean4
/-- For a field extension `L/K`, `galGroupBasis K L` is the group filter basis on `L ≃ₐ[K] L`
whose sets are `Gal(L/E)` for finite subextensions `E/K`. -/
def galGroupBasis (K L : Type*) [Field K] [Field L] [Algebra K L] : GroupFilterBasis (L ≃ₐ[K] L)
where
toFilterBasis := galBasis K L
one' := fun ⟨H, _, h2⟩ => h2 ▸ H.one_mem
mul' {U}
hU :=
⟨U, hU, by
rcases hU with ⟨H, _, rfl⟩
rintro x ⟨a, haH, b, hbH, rfl⟩
exact H.mul_mem haH hbH⟩
inv' {U}
hU :=
⟨U, hU, by
rcases hU with ⟨H, _, rfl⟩
exact fun _ => H.inv_mem'⟩
conj' := by
rintro σ U ⟨H, ⟨E, hE, rfl⟩, rfl⟩
let F : IntermediateField K L := E.map σ.symm.toAlgHom
refine ⟨F.fixingSubgroup.carrier, ⟨⟨F.fixingSubgroup, ⟨F, ?_, rfl⟩, rfl⟩, fun g hg => ?_⟩⟩
· have : FiniteDimensional K E := hE
exact IntermediateField.finiteDimensional_map σ.symm.toAlgHom
change σ * g * σ⁻¹ ∈ E.fixingSubgroup
rw [IntermediateField.mem_fixingSubgroup_iff]
intro x hx
change σ (g (σ⁻¹ x)) = x
have h_in_F : σ⁻¹ x ∈ F := ⟨x, hx, by dsimp; rw [← AlgEquiv.invFun_eq_symm]; rfl⟩
have h_g_fix : g (σ⁻¹ x) = σ⁻¹ x :=
by
rw [Subgroup.mem_carrier, IntermediateField.mem_fixingSubgroup_iff F g] at hg
exact hg (σ⁻¹ x) h_in_F
rw [h_g_fix]
change σ (σ⁻¹ x) = x
exact AlgEquiv.apply_symm_apply σ x
