comp_liftOfSurjective — Mathlib

English

The composition identity with liftOfSurjective holds: g ∘ liftOfSurjective f g hg hg' = f.

Русский

Сочетание соотношений имеет вид: g ∘ liftOfSurjective f g hg hg' = f.

LaTeX

$$g ∘ (FormallySmooth.liftOfSurjective f g hg hg') = f$$

Lean4

@[simp]
theorem comp_liftOfSurjective [FormallySmooth R A] (f : A →ₐ[R] C) (g : B →ₐ[R] C) (hg : Function.Surjective g)
    (hg' : IsNilpotent <| RingHom.ker (g : B →+* C)) : g.comp (FormallySmooth.liftOfSurjective f g hg hg') = f :=
  AlgHom.ext (FormallySmooth.liftOfSurjective_apply f g hg hg')

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