apply_map — Mathlib

English

Under a compatible-preserving structure, pushing forward a compatible family along G preserves its compatibility identity for pushforward maps.

Русский

При совместимом сохранении структура передвижения семейства сохраняет совместимость через отображение.

LaTeX

$$$x.functorPushforward G (G.map f) (image_mem_functorPushforward G T hf) = x f hf$$$

Lean4

@[simp]
theorem apply_map {Y : C} {f : Y ⟶ Z} (hf : T f) :
    x.functorPushforward G (G.map f) (image_mem_functorPushforward G T hf) = x f hf :=
  by
  unfold FamilyOfElements.functorPushforward
  rcases getFunctorPushforwardStructure (image_mem_functorPushforward G T hf) with ⟨X, g, f', hg, eq⟩
  simpa using hG.compatible ℱ h f' (𝟙 _) hg hf (by simp [eq])

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