mulEquivAlgEquiv — Mathlib

English

There exists a multiplicative isomorphism between the Galois group G and the automorphism group Aut_K(L).

Русский

Существует мультипликативное изоморфизм между Галуа-группой G и Aut_K(L).

LaTeX

$$G \\cong_* (L \\simeq_K L)$$

Lean4

/-- If `G` is a finite Galois group for `L/K`, then `G` is isomorphic to `L ≃ₐ[K] L`. -/
@[simps!]
noncomputable def mulEquivAlgEquiv [IsGaloisGroup G K L] [Finite G] : G ≃* (L ≃ₐ[K] L) :=
  MulEquiv.ofBijective (MulSemiringAction.toAlgAut G K L)
    (by
      have := isGalois G K L
      have := finiteDimensional G K L
      rw [Nat.bijective_iff_injective_and_card, card_eq_finrank G K L, IsGalois.card_aut_eq_finrank K L]
      exact ⟨fun _ _ ↦ (faithful K).eq_of_smul_eq_smul ∘ DFunLike.ext_iff.mp, rfl⟩)

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