English
For a closed subgroup H, the fixedField of H equals the fixedField of its associated subgroup; i.e., H’s fixed field equals the fixed field of the corresponding subgroup.
Русский
Для замкнутой подгруппы H фиксированное поле H равно фиксированному полю соответствующей подгруппы.
LaTeX
$$$ (H).fixedField = H.1 $$$
Lean4
theorem fixingSubgroup_fixedField (H : ClosedSubgroup (K ≃ₐ[k] K)) [IsGalois k K] :
(IntermediateField.fixedField H).fixingSubgroup = H.1 :=
by
apply le_antisymm _ ((IntermediateField.le_iff_le H.toSubgroup (IntermediateField.fixedField H.toSubgroup)).mp le_rfl)
intro σ hσ
by_contra h
have nhds : H.carrierᶜ ∈ nhds σ := H.isClosed'.isOpen_compl.mem_nhds h
rw [GroupFilterBasis.nhds_eq (x₀ := σ) (galGroupBasis k K)] at nhds
rcases nhds with ⟨b, ⟨gp, ⟨L, hL, eq'⟩, eq⟩, sub⟩
rw [← eq'] at eq
have := hL.out
let L' : FiniteGaloisIntermediateField k K :=
{ normalClosure k L K with
finiteDimensional := normalClosure.is_finiteDimensional k L K
isGalois := IsGalois.normalClosure k L K }
have compl : σ • L'.1.fixingSubgroup.carrier ⊆ H.carrierᶜ :=
by
rintro φ ⟨τ, hτ, muleq⟩
have sub' : σ • b ⊆ H.carrierᶜ := Set.smul_set_subset_iff.mpr sub
apply sub'
simp only [← muleq, ← eq]
apply Set.smul_mem_smul_set
exact (L.fixingSubgroup_le (IntermediateField.le_normalClosure L) hτ)
have fix : ∀ x ∈ IntermediateField.fixedField H.toSubgroup ⊓ ↑L', σ x = x := fun x hx ↦
((mem_fixingSubgroup_iff (K ≃ₐ[k] K)).mp hσ) x hx.1
rw [restrict_fixedField H.1 L'.1] at fix
have : (restrictNormalHom L') σ ∈ (Subgroup.map (restrictNormalHom L') H.1) :=
by
rw [← IntermediateField.fixingSubgroup_fixedField (Subgroup.map (restrictNormalHom L') H.1)]
apply (mem_fixingSubgroup_iff (L' ≃ₐ[k] L')).mpr
intro y hy
apply Subtype.val_injective
simp only [AlgEquiv.smul_def, restrictNormalHom_apply L'.1 σ y, fix y.1 ((IntermediateField.mem_lift y).mpr hy)]
rcases this with ⟨h, mem, eq⟩
have : h ∈ σ • L'.1.fixingSubgroup.carrier := by
use σ⁻¹ * h
simp only [Subsemigroup.mem_carrier, Submonoid.mem_toSubsemigroup, Subgroup.mem_toSubmonoid, smul_eq_mul,
mul_inv_cancel_left, and_true]
apply (mem_fixingSubgroup_iff (K ≃ₐ[k] K)).mpr
intro y hy
simp only [AlgEquiv.smul_def, AlgEquiv.mul_apply]
have : ((restrictNormalHom L') h ⟨y, hy⟩).1 = ((restrictNormalHom L') σ ⟨y, hy⟩).1 := by rw [eq]
rw [restrictNormalHom_apply L'.1 h ⟨y, hy⟩, restrictNormalHom_apply L'.1 σ ⟨y, hy⟩] at this
simp only [this, ← AlgEquiv.mul_apply, inv_mul_cancel, one_apply]
absurd compl
apply Set.not_subset.mpr
use h
simpa only [this, Set.mem_compl_iff, Subsemigroup.mem_carrier, Submonoid.mem_toSubsemigroup, Subgroup.mem_toSubmonoid,
not_not, true_and] using mem
