English
Let F: J → AlgCat(R) be a diagram of R-algebras. There exists a limit cone Lim(F) in AlgCat(R) together with, for every j ∈ J, a canonical R-algebra homomorphism from Lim(F) to F(j) arising from the limit of the underlying types; these π_j form the projections of the limit cone.
Русский
Пусть F: J → AlgCat(R) задаёт диаграмму R-алгебр. Существует предел ako Lim(F) в AlgCat(R) и, для каждого j ∈ J, канонический гомоморфизм R-алгебр π_j: Lim(F) → F(j), являющийся проекцией предела на компоненту j.
LaTeX
$$$$\exists A\,\{\pi_j: A \to F(j)\}_{j \in J},\quad (A, \pi_j) \text{ есть предел над F}.$$$$
Lean4
/-- `limit.π (F ⋙ forget (AlgCat R)) j` as a `AlgHom`. -/
def limitπAlgHom (j) : (Types.Small.limitCone (F ⋙ forget (AlgCat R))).pt →ₐ[R] (F ⋙ forget (AlgCat.{w} R)).obj j :=
letI : Small.{w} (Functor.sections ((F ⋙ forget₂ _ RingCat ⋙ forget₂ _ SemiRingCat) ⋙ forget _)) :=
inferInstanceAs <| Small.{w} (F ⋙ forget _).sections
{
SemiRingCat.limitπRingHom (F ⋙ forget₂ (AlgCat R) RingCat.{w} ⋙ forget₂ RingCat SemiRingCat.{w})
j with
toFun := (Types.Small.limitCone (F ⋙ forget (AlgCat.{w} R))).π.app j
commutes' := fun x =>
by
simp only [Types.Small.limitCone_π_app, ← Shrink.algEquiv_apply R, Types.Small.limitCone_pt, AlgEquiv.commutes]
rfl }
