mkUnder — Mathlib

English

From an R-algebra A, one obtains an object of Under R whose right component is A with the structure map given by the algebra map R → A.

Русский

Из R-алгебры A образуется объект в Under R, чья правая часть равна A и структура задается через алгебраическую карту R → A.

LaTeX

$$$\mathrm{mkUnder}(R,A) \in \mathrm{Under}(R), \quad \text{with right } A \text{ and } \text{structure map } R \to A$$$

Lean4

/-- Make an object of `Under R` from an `R`-algebra. -/
@[simps! hom, simps! -isSimp right]
def mkUnder (A : Type u) [CommRing A] [Algebra R A] : Under R :=
  Under.mk (CommRingCat.ofHom <| algebraMap R A)

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