lift_gen — Mathlib

English

There is a natural equivalence between A-algebra homomorphisms S →_A B and roots y in B of the minimal polynomial of pb.gen; the equivalence sends f to f(pb.gen).

Русский

Существует естественное эквивалентное отображение между алгебраическими гомоморфизмами S →_A B и корнями y в B минимального полинома pb.gen; отображение отправляет f в f(pb.gen).

LaTeX

$$@(pb := PowerBasis A S) \text{liftEquiv} : (S \to_A B) ≃ { y : B // y ∈ (minpoly A pb.gen).aroots B }$$

Lean4

@[simp]
theorem lift_gen (pb : PowerBasis A S) (y : S') (hy : aeval y (minpoly A pb.gen) = 0) : pb.lift y hy pb.gen = y :=
  pb.constr_pow_gen hy

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