English
Constancy is preserved under equivalence of sheaf categories: the inverse image of F under the equivalence is constant iff F is constant in the target topology.
Русский
Константность сохраняется при эквивалентности категорий касательных: обратное относительно эквивалентности F константно тогда и только тогда, когда F константно в другой топологии.
LaTeX
$$$((\text{sheafEquiv } G J K D).\text{inverse}.\text{obj }F).IsConstant(J) \;\iff\; \mathrm{IsConstant}(K,F)$$$
Lean4
/-- The property of a sheaf of being constant is invariant under equivalence of sheaf
categories.
-/
theorem isConstant_iff_of_equivalence (F : Sheaf K D) :
((sheafEquiv G J K D).inverse.obj F).IsConstant J ↔ IsConstant K F :=
by
constructor
·
exact fun ⟨Y, ⟨i⟩⟩ ↦
⟨_,
⟨(equivCommuteConstant J D K G hT hT').symm.app _ ≪≫
(sheafEquiv G J K D).functor.mapIso i ≪≫ (sheafEquiv G J K D).counitIso.app _⟩⟩
· exact fun ⟨Y, ⟨i⟩⟩ ↦ ⟨_, ⟨(equivCommuteConstant' J D K G hT hT').app _ ≪≫ (sheafEquiv G J K D).inverse.mapIso i⟩⟩
