Theorems · Definition · commutative algebra

IsLocalization.liftAlgHom

{A : Type u_4} →
  [inst : CommSemiring A] →
    {R : Type u_5} →
      [inst_1 : CommSemiring R] →
        [inst_2 : Algebra A R] →
          {M : Submonoid R} →
            {S : Type u_6} →
              [inst_3 : CommSemiring S] →
                [inst_4 : Algebra A S] →
                  [inst_5 : Algebra R S] →
                    [IsScalarTower A R S] →
                      {P : Type u_7} →
                        [inst_7 : CommSemiring P] →
                          [inst_8 : Algebra A P] →
                            [IsLocalization M S] → {f : R →ₐ[A] P} → (∀ (y : ↥M), IsUnit (f ↑y)) → S →ₐ[A] P

AlgHom version of IsLocalization.lift.

Defined in

Mathlib.RingTheory.Localization.Basic

Cited by

11 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiringAlgebraCommSemiringAlgebraAlgebraIsScalarTowerCommSemiringAlgebraIsLocalization