English
A simplified version of membership characterization for fixingSubgroup; expresses the same equivalence in a streamlined form.
Русский
Упрощённое выражение эквивалентности принадлежности в фиксирующей подгруппе.
LaTeX
$$$ (\text{mem_fixingSubgroup_iff}) \text{(simplified)} $$$
Lean4
theorem fixingSubgroup_isClosed (L : IntermediateField k K) [IsGalois k K] :
IsClosed (L.fixingSubgroup : Set (K ≃ₐ[k] K)) where
isOpen_compl :=
isOpen_iff_mem_nhds.mpr fun σ h => by
apply mem_nhds_iff.mpr
rcases Set.not_subset.mp ((mem_fixingSubgroup_iff (K ≃ₐ[k] K)).not.mp h) with ⟨y, yL, ne⟩
use σ • ((adjoin k { y }).1.fixingSubgroup : Set (K ≃ₐ[k] K))
constructor
· intro f hf
rcases (Set.mem_smul_set.mp hf) with ⟨g, hg, eq⟩
simp only [Set.mem_compl_iff, SetLike.mem_coe, ← eq]
apply (mem_fixingSubgroup_iff (K ≃ₐ[k] K)).not.mpr
push_neg
use y
simp only [yL, smul_eq_mul, AlgEquiv.smul_def, AlgEquiv.mul_apply, ne_eq, true_and]
have : g y = y := (mem_fixingSubgroup_iff (K ≃ₐ[k] K)).mp hg y <| adjoin_simple_le_iff.mp le_rfl
simpa only [this, ne_eq, AlgEquiv.smul_def] using ne
· simp only [(IntermediateField.fixingSubgroup_isOpen (adjoin k { y }).1).smul σ, true_and]
use 1
simp only [SetLike.mem_coe, smul_eq_mul, mul_one, and_true, Subgroup.one_mem]
