liftOfSurjective — Mathlib

English

The symmetry lemma expresses that composing the equivalence with the original map recovers the original g.

Русский

Лемма симметрии показывает, что композиция обратной связи восстанавливает исходный g.

LaTeX

$$$$ \\text{(symm_apply)}(f.liftOfRightInverse) = g. $$$$

Lean4

/-- A non-computable version of `RingHom.liftOfRightInverse` for when no computable right
inverse is available, that uses `Function.surjInv`. -/
@[simp]
noncomputable abbrev liftOfSurjective (hf : Function.Surjective f) :
    { g : A →+* C // RingHom.ker f ≤ RingHom.ker g } ≃ (B →+* C) :=
  f.liftOfRightInverse (Function.surjInv hf) (Function.rightInverse_surjInv hf)

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