nonempty_algEquiv_or_of_finrank_eq_two

English

If k is a field and K is an algebraic extension, IsAlgClosed k implies L = ⊥ for L an algebraic intermediate field of k ⊆ K.

Русский

Если k — поле, K — алгебраическое расширение, и IsAlgClosed k, то для любой алгебраически-расширяемой подполя L внутри K выполняется L = ⊥.

LaTeX

$$$L = \bot$$$

Lean4

theorem nonempty_algEquiv_or_of_finrank_eq_two {F F' : Type*} (E : Type*) [Field F] [Field F'] [Field E] [Algebra F F']
    [Algebra F E] [Algebra.IsAlgebraic F E] [IsAlgClosed F'] (h : Module.finrank F F' = 2) :
    Nonempty (E ≃ₐ[F] F) ∨ Nonempty (E ≃ₐ[F] F') :=
  by
  have emb : E →ₐ[F] F' := lift
  have e := AlgEquiv.ofInjectiveField emb
  have := Subalgebra.isSimpleOrder_of_finrank h
  obtain h | h := IsSimpleOrder.eq_bot_or_eq_top emb.range <;> rw [h] at e
  exacts [.inl ⟨e.trans <| Algebra.botEquiv ..⟩, .inr ⟨e.trans Subalgebra.topEquiv⟩]

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