English
For any category C, κ, the property HasCardinalLT (Arrow(Cᵒᵖ)) κ is equivalent to HasCardinalLT (Arrow(C)) κ; the opposite category does not change the cardinal-lt property of the arrow category.
Русский
Для любой категории C и кардинала κ тождество HasCardinalLT (Arrow(Cᵒᵖ)) κ ⇔ HasCardinalLT (Arrow(C)) κ: свойство кардинального LT стрелочного категориального класса сохраняется при переходе к противоположной категории.
LaTeX
$$$\\\\operatorname{HasCardinalLT}(\\\\operatorname{Arrow}(C^{op}),\\\\kappa) \\\\iff \\\\operatorname{HasCardinalLT}(\\\\operatorname{Arrow}(C),\\\\kappa)$$$
Lean4
theorem finite_iff (C : Type u) [SmallCategory C] : Finite (Arrow C) ↔ Nonempty (FinCategory C) :=
by
constructor
· intro
refine ⟨?_, fun a b ↦ ?_⟩
· have := Finite.of_injective (fun (a : C) ↦ Arrow.mk (𝟙 a)) (fun _ _ ↦ congr_arg Comma.left)
apply Fintype.ofFinite
· have :=
Finite.of_injective (fun (f : a ⟶ b) ↦ Arrow.mk f)
(fun f g h ↦ by
change (Arrow.mk f).hom = (Arrow.mk g).hom
congr)
apply Fintype.ofFinite
· rintro ⟨_⟩
have := Fintype.ofEquiv _ (Arrow.equivSigma C).symm
infer_instance
