English
For a finite index J, the whiskering with a discrete J-object category preserves localization: the induced functor on functors from C to D to functors from C to E localizes with respect to the pointwise morphism property.
Русский
При конечном индексе J взятие whiskering справа на дискретной категории J сохраняет локализацию: индуцованный функтор между категориями функторов локализуется по точечному свойству морфизмов.
LaTeX
$$$((\\text{whiskeringRight } (\\mathbf{Discrete} J) C D).obj L).IsLocalization( W.functorCategory(\\mathbf{Discrete} J) )$$$
Lean4
/-- If `L : C ⥤ D` is a localization functor for `W : MorphismProperty C`, then
the induced functor `(Discrete J ⥤ C) ⥤ (Discrete J ⥤ D)` is also a localization
for `W.functorCategory (Discrete J)` if `W` contains identities. -/
instance {J : Type} [Finite J] {C : Type u₁} {D : Type u₂} [Category.{v₁} C] [Category.{v₂} D] (L : C ⥤ D)
(W : MorphismProperty C) [W.ContainsIdentities] [L.IsLocalization W] :
((whiskeringRight (Discrete J) C D).obj L).IsLocalization (W.functorCategory (Discrete J)) :=
by
let E := piEquivalenceFunctorDiscrete J C
let E' := piEquivalenceFunctorDiscrete J D
let L₂ := (whiskeringRight (Discrete J) C D).obj L
let L₁ := Functor.pi (fun (_ : J) => L)
have : CatCommSq E.functor L₁ L₂ E'.functor :=
⟨(Functor.rightUnitor _).symm ≪≫
isoWhiskerLeft _ E'.counitIso.symm ≪≫
Functor.associator _ _ _ ≪≫
isoWhiskerLeft _ ((Functor.associator _ _ _).symm ≪≫ isoWhiskerRight (by exact Iso.refl _) _) ≪≫
(Functor.associator _ _ _).symm ≪≫
isoWhiskerRight ((Functor.associator _ _ _).symm ≪≫ isoWhiskerRight E.unitIso.symm L₁) _ ≪≫
isoWhiskerRight L₁.leftUnitor _⟩
refine Functor.IsLocalization.of_equivalences L₁ (MorphismProperty.pi (fun _ => W)) L₂ _ E E' ?_ ?_
· intro X Y f hf
exact MorphismProperty.le_isoClosure _ _ (fun ⟨j⟩ => hf j)
· intro X Y f hf
have : ∀ (j : Discrete J), IsIso ((L₂.map f).app j) := fun j => Localization.inverts L W _ (hf j)
apply NatIso.isIso_of_isIso_app
