isAmalgamation_map_localPreimage — Mathlib

English

For a map φ: R → R' of presieves FamilyOfElements, the localPreimage map φ induces an amalgamation over r' ∈ R'.obj(X).

Русский

Для отображения φ: R → R' в семье элементов, локальный предобраз φ индуцирует амальгамацию на r' ∈ R'.obj(X).

LaTeX

$$$((\mathrm{localPreimage}\ \phi\ r').map\ \phi).IsAmalgamation\ r'$$$

Lean4

theorem isAmalgamation_map_localPreimage : ((localPreimage φ r').map φ).IsAmalgamation r' := fun _ f hf =>
  (Presheaf.app_localPreimage φ r' f hf).symm

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