Theorems · Theorem · commutative algebra

IsLocalization.coe_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]
  [inst_6 : IsScalarTower A R S] {P : Type u_7} [inst_7 : CommSemiring P] [inst_8 : Algebra A P]
  [inst_9 : IsLocalization M S] {f : R →ₐ[A] P} (hf : ∀ (y : ↥M), IsUnit (f ↑y)),
  ⇑(IsLocalization.liftAlgHom hf) = ⇑(IsLocalization.lift hf)

Defined in

Mathlib.RingTheory.Localization.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiringAlgebraCommSemiringAlgebraAlgebraIsScalarTowerCommSemiringAlgebraIsLocalization