English
Given f1, f2: A →ₐ[R] B that lift the same map A → B/I, there is a canonical R-linear map from A into I capturing their difference, defined by x ↦ f1(x) − f2(x).
Русский
Пусть f1, f2: A →ₐ[R] B — две аппроксимации, которые поднимают один и тот же гомоморфизм A → B/I; существует единственный R-линейный отображение A → I, задаваемый x ↦ f1(x) − f2(x).
LaTeX
$$$\exists\! \text{diffToIdealOfQuotientCompEq } I f1 f2 e : A \to_{\mathrm{L}}[R] I \quad \text{such that } (f1 - f2)(x) \in I$ for all x and the map is R-linear.$$
Lean4
/-- If `f₁ f₂ : A →ₐ[R] B` are two lifts of the same `A →ₐ[R] B ⧸ I`,
we may define a map `f₁ - f₂ : A →ₗ[R] I`. -/
def diffToIdealOfQuotientCompEq (f₁ f₂ : A →ₐ[R] B)
(e : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂) : A →ₗ[R] I :=
LinearMap.codRestrict (I.restrictScalars _) (f₁.toLinearMap - f₂.toLinearMap)
(by
intro x
change f₁ x - f₂ x ∈ I
rw [← Ideal.Quotient.eq, ← Ideal.Quotient.mkₐ_eq_mk R, ← AlgHom.comp_apply, e]
rfl)
