arrows_generate_map_eq_functorPushforward

English

The pushforward arrows along F coincide with the functorPushforward construction.

Русский

Стрелы переноса вдоль F совпадают с конструкцией functorPushforward.

LaTeX

$$Theorem: arrows_pushforward equality: (S.arrows).pushforward F = S.functorPushforward F$$

Lean4

theorem arrows_generate_map_eq_functorPushforward {s : Presieve X} :
    (generate (s.map F)).arrows = s.functorPushforward F :=
  by
  refine funext fun Z ↦ Set.ext fun u ↦ ⟨?_, ?_⟩
  · rintro ⟨_, _, _, ⟨hu⟩, rfl⟩; exact ⟨_, _, _, hu, rfl⟩
  · rintro ⟨_, _, _, hu, rfl⟩; exact ⟨_, _, _, ⟨hu⟩, rfl⟩

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