English
The evaluation of liftₐ at an element x coincides with the evaluation of lifting via ring homomorphism, i.e., liftₐ I f hI x = lift I (f) hI x.
Русский
Значение liftₐ на элементе x совпадает с значением lift через кольцевой гомоморфизм.
LaTeX
$$$\\text{lift}ₐ(I,f,hI)(x) = \\text{lift}(f,hI)(x)$$$
Lean4
/-- `Ideal.quotient.lift` as an `AlgHom`. -/
def liftₐ (I : Ideal A) [I.IsTwoSided] (f : A →ₐ[R₁] B) (hI : ∀ a : A, a ∈ I → f a = 0) : A ⧸ I →ₐ[R₁] B :=
{ -- this is IsScalarTower.algebraMap_apply R₁ A (A ⧸ I) but the file `Algebra.Algebra.Tower`
-- imports this file.
Ideal.Quotient.lift I (f : A →+* B) hI with
commutes' := fun r =>
by
have : algebraMap R₁ (A ⧸ I) r = Ideal.Quotient.mk I (algebraMap R₁ A r) := rfl
rw [this, RingHom.toFun_eq_coe, Ideal.Quotient.lift_mk, AlgHom.coe_toRingHom, Algebra.algebraMap_eq_smul_one,
Algebra.algebraMap_eq_smul_one, map_smul, map_one] }
