mem_functorPushforward_iff_of_full_of_faithful

English

If F is full and faithful, then for R: Sieve X and f: Y → X, (R.arrows.functorPushforward F)(F.map f) is equivalent to R f.

Русский

Пусть F полностью полноформиран и инъективен; тогда для R и f выполняется эквивалентность: (R.arrows.functorPushforward F)(F.map f) ⇔ R f.

LaTeX

$$$ (R.arrows.functorPushforward F)(F.map f) \iff R f $$$

Lean4

theorem mem_functorPushforward_iff_of_full_of_faithful [F.Full] [F.Faithful] {X Y : C} (R : Sieve X) (f : Y ⟶ X) :
    (R.arrows.functorPushforward F) (F.map f) ↔ R f :=
  by
  rw [Sieve.mem_functorPushforward_iff_of_full]
  refine ⟨fun ⟨g, hcomp, hg⟩ ↦ ?_, fun hf ↦ ⟨f, rfl, hf⟩⟩
  rwa [← F.map_injective hcomp]

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