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