Theorems · Definition · commutative algebra

PowerBasis.lift

{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) → (y : S') → (Polynomial.aeval y) (minpoly A pb.gen) = 0 → S →ₐ[A] S'

pb.lift y hy is the algebra map sending pb.gen to y, where hy states the higher powers of y are the same as the higher powers of pb.gen. See PowerBasis.liftEquiv for a bundled equiv sending ⟨y, hy⟩ to the algebra map.

Defined in

Mathlib.RingTheory.PowerBasis

Cited by

9 results in Mathlib

Foundations

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

Assumes

RingCommRingAlgebraRingAlgebra