equalizerFork'IsLimit — Mathlib

English

The equalizer fork for algebra maps f, g is a limit in the Under category; more precisely, equalizerFork' f g is a limit of f and g in CommRingCat.Under.

Русский

Равносилийный форк для гомоморфизмов f, g является пределом в категории Under; то есть Under.equalizerFork' f g является пределом для f и g.

LaTeX

$$$ \\operatorname{IsLimit}( \\operatorname{Under.equalizerFork'}(f,g) )$$$

Lean4

/-- Variant of `Under.equalizerForkIsLimit` for algebra maps. -/
def equalizerFork'IsLimit {A B : Type u} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (f g : A →ₐ[R] B) :
    IsLimit (Under.equalizerFork' f g) :=
  Under.equalizerForkIsLimit f.toUnder g.toUnder

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