restrictNormalHom_continuous — Mathlib

English

There exists x ∈ L such that the orbit { σ(x) } is K-linearly independent, giving a normal basis.

Русский

Существует x ∈ L, орбита { σ(x) } образует линейно независимый набор над K, образуя нормальный базис.

LaTeX

$$$\\exists x \\in L:\\; LinearIndependent_K(\\,\\sigma x\\,|\\sigma \\in Aut_K(L)\\,)$$$

Lean4

theorem restrictNormalHom_continuous (L : IntermediateField k K) [Normal k L] :
    Continuous (AlgEquiv.restrictNormalHom (F := k) (K₁ := K) L) :=
  by
  apply continuous_of_continuousAt_one _ (continuousAt_def.mpr _)
  intro N hN
  rw [map_one, krullTopology_mem_nhds_one_iff] at hN
  obtain ⟨L', _, hO⟩ := hN
  have := Module.Finite.equiv <| AlgEquiv.toLinearEquiv <| IntermediateField.liftAlgEquiv L'
  apply mem_nhds_iff.mpr
  use (IntermediateField.lift L').fixingSubgroup
  constructor
  · intro x hx
    apply hO
    simp only [SetLike.mem_coe, IntermediateField.mem_fixingSubgroup_iff] at hx ⊢
    intro y hy
    have := AlgEquiv.restrictNormal_commutes x L y
    dsimp at this
    rw [hx y.1 ((IntermediateField.mem_lift y).mpr hy)] at this
    exact SetLike.coe_eq_coe.mp this
  · exact ⟨IntermediateField.fixingSubgroup_isOpen (IntermediateField.lift L'), congrFun rfl⟩

Похожие утверждения