liftAlgHom_mkAlgHom_apply — Mathlib

English

If f : A →ₐ[S] B and g : RingQuot s →ₐ[S] B with h: g ∘ mkAlgHom S s = f, then g = LiftAlgHom ⟨f,w⟩.

Русский

Если f : A →ₐ[S] B и g : RingQuot s →ₐ[S] B при условии h: g ∘ mkAlgHom S s = f, то g = LiftAlgHom ⟨f,w⟩.

LaTeX

$$$\\forall f:\\, A \\to_{S} B\\;{s}\\; (w:\\forall x y, s x y → f x = f y)\\; (g:\\ RingQuot s \\to_{S} B),\\ g \\circ (mkAlgHom S s) = f \\Rightarrow g = LiftAlgHom S ⟨f,w⟩$$$

Lean4

@[simp]
theorem liftAlgHom_mkAlgHom_apply (f : A →ₐ[S] B) {s : A → A → Prop} (w : ∀ ⦃x y⦄, s x y → f x = f y) (x) :
    (liftAlgHom S ⟨f, w⟩) ((mkAlgHom S s) x) = f x :=
  by
  simp_rw [liftAlgHom_def, preLiftAlgHom_def, mkAlgHom_def, mkRingHom_def]
  rfl
    -- note this is essentially `(liftAlgHom S).symm_apply_eq.mp h`

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