toAlgAut_surjective — Mathlib

English

The map toAlgAut G (FixedPoints.subfield G F) F is surjective for finite G; every algebra automorphism fixing FixedPoints.subfield arises from some g ∈ G.

Русский

Отображение toAlgAut превышает всю область; каждый алгебраический аутоморфизм, фиксирующий FixedPoints.subfield, соответствует некоторому g ∈ G.

LaTeX

$$$\\text{toAlgAut_surjective } G F : \\text{Surjective}(\\operatorname{MulSemiringAction.toAlgAut } G (\\operatorname{FixedPoints.subfield } G F) F)$$$

Lean4

/-- `MulSemiringAction.toAlgAut` is surjective. -/
theorem toAlgAut_surjective [Finite G] :
    Function.Surjective (MulSemiringAction.toAlgAut G (FixedPoints.subfield G F) F) :=
  by
  let f : G →* F ≃ₐ[FixedPoints.subfield G F] F := MulSemiringAction.toAlgAut G (FixedPoints.subfield G F) F
  let Q := G ⧸ f.ker
  let _ : MulSemiringAction Q F := MulSemiringAction.compHom _ (QuotientGroup.kerLift f)
  have : FaithfulSMul Q F :=
    ⟨by
      intro q₁ q₂
      refine Quotient.inductionOn₂' q₁ q₂ (fun g₁ g₂ h ↦ QuotientGroup.eq.mpr ?_)
      rwa [MonoidHom.mem_ker, map_mul, map_inv, inv_mul_eq_one, AlgEquiv.ext_iff]⟩
  intro f
  obtain ⟨q, hq⟩ :=
    (toAlgAut_bijective Q F).surjective (AlgEquiv.ofRingEquiv (f := f) (fun ⟨x, hx⟩ ↦ f.commutes' ⟨x, fun g ↦ hx g⟩))
  revert hq
  refine QuotientGroup.induction_on q (fun g hg ↦ ⟨g, ?_⟩)
  rwa [AlgEquiv.ext_iff] at hg ⊢

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