Theorems · Definition · commutative algebra

PowerBasis.liftEquiv

{S : Type u_2} →
  [inst : Ring S] →
    {A : Type u_4} →
      [inst_1 : CommRing A] →
        [inst_2 : Algebra A S] →
          {S' : Type u_7} →
            [inst_3 : Ring S'] →
              [inst_4 : Algebra A S'] →
                (pb : PowerBasis A S) → (S →ₐ[A] S') ≃ { y // (Polynomial.aeval y) (minpoly A pb.gen) = 0 }

pb.liftEquiv states that roots of the minimal polynomial of pb.gen correspond to maps sending pb.gen to that root. This is the bundled equiv version of PowerBasis.lift. If the codomain of the AlgHoms is an integral domain, then the roots form a multiset, see liftEquiv' for the corresponding statement.

Defined in

Mathlib.RingTheory.PowerBasis

Cited by

3 results in Mathlib

Foundations

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

Assumes

RingCommRingAlgebraRingAlgebra