English
For any F, RepresentablyFlat F.op iff RepresentablyCoflat F.
Русский
Для любого F, RepresentablyFlat F.op эквивалентно RepresentablyCoflat F.
LaTeX
$$$$ \\mathrm{RepresentablyFlat}(F^{\\mathrm{op}}) \\iff \\mathrm{RepresentablyCoflat}(F). $$$$
Lean4
theorem representablyFlat_op_iff : RepresentablyFlat F.op ↔ RepresentablyCoflat F :=
by
refine ⟨fun _ => ⟨fun X => ?_⟩, fun _ => ⟨fun ⟨X⟩ => ?_⟩⟩
· suffices IsCofiltered (CostructuredArrow F X)ᵒᵖ from isFiltered_of_isCofiltered_op _
apply IsCofiltered.of_equivalence (costructuredArrowOpEquivalence _ _).symm
· suffices IsFiltered (StructuredArrow (op X) F.op)ᵒᵖ from isCofiltered_of_isFiltered_op _
suffices IsFiltered (CostructuredArrow F X)ᵒᵖᵒᵖ from
IsFiltered.of_equivalence (costructuredArrowOpEquivalence _ _).op
apply IsFiltered.of_equivalence (opOpEquivalence _)
