English
There is a universal equivalence between the data of a pair (f,g) with zero-product and compatibility conditions and algebra homomorphisms from the trivial square-zero extension to A; this equivalence respects the endpoints via the left and right projections given by lift.
Русский
Существует универсальное эквивалентное отображение между данными пары (f,g), удовлетворяющей условиям нулевой продукции и совместимости, и алгебра-гомоморфизмами из тривиального квадратно-нульевого расширения в A; эквивелентность сохраняет заданные проекции слева и справа, задаваемые через lift.
LaTeX
$$$\\text{liftEquiv} : \\{ fg : (R \\to_A[S] A) \\times (M \\to_l[S] A) \\mid \\dots \\} \\simeq (tsze\\ R\\ M \\to_A[S] A)$$$
Lean4
/-- A universal property of the trivial square-zero extension, providing a unique
`TrivSqZeroExt R M →ₐ[R] A` for every pair of maps `f : R →ₐ[S] A` and `g : M →ₗ[S] A`,
where the range of `g` has no non-zero products, and scaling the input to `g` on the left or right
amounts to a corresponding multiplication by `f` in the output.
This isomorphism is named to match the very similar `Complex.lift`. -/
@[simps! apply symm_apply_coe]
def liftEquiv :
{ fg : (R →ₐ[S] A) × (M →ₗ[S] A) //
(∀ x y, fg.2 x * fg.2 y = 0) ∧
(∀ r x, fg.2 (r •> x) = fg.1 r * fg.2 x) ∧ (∀ r x, fg.2 (x <• r) = fg.2 x * fg.1 r) } ≃
(tsze R M →ₐ[S] A)
where
toFun fg := lift fg.val.1 fg.val.2 fg.prop.1 fg.prop.2.1 fg.prop.2.2
invFun
F :=
⟨(F.comp (inlAlgHom _ _ _), F.toLinearMap ∘ₗ (inrHom _ _ |>.restrictScalars _)),
(fun _x _y => (map_mul F _ _).symm.trans <| (F.congr_arg <| inr_mul_inr _ _ _).trans (map_zero F)),
(fun _r _x => (F.congr_arg (inl_mul_inr _ _).symm).trans (map_mul F _ _)),
(fun _r _x => (F.congr_arg (inr_mul_inl _ _).symm).trans (map_mul F _ _))⟩
left_inv _f := Subtype.ext <| Prod.ext (lift_comp_inlHom _ _ _ _ _) (lift_comp_inrHom _ _ _ _ _)
right_inv _F := algHom_ext' (lift_comp_inlHom _ _ _ _ _) (lift_comp_inrHom _ _ _ _ _)
