succEquiv — Mathlib

English

There is a canonical equivalence between embeddings at i and the product of embeddings at i and a fresh coordinate X_i.

Русский

Существует каноническое эквивалентное отображение между вложениями на шаге i и их произведением с новой координатой X_i.

LaTeX

$$$$\\text{succEquiv}_i : (E⟮

Lean4

/-- Each embedding of `E⟮<i⟯` into `Ē` extend to `#(X i)` embeddings of `E⟮<i⁺⟯`. -/
def succEquiv (i : ι) : (E⟮<i⁺⟯ →ₐ[F] Ē) ≃ (E⟮<i⟯ →ₐ[F] Ē) × X i :=
  (((show _ ≃ₐ[F] E⟮<i⟯⟮b (φ i)⟯ from equivOfEq (filtration_succ i))).arrowCongr .refl).trans <|
    algHomEquivSigma (B := E⟮<i⟯).trans <|
      .sigmaEquivProdOfEquiv fun _ ↦
        (@Field.embEquivOfIsAlgClosed _ _ _ _ _ _ _ (_) <|
            (Algebra.IsAlgebraic.tower_top (K := F) _).of_injective (val _) Subtype.val_injective).symm

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