English
If F is a functor with a left adjoint and certain fullness/faithfulness properties, then finitary extensivity of D implies finitary extensivity of C when F reflects limits and preserves colimits of a suitable shape.
Русский
Если F — автоперемещение слева с дополнительными свойствами полноты/верности, и F отражает пределы и сохраняет копроизведения соответствующей формы, тогда финитная расширяемость D влечет за собой финитную расширяемость C.
LaTeX
$$$FinitaryExtensive\; C$ под условиями, что $F: C\to D$ сохраняет и отражает пределы и совместимо сохраняет/отражает копродукты. Тогда $FinitaryExtensive\; C$.$$
Lean4
theorem finitaryExtensive_of_reflective [HasFiniteCoproducts D] [HasPullbacksOfInclusions D] [FinitaryExtensive C]
{Gl : C ⥤ D} {Gr : D ⥤ C} (adj : Gl ⊣ Gr) [Gr.Full] [Gr.Faithful]
[∀ X Y (f : X ⟶ Gl.obj Y), HasPullback (Gr.map f) (adj.unit.app Y)]
[∀ X Y (f : X ⟶ Gl.obj Y), PreservesLimit (cospan (Gr.map f) (adj.unit.app Y)) Gl]
[PreservesPullbacksOfInclusions Gl] : FinitaryExtensive D :=
by
have : PreservesColimitsOfSize Gl := adj.leftAdjoint_preservesColimits
constructor
intro X Y c hc
apply
(IsVanKampenColimit.precompose_isIso_iff
(Functor.isoWhiskerLeft _ (asIso adj.counit) ≪≫ Functor.rightUnitor _).hom).mp
have :
∀ (Z : C) (i : Discrete WalkingPair) (f : Z ⟶ (colimit.cocone (pair X Y ⋙ Gr)).pt),
PreservesLimit (cospan f ((colimit.cocone (pair X Y ⋙ Gr)).ι.app i)) Gl :=
by
have : pair X Y ⋙ Gr = pair (Gr.obj X) (Gr.obj Y) :=
by
apply Functor.hext
· rintro ⟨⟨⟩⟩ <;> rfl
· rintro ⟨⟨⟩⟩ ⟨j⟩ ⟨⟨rfl : _ = j⟩⟩ <;> simp
rw [this]
rintro Z ⟨_ | _⟩ f <;> dsimp <;> infer_instance
refine
((FinitaryExtensive.vanKampen _ (colimit.isColimit <| pair X Y ⋙ _)).map_reflective adj).of_iso
(IsColimit.uniqueUpToIso ?_ ?_)
· exact isColimitOfPreserves Gl (colimit.isColimit _)
· exact (IsColimit.precomposeHomEquiv _ _).symm hc
