toLoc — Mathlib

English

The 1-morphism in LocallyDiscrete C induced by a morphism f: a ⟶ b in C is the LocallyDiscrete object morphism ⟨f⟩.

Русский

Линейный 1-морфизм в LocallyDiscrete C, порождённый морфизмом f: a ⟶ b, равен ⟨f⟩.

LaTeX

$$$ toLoc(f) = \\langle f \\rangle $$$

Lean4

/-- The 1-morphism in `LocallyDiscrete C` associated to a given morphism `f : a ⟶ b` in `C` -/
@[simps]
def toLoc {a b : C} (f : a ⟶ b) : LocallyDiscrete.mk a ⟶ LocallyDiscrete.mk b :=
  ⟨f⟩

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