liftₐ_comp — Mathlib

English

In the general two-sided ideal context with a target K, the two-step lift and mk maps compose to the single mk map for the transitive inclusion hIJ.trans hJK.

Русский

В общем случае двухсторонних идеалов композиция liftₐ и mkₐ эквивалентна mkₐ для перехода по включению hIJ.trans hJK.

LaTeX

$$$(Ideal.Quotient.liftₐ I f hI).comp (Ideal.Quotient.mkₐ R₁ I) = f$$$

Lean4

theorem liftₐ_comp (I : Ideal A) [I.IsTwoSided] (f : A →ₐ[R₁] B) (hI : ∀ a : A, a ∈ I → f a = 0) :
    (Ideal.Quotient.liftₐ I f hI).comp (Ideal.Quotient.mkₐ R₁ I) = f :=
  AlgHom.ext fun _ => (Ideal.Quotient.lift_mk I (f : A →+* B) hI :)

Похожие утверждения