English
Siftedness is preserved by equivalences: if C is sifted and D ≃ C, then D is sifted.
Русский
Ситообразность сохраняется при эквивалентности: если C ситообразна, а D эквивалентна C, то D тоже ситообразна.
LaTeX
$$IsSifted(D) if e: D ≃ C and IsSifted(C)$$
Lean4
/-- Being sifted is preserved by equivalences of categories -/
theorem isSifted_of_equiv [IsSifted C] {D : Type u₁} [Category.{v₁} D] (e : D ≌ C) : IsSifted D :=
letI : Final (diag D) := by
letI : D × D ≌ C × C := Equivalence.prod e e
have sq : (e.inverse ⋙ diag D ⋙ this.functor ≅ diag C) :=
NatIso.ofComponents
(fun c ↦ by
dsimp [this]
exact Iso.prod (e.counitIso.app c) (e.counitIso.app c))
apply_rules [final_iff_comp_equivalence _ this.functor |>.mpr, final_iff_final_comp e.inverse _ |>.mpr,
final_of_natIso sq.symm]
letI : _root_.Nonempty D := ⟨e.inverse.obj (_root_.Nonempty.some IsSifted.nonempty)⟩
⟨⟩
