English
If L1 localizes C1 to D1 and L2 localizes C2 to D2 with equivalences between the source and target, localization transfers along the equivalences.
Русский
Если локализация L1 локализует C1 в D1, а L2 локализует C2 в D2 и существуют эквиваленции между источниками и целями, локализация передаётся через эквивалентности.
LaTeX
$$$\\text{of_equivalences }(L_1,W_1,L_2,W_2,E,E',\\_ ) : L_2.IsLocalization W_2$$$
Lean4
/-- If `L₁ : C₁ ⥤ D` is a localization functor for `W₁ : MorphismProperty C₁`, then it is also
the case of a functor `L₂ : C₂ ⥤ D` for a suitable `W₂ : MorphismProperty C₂` when
we have an equivalence of category `E : C₁ ≌ C₂` and an isomorphism `E.functor ⋙ L₂ ≅ L₁`. -/
theorem of_equivalence_source (L₁ : C₁ ⥤ D) (W₁ : MorphismProperty C₁) (L₂ : C₂ ⥤ D) (W₂ : MorphismProperty C₂)
(E : C₁ ≌ C₂) (hW₁ : W₁ ≤ W₂.isoClosure.inverseImage E.functor) (hW₂ : W₂.IsInvertedBy L₂) [L₁.IsLocalization W₁]
(iso : E.functor ⋙ L₂ ≅ L₁) : L₂.IsLocalization W₂ :=
by
have h : W₁.IsInvertedBy (E.functor ⋙ W₂.Q) := fun _ _ f hf =>
by
obtain ⟨_, _, f', hf', ⟨e⟩⟩ := hW₁ f hf
exact
((MorphismProperty.isomorphisms _).arrow_mk_iso_iff (W₂.Q.mapArrow.mapIso e)).1
(Localization.inverts W₂.Q W₂ _ hf')
exact
{ inverts := hW₂
isEquivalence :=
Localization.isEquivalence W₂.Q W₂ L₁ W₁ L₂ (Construction.lift L₂ hW₂) (E.functor ⋙ W₂.Q)
(Localization.lift (E.functor ⋙ W₂.Q) h L₁)
(by
calc
L₂ ⋙ lift (E.functor ⋙ W₂.Q) h L₁ ≅ _ := (leftUnitor _).symm
_ ≅ _ := (isoWhiskerRight E.counitIso.symm _)
_ ≅ E.inverse ⋙ E.functor ⋙ L₂ ⋙ lift (E.functor ⋙ W₂.Q) h L₁ := (Functor.associator _ _ _)
_ ≅ E.inverse ⋙ L₁ ⋙ lift (E.functor ⋙ W₂.Q) h L₁ :=
(isoWhiskerLeft E.inverse ((Functor.associator _ _ _).symm ≪≫ isoWhiskerRight iso _))
_ ≅ E.inverse ⋙ E.functor ⋙ W₂.Q := (isoWhiskerLeft _ (Localization.fac (E.functor ⋙ W₂.Q) h L₁))
_ ≅ (E.inverse ⋙ E.functor) ⋙ W₂.Q := (Functor.associator _ _ _).symm
_ ≅ 𝟭 C₂ ⋙ W₂.Q := (isoWhiskerRight E.counitIso _)
_ ≅ W₂.Q := leftUnitor _)
(Functor.associator _ _ _ ≪≫ isoWhiskerLeft _ (Lifting.iso W₂.Q W₂ _ _) ≪≫ iso) }
