lift_apply_inl — Mathlib

English

Two AlgHoms are equal if their values on inl and inr parts agree suitably.

Русский

Два алгебра-гомоморфизма равны, если они согласованы на частях inl и inr.

LaTeX

$$$ \\text{ext'} (f,g) \\,=\\, \\text{equality condition on inl and inr maps}$$$

Lean4

@[simp]
theorem lift_apply_inl (f : R →ₐ[S] A) (g : M →ₗ[S] A) (hg : ∀ x y, g x * g y = 0) (hfg : ∀ r x, g (r •> x) = f r * g x)
    (hgf : ∀ r x, g (x <• r) = g x * f r) (r : R) : lift f g hg hfg hgf (inl r) = f r :=
  show f r + g 0 = f r by rw [map_zero, add_zero]

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