nonempty_algEquiv_adjoin_of_isSepClosed

English

If L/K is S-cyclotomic and M is a sep-closed field with a K-algebra structure, there exists a K-algebra isomorphism from L to the subalgebra generated by the S-root-of-unity elements in M.

Русский

Если L/K циклотомическое по S, и M — sep-closed поле с структурой K-алгебры, существует K-алгебраическое изоморфизм L к подалгебре, порождаемой корнями unity из M с экспонентами из S.

LaTeX

$$$\\exists \\varphi: L \\cong_K \\operatorname{adjoin}_K\\{ x \\in M \\mid \\exists n \\in S, n \\neq 0 \\land x^n = 1 \\}$$$

Lean4

theorem nonempty_algEquiv_adjoin_of_isSepClosed [IsCyclotomicExtension S K L] (M : Type*) [Field M] [Algebra K M]
    [IsSepClosed M] : Nonempty (L ≃ₐ[K] IntermediateField.adjoin K {x : M | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}) :=
  by
  have := isSeparable S K L
  let i : L →ₐ[K] M := IsSepClosed.lift
  refine
    ⟨(show L ≃ₐ[K] i.fieldRange from AlgEquiv.ofInjectiveField i).trans
        (IntermediateField.equivOfEq (le_antisymm ?_ ?_))⟩
  · rintro x (hx : x ∈ i.range)
    let e :=
      Subalgebra.equivOfEq _ _ ((IsCyclotomicExtension.iff_adjoin_eq_top S K L).1 ‹_›).2 |>.trans Subalgebra.topEquiv
    have hrange : i.range = (i.comp (AlgHomClass.toAlgHom e)).range :=
      by
      ext x
      simp only [AlgHom.mem_range, AlgHom.coe_comp, AlgHom.coe_coe, Function.comp_apply]
      constructor
      · rintro ⟨y, rfl⟩; exact ⟨e.symm y, by simp⟩
      · rintro ⟨y, rfl⟩; exact ⟨e y, rfl⟩
    rw [hrange, AlgHom.mem_range] at hx
    obtain ⟨⟨y, hy⟩, rfl⟩ := hx
    induction hy using Algebra.adjoin_induction with
    | mem x hx =>
      obtain ⟨n, hn, h1, h2⟩ := hx
      apply IntermediateField.subset_adjoin
      use n, hn, h1
      rw [← map_pow, ← map_one (i.comp (AlgHomClass.toAlgHom e))]
      congr 1
      apply_fun _ using Subtype.val_injective
      simpa
    | algebraMap x =>
      convert IntermediateField.algebraMap_mem _ x
      exact AlgHom.commutes _ x
    | add x y hx hy ihx ihy =>
      convert add_mem ihx ihy
      exact map_add (i.comp (AlgHomClass.toAlgHom e)) ⟨x, hx⟩ ⟨y, hy⟩
    | mul x y hx hy ihx ihy =>
      convert mul_mem ihx ihy
      exact map_mul (i.comp (AlgHomClass.toAlgHom e)) ⟨x, hx⟩ ⟨y, hy⟩
  · rw [IntermediateField.adjoin_le_iff]
    rintro x ⟨n, hn, h1, h2⟩
    have := NeZero.mk h1
    obtain ⟨y, hy⟩ := exists_isPrimitiveRoot K L hn h1
    obtain ⟨m, -, rfl⟩ := (hy.map_of_injective (f := i) i.injective).eq_pow_of_pow_eq_one h2
    exact ⟨y ^ m, by simp⟩

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