sectionsEquivHom_naturality — Mathlib

English

For F,G : C ⥤ Type, f : F ⟶ G, X a Type with Unique X, and x ∈ F.sections, the naturality of the equivalence says (G.sectionsEquivHom X)((sectionsFunctor C).map f x) = (F.sectionsEquivHom X) x ≫ f.

Русский

Для F,G : C ⥤ Type, f : F ⟶ G, X с единственным элементом, и x ∈ F.sections, естественная совместимость гласит, что (G.sectionsEquivHom X)((sectionsFunctor C).map f x) = (F.sectionsEquivHom X) x ≫ f.

LaTeX

$$$$ (G.sectionsEquivHom X)\big((sectionsFunctor C).map f\, x\big) = (F.sectionsEquivHom X)\, x \;\gg\; f $$$$

Lean4

theorem sectionsEquivHom_naturality {F G : C ⥤ Type u₂} (f : F ⟶ G) (X : Type u₂) [Unique X] (x : F.sections) :
    (G.sectionsEquivHom X) ((sectionsFunctor C).map f x) = (F.sectionsEquivHom X) x ≫ f := by rfl

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