Theorems · Definition · field theory

RatFunc.liftAlgHom

{K : Type u} →
  [inst : CommRing K] →
    [inst_1 : IsDomain K] →
      {L : Type u_1} →
        {S : Type u_3} →
          [inst_2 : Field L] →
            [inst_3 : CommSemiring S] →
              [inst_4 : Algebra S (Polynomial K)] →
                [inst_5 : Algebra S L] →
                  (φ : Polynomial K →ₐ[S] L) →
                    nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors L) → RatFunc K →ₐ[S] L

Lift an injective algebra homomorphism K[X] →ₐ[S] L to a K⟮X⟯ →ₐ[S] L by mapping both the numerator and denominator and quotienting them.

Defined in

Mathlib.FieldTheory.RatFunc.Basic

Cited by

7 results in Mathlib

Foundations

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

Assumes

CommRingIsDomainFieldCommSemiringAlgebraAlgebra