feat(CategoryTheory/Localization): inverse in SmallShiftedHom (#32442)

The post/precomposition on the types `SmallShiftedHom W` with a morphism which satisfies `W` is a bijection.

Author: joelriou

Mathlib/CategoryTheory/Localization/SmallShiftedHom.lean

@@ -162,6 +162,14 @@ noncomputable def mk₀ [HasSmallLocalizedShiftedHom.{w} W M X Y]
     SmallShiftedHom.{w} W X Y m₀ :=
   SmallShiftedHom.mk _ (ShiftedHom.mk₀ _ hm₀ f)
 
+/-- The formal inverse in `SmallShiftedHom.{w} W Y X m₀` of a morphism `f : Y ⟶ X`
+such that `W f`. -/
+noncomputable def mk₀Inv [HasSmallLocalizedShiftedHom.{w} W M Y X] [W.RespectsIso]
+    (m₀ : M) (hm₀ : m₀ = 0) (f : X ⟶ Y) (hf : W f) :
+    SmallShiftedHom.{w} W Y X m₀ :=
+  SmallHom.mkInv ((shiftFunctorZero' C m₀ hm₀).hom.app X ≫ f)
+    (MorphismProperty.RespectsIso.precomp _ _ _ hf)
+
 end
 
 section
@@ -236,6 +244,17 @@ lemma equiv_mk₀ [HasSmallLocalizedShiftedHom.{w} W M X Y]
   simp only [comp_id, L.commShiftIso_zero, Functor.CommShift.isoZero_hom_app, assoc,
     ← Functor.map_comp_assoc, Iso.inv_hom_id_app, Functor.id_obj, Functor.map_id, id_comp]
 
+@[simp]
+lemma equiv_mk₀Inv [HasSmallLocalizedShiftedHom.{w} W M Y X] [W.RespectsIso]
+    (m₀ : M) (hm₀ : m₀ = 0) (f : X ⟶ Y) (hf : W f) :
+    equiv W L (mk₀Inv m₀ hm₀ f hf) =
+      ShiftedHom.mk₀ m₀ hm₀ ((isoOfHom L W f hf).inv) := by
+  have hf' : W ((shiftFunctorZero' C m₀ hm₀).hom.app X ≫ f) :=
+    MorphismProperty.RespectsIso.precomp _ _ _ hf
+  refine (SmallHom.equiv_mkInv L _ hf' =≫ _).trans ?_
+  rw [← cancel_epi (isoOfHom L W _ hf').hom, Iso.hom_inv_id_assoc]
+  simp [ShiftedHom.mk₀, Functor.commShiftIso_zero' _ _ m₀ hm₀]
+
 end
 
 section
@@ -257,6 +276,84 @@ lemma comp_assoc {X Y Z T : C} {a₁ a₂ a₃ a₁₂ a₂₃ a : M}
 
 end
 
+variable {W} in
+@[simp]
+lemma mk₀_comp_mk₀Inv {X Y : C} [HasSmallLocalizedShiftedHom.{w} W M X Y]
+    [HasSmallLocalizedShiftedHom.{w} W M Y Y]
+    [HasSmallLocalizedShiftedHom.{w} W M Y X] [W.IsCompatibleWithShift M] [W.RespectsIso]
+    (m₀ : M) (hm₀ : m₀ = 0) (f : Y ⟶ X) (hf : W f) :
+    (mk₀ W m₀ hm₀ f).comp (mk₀Inv m₀ hm₀ f hf) (by subst hm₀; simp) =
+      mk₀ W m₀ hm₀ (𝟙 Y) :=
+  (equiv W W.Q).injective (by simp [equiv_comp])
+
+variable {W} in
+@[simp]
+lemma mk₀Inv_comp_mk₀ {X Y : C} [HasSmallLocalizedShiftedHom.{w} W M X Y]
+    [HasSmallLocalizedShiftedHom.{w} W M X X]
+    [HasSmallLocalizedShiftedHom.{w} W M Y X] [W.IsCompatibleWithShift M] [W.RespectsIso]
+    (m₀ : M) (hm₀ : m₀ = 0) (f : Y ⟶ X) (hf : W f) :
+    (mk₀Inv m₀ hm₀ f hf).comp (mk₀ W m₀ hm₀ f) (by subst hm₀; simp) =
+      mk₀ W m₀ hm₀ (𝟙 X) :=
+  (equiv W W.Q).injective (by simp [equiv_comp])
+
+variable {W} in
+@[simp]
+lemma comp_mk₀_id {X Y : C} [HasSmallLocalizedShiftedHom.{w} W M X Y]
+    [HasSmallLocalizedShiftedHom.{w} W M Y Y]
+    [W.IsCompatibleWithShift M] {m : M}
+    (α : SmallShiftedHom.{w} W X Y m) (m₀ : M) (hm₀ : m₀ = 0) :
+    α.comp (mk₀ W m₀ hm₀ (𝟙 Y)) (by aesop) = α :=
+  (equiv W W.Q).injective (by simp [equiv_comp])
+
+variable {W} in
+@[simp]
+lemma mk₀_id_comp {X Y : C} [HasSmallLocalizedShiftedHom.{w} W M X Y]
+    [HasSmallLocalizedShiftedHom.{w} W M X X]
+    [HasSmallLocalizedShiftedHom.{w} W M Y Y]
+    [W.IsCompatibleWithShift M] {m : M}
+    (α : SmallShiftedHom.{w} W X Y m) (m₀ : M) (hm₀ : m₀ = 0) :
+    (mk₀ W m₀ hm₀ (𝟙 X)).comp α (by aesop) = α :=
+  (equiv W W.Q).injective (by simp [equiv_comp])
+
+variable {W} in
+/-- The postcomposition on the types `SmallShiftedHom W` with a morphism
+which satisfies `W` is a bijection. -/
+@[simps!]
+noncomputable def postcompEquiv {X Y Z : C}
+    [W.RespectsIso] [W.IsCompatibleWithShift M]
+    [HasSmallLocalizedShiftedHom.{w} W M X Y]
+    [HasSmallLocalizedShiftedHom.{w} W M Y Z]
+    [HasSmallLocalizedShiftedHom.{w} W M X Z]
+    [HasSmallLocalizedShiftedHom.{w} W M Z Y]
+    [HasSmallLocalizedShiftedHom.{w} W M Y Y]
+    [HasSmallLocalizedShiftedHom.{w} W M Z Z]
+    (f : Y ⟶ Z) (hf : W f) {a : M} :
+    SmallShiftedHom.{w} W X Y a ≃ SmallShiftedHom.{w} W X Z a where
+  toFun α := α.comp (mk₀ _ _ rfl f) (zero_add _)
+  invFun β := β.comp (mk₀Inv _ rfl _ hf) (zero_add _)
+  left_inv α := by simp [comp_assoc]
+  right_inv β := by simp [comp_assoc]
+
+variable {W} in
+/-- The precomposition on the types `SmallShiftedHom W` with a morphism
+which satisfies `W` is a bijection. -/
+@[simps!]
+noncomputable def precompEquiv {X Y Z : C}
+    [W.RespectsIso] [W.IsCompatibleWithShift M]
+    [HasSmallLocalizedShiftedHom.{w} W M X X]
+    [HasSmallLocalizedShiftedHom.{w} W M Y Y]
+    [HasSmallLocalizedShiftedHom.{w} W M X Y]
+    [HasSmallLocalizedShiftedHom.{w} W M Y X]
+    [HasSmallLocalizedShiftedHom.{w} W M Y Z]
+    [HasSmallLocalizedShiftedHom.{w} W M X Z]
+    [HasSmallLocalizedShiftedHom.{w} W M Z Z]
+    (f : X ⟶ Y) (hf : W f) {a : M} :
+    SmallShiftedHom.{w} W Y Z a ≃ SmallShiftedHom.{w} W X Z a where
+  toFun α := (mk₀ _ _ rfl f).comp α (add_zero _)
+  invFun β := (mk₀Inv _ rfl _ hf).comp β (add_zero _)
+  left_inv α := by simp [← comp_assoc]
+  right_inv β  := by simp [← comp_assoc]
+
 section ChangeOfUniverse
 
 variable {W}