lift_comp_kernelIsoOfEq_inv — Mathlib

English

If h is the equality f ≡ g, then lifting along f and composing with the inverse of kernelIsoOfEq h equals lifting along g with a modified equality.

Русский

Если h задаёт равенство f ≡ g, то лифт по f и композиция с инверсией kernelIsoOfEq h равны лифт по g с изменённым равенством.

LaTeX

$$$\\forall Z\\; f,g: X\\to Y\\; (h: f=g)\\; (e: Z\\to X) (he)\\;\\text{: }\\operatorname{kernel.lift} f e he \\circ (\\operatorname{kernelIsoOfEq} h)^{-1} = \\operatorname{kernel.lift} g e (by \\text{simp}[\\!\\,h, e])$$$

Lean4

@[reassoc (attr := simp)]
theorem lift_comp_kernelIsoOfEq_inv {Z} {f g : X ⟶ Y} [HasKernel f] [HasKernel g] (h : f = g) (e : Z ⟶ X) (he) :
    kernel.lift _ e he ≫ (kernelIsoOfEq h).inv = kernel.lift _ e (by simp [h, he]) := by cases h; simp

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