C : Type u_4
D : Type u_6
inst✝⁴ : Category C
inst✝³ : Category D
L : C ⥤ D
W : MorphismProperty C
E✝ : Type ?u.77743
inst✝² : Category E✝
E : Type u_1
inst✝¹ : Category E
L' : C ⥤ E
eq : D ≌ E
inst✝ : IsLocalization L W
e : L ⋙ eq.functor ≅ L'
h : MorphismProperty.IsInvertedBy W L'
⊢ IsLocalization L' W
C : Type u_4
D : Type u_6
inst✝⁴ : Category C
inst✝³ : Category D
L : C ⥤ D
W : MorphismProperty C
E✝ : Type ?u.77743
inst✝² : Category E✝
E : Type u_1
inst✝¹ : Category E
L' : C ⥤ E
eq : D ≌ E
inst✝ : IsLocalization L W
e : L ⋙ eq.functor ≅ L'
⊢ IsLocalization L' W
have h : W.IsInvertedBy L' := by
  rw [← MorphismProperty.IsInvertedBy.iff_of_iso W e]
  exact MorphismProperty.IsInvertedBy.of_comp W L (Localization.inverts L W) eq.functor
C : Type u_4
D : Type u_6
inst✝⁴ : Category C
inst✝³ : Category D
L : C ⥤ D
W : MorphismProperty C
E✝ : Type ?u.77743
inst✝² : Category E✝
E : Type u_1
inst✝¹ : Category E
L' : C ⥤ E
eq : D ≌ E
inst✝ : IsLocalization L W
e : L ⋙ eq.functor ≅ L'
h : MorphismProperty.IsInvertedBy W L'
F₁ : MorphismProperty.Localization W ⥤ D := Construction.lift L (_ : MorphismProperty.IsInvertedBy W L)
⊢ IsLocalization L' W
C : Type u_4
D : Type u_6
inst✝⁴ : Category C
inst✝³ : Category D
L : C ⥤ D
W : MorphismProperty C
E✝ : Type ?u.77743
inst✝² : Category E✝
E : Type u_1
inst✝¹ : Category E
L' : C ⥤ E
eq : D ≌ E
inst✝ : IsLocalization L W
e : L ⋙ eq.functor ≅ L'
h : MorphismProperty.IsInvertedBy W L'
⊢ IsLocalization L' W
let F₁ := Localization.Construction.lift L (Localization.inverts L W)
C : Type u_4
D : Type u_6
inst✝⁴ : Category C
inst✝³ : Category D
L : C ⥤ D
W : MorphismProperty C
E✝ : Type ?u.77743
inst✝² : Category E✝
E : Type u_1
inst✝¹ : Category E
L' : C ⥤ E
eq : D ≌ E
inst✝ : IsLocalization L W
e : L ⋙ eq.functor ≅ L'
h : MorphismProperty.IsInvertedBy W L'
F₁ : MorphismProperty.Localization W ⥤ D := Construction.lift L (_ : MorphismProperty.IsInvertedBy W L)
F₂ : MorphismProperty.Localization W ⥤ E := Construction.lift L' h
⊢ IsLocalization L' W
C : Type u_4
D : Type u_6
inst✝⁴ : Category C
inst✝³ : Category D
L : C ⥤ D
W : MorphismProperty C
E✝ : Type ?u.77743
inst✝² : Category E✝
E : Type u_1
inst✝¹ : Category E
L' : C ⥤ E
eq : D ≌ E
inst✝ : IsLocalization L W
e : L ⋙ eq.functor ≅ L'
h : MorphismProperty.IsInvertedBy W L'
F₁ : MorphismProperty.Localization W ⥤ D := Construction.lift L (_ : MorphismProperty.IsInvertedBy W L)
⊢ IsLocalization L' W
let F₂ := Localization.Construction.lift L' h
C : Type u_4
D : Type u_6
inst✝⁴ : Category C
inst✝³ : Category D
L : C ⥤ D
W : MorphismProperty C
E✝ : Type ?u.77743
inst✝² : Category E✝
E : Type u_1
inst✝¹ : Category E
L' : C ⥤ E
eq : D ≌ E
inst✝ : IsLocalization L W
e : L ⋙ eq.functor ≅ L'
h : MorphismProperty.IsInvertedBy W L'
F₁ : MorphismProperty.Localization W ⥤ D := Construction.lift L (_ : MorphismProperty.IsInvertedBy W L)
F₂ : MorphismProperty.Localization W ⥤ E := Construction.lift L' h
e' : F₁ ⋙ eq.functor ≅ F₂ := liftNatIso (MorphismProperty.Q W) W (L ⋙ eq.functor) L' (F₁ ⋙ eq.functor) F₂ e
⊢ IsLocalization L' W
C : Type u_4
D : Type u_6
inst✝⁴ : Category C
inst✝³ : Category D
L : C ⥤ D
W : MorphismProperty C
E✝ : Type ?u.77743
inst✝² : Category E✝
E : Type u_1
inst✝¹ : Category E
L' : C ⥤ E
eq : D ≌ E
inst✝ : IsLocalization L W
e : L ⋙ eq.functor ≅ L'
h : MorphismProperty.IsInvertedBy W L'
F₁ : MorphismProperty.Localization W ⥤ D := Construction.lift L (_ : MorphismProperty.IsInvertedBy W L)
F₂ : MorphismProperty.Localization W ⥤ E := Construction.lift L' h
⊢ IsLocalization L' W
let e' : F₁ ⋙ eq.functor ≅ F₂ := liftNatIso W.Q W (L ⋙ eq.functor) L' _ _ e
no goals
C : Type u_4
D : Type u_6
inst✝⁴ : Category C
inst✝³ : Category D
L : C ⥤ D
W : MorphismProperty C
E✝ : Type ?u.77743
inst✝² : Category E✝
E : Type u_1
inst✝¹ : Category E
L' : C ⥤ E
eq : D ≌ E
inst✝ : IsLocalization L W
e : L ⋙ eq.functor ≅ L'
h : MorphismProperty.IsInvertedBy W L'
F₁ : MorphismProperty.Localization W ⥤ D := Construction.lift L (_ : MorphismProperty.IsInvertedBy W L)
F₂ : MorphismProperty.Localization W ⥤ E := Construction.lift L' h
e' : F₁ ⋙ eq.functor ≅ F₂ := liftNatIso (MorphismProperty.Q W) W (L ⋙ eq.functor) L' (F₁ ⋙ eq.functor) F₂ e
⊢ IsLocalization L' W
exact
  { inverts := h
    nonempty_isEquivalence := Nonempty.intro (IsEquivalence.ofIso e' inferInstance) }
C : Type u_4
D : Type u_6
inst✝⁴ : Category C
inst✝³ : Category D
L : C ⥤ D
W : MorphismProperty C
E✝ : Type ?u.77743
inst✝² : Category E✝
E : Type u_1
inst✝¹ : Category E
L' : C ⥤ E
eq : D ≌ E
inst✝ : IsLocalization L W
e : L ⋙ eq.functor ≅ L'
⊢ MorphismProperty.IsInvertedBy W (L ⋙ eq.functor)
C : Type u_4
D : Type u_6
inst✝⁴ : Category C
inst✝³ : Category D
L : C ⥤ D
W : MorphismProperty C
E✝ : Type ?u.77743
inst✝² : Category E✝
E : Type u_1
inst✝¹ : Category E
L' : C ⥤ E
eq : D ≌ E
inst✝ : IsLocalization L W
e : L ⋙ eq.functor ≅ L'
⊢ MorphismProperty.IsInvertedBy W L'
rw [← MorphismProperty.IsInvertedBy.iff_of_iso W e]
no goals
C : Type u_4
D : Type u_6
inst✝⁴ : Category C
inst✝³ : Category D
L : C ⥤ D
W : MorphismProperty C
E✝ : Type ?u.77743
inst✝² : Category E✝
E : Type u_1
inst✝¹ : Category E
L' : C ⥤ E
eq : D ≌ E
inst✝ : IsLocalization L W
e : L ⋙ eq.functor ≅ L'
⊢ MorphismProperty.IsInvertedBy W (L ⋙ eq.functor)
exact MorphismProperty.IsInvertedBy.of_comp W L (Localization.inverts L W) eq.functor