equivOfRoot — Mathlib

English

There is a well-behaved equivalence between power-basis-based algebra homomorphisms when the root relations hold; in particular, lifting respects composition with pb.lift.

Русский

Существуют хорошо ведённые соответствия между алгебраическими гомоморфизмами с базисом мощности, если соблюдены корневые отношения; в частности, перенос через pb.lift сохраняет композицию.

LaTeX

$$pb.equivOfRoot pb' h1 h2 : S ≃_A S' and pb'.lift pb.gen h1 etc.$$

Lean4

/-- `pb.equivOfRoot pb' h₁ h₂` is an equivalence of algebras with the same power basis,
where "the same" means that `pb` is a root of `pb'`s minimal polynomial and vice versa.

See also `PowerBasis.equivOfMinpoly` which takes the hypothesis that the
minimal polynomials are identical.
-/
@[simps! -isSimp apply]
noncomputable def equivOfRoot (pb : PowerBasis A S) (pb' : PowerBasis A S') (h₁ : aeval pb.gen (minpoly A pb'.gen) = 0)
    (h₂ : aeval pb'.gen (minpoly A pb.gen) = 0) : S ≃ₐ[A] S' :=
  AlgEquiv.ofAlgHom (pb.lift pb'.gen h₂) (pb'.lift pb.gen h₁)
    (by
      ext x
      obtain ⟨f, hf, rfl⟩ := pb'.exists_eq_aeval' x
      simp)
    (by
      ext x
      obtain ⟨f, hf, rfl⟩ := pb.exists_eq_aeval' x
      simp)

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