Theorems · Definition · field theory

Field.Emb.Cardinal.equivLim

{F : Type u} →
  {E : Type v} →
    [inst : Field F] →
      [inst_1 : Field E] →
        [inst_2 : Algebra F E] →
          [rank_inf : Fact (Cardinal.aleph0 ≤ Module.rank F E)] →
            [inst_3 : Algebra.IsAlgebraic F E] →
              {i : WithTop (Module.rank F E).ord.ToType} →
                Order.IsSuccPrelimit i →
                  (↥(Field.Emb.Cardinal.filtration i) →ₐ[F] AlgebraicClosure E) ≃
                    ↑(InverseSystem.limit (Field.Emb.Cardinal.embFunctor F E) i)

If i is a limit, the type of embeddings of E⟮<i⟯ into Ē is the limit of the types of embeddings of E⟮<j⟯ for j < i.

Defined in

Mathlib.FieldTheory.CardinalEmb

Cited by

1 results in Mathlib

Foundations

Depth 180 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldFieldAlgebraFactAlgebra.IsAlgebraic