mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
J : Type u_1
inst✝ : Category.{v_1, u_1} J
R : J ⥤ F.PartialRightAdjointSource
c : Cone (R ⋙ F.rightAdjointObjIsDefined.ι)
hc : IsLimit c
c' : Cone (R ⋙ F.partialRightAdjoint)
hc' : IsLimit c'
Y Y' : C
g : Y ⟶ Y'
f : Y' ⟶ c'.pt
j : J
⊢ {
          toFun := fun f ↦
            hc.lift
              { pt := F.1 Y, π := { app := fun j ↦ F.partialRightAdjointHomEquiv (f ≫ c'.π.app j), naturality := ⋯ } },
          invFun := fun g ↦
            hc'.lift
              { pt := Y, π := { app := fun j ↦ F.partialRightAdjointHomEquiv.symm (g ≫ c.π.app j), naturality := ⋯ } },
          left_inv := ⋯, right_inv := ⋯ }
        (g ≫ f) ≫
      c.π.app j =
    (ConcreteCategory.hom ((F.op ⋙ yoneda.obj c.pt).map g.op))
        ({
            toFun := fun f ↦
              hc.lift
                { pt := F.1 Y',
                  π := { app := fun j ↦ F.partialRightAdjointHomEquiv (f ≫ c'.π.app j), naturality := ⋯ } },
            invFun := fun g ↦
              hc'.lift
                { pt := Y',
                  π := { app := fun j ↦ F.partialRightAdjointHomEquiv.symm (g ≫ c.π.app j), naturality := ⋯ } },
            left_inv := ⋯, right_inv := ⋯ }
          f) ≫
      c.π.app j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.CompositionIso

Goal state before:
pp: C₀ : Type u_1
inst✝ : Category.{v_1, u_1} C₀
F G : C₀ ⥤ C₀
adj : F ⊣ G
e : G ≅ 𝟭 C₀
⊢ (conjugateEquiv id adj) (adj.leftAdjointIdIso e).hom = e.inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.CompositionIso

Goal state before:
pp: C₀ : Type u_1
C₁ : Type u_2
C₂ : Type u_3
inst✝² : Category.{v_1, u_1} C₀
inst✝¹ : Category.{v_2, u_2} C₁
inst✝ : Category.{v_3, u_3} C₂
F₀₁ : C₀ ⥤ C₁
F₁₂ : C₁ ⥤ C₂
F₀₂ : C₀ ⥤ C₂
G₁₀ : C₁ ⥤ C₀
G₂₁ : C₂ ⥤ C₁
G₂₀ : C₂ ⥤ C₀
adj₀₁ : F₀₁ ⊣ G₁₀
adj₁₂ : F₁₂ ⊣ G₂₁
adj₀₂ : F₀₂ ⊣ G₂₀
e₀₁₂ : G₂₁ ⋙ G₁₀ ≅ G₂₀
⊢ (conjugateEquiv (adj₀₁.comp adj₁₂) adj₀₂) (adj₀₁.leftAdjointCompIso adj₁₂ adj₀₂ e₀₁₂).inv = e₀₁₂.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.CompositionIso

Goal state before:
pp: C₀ : Type u_1
C₁ : Type u_2
inst✝¹ : Category.{v_1, u_1} C₀
inst✝ : Category.{v_2, u_2} C₁
F₀₁ : C₀ ⥤ C₁
F₁₁' : C₁ ⥤ C₁
G₁₀ : C₁ ⥤ C₀
G₁'₁ : C₁ ⥤ C₁
adj₀₁ : F₀₁ ⊣ G₁₀
adj₁₁' : F₁₁' ⊣ G₁'₁
e₀₁₁' : G₁'₁ ⋙ G₁₀ ≅ G₁₀
e₁'₁ : G₁'₁ ≅ 𝟭 C₁
h : e₀₁₁' = isoWhiskerRight e₁'₁ G₁₀ ≪≫ G₁₀.leftUnitor
⊢ adj₀₁.leftAdjointCompIso adj₁₁' adj₀₁ e₀₁₁' = F₀₁.isoWhiskerLeft (adj₁₁'.leftAdjointIdIso e₁'₁) ≪≫ F₀₁.rightUnitor

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
⊢ map hcR hcM hcM (𝟙 M) = LinearMap.id

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.CompositionIso

Goal state before:
pp: C₀ : Type u_1
C₁ : Type u_2
inst✝¹ : Category.{v_1, u_1} C₀
inst✝ : Category.{v_2, u_2} C₁
F₀₀' : C₀ ⥤ C₀
F₀'₁ : C₀ ⥤ C₁
G₀'₀ : C₀ ⥤ C₀
G₁₀' : C₁ ⥤ C₀
adj₀₀' : F₀₀' ⊣ G₀'₀
adj₀'₁ : F₀'₁ ⊣ G₁₀'
e₀'₀ : G₀'₀ ≅ 𝟭 C₀
X₀ : C₀
h₁ :
  F₀'₁.map ((G₀'₀ ⋙ F₀₀').map (adj₀'₁.unit.app X₀) ≫ adj₀₀'.counit.app ((F₀'₁ ⋙ G₁₀').obj X₀)) =
    F₀'₁.map (adj₀₀'.counit.app ((𝟭 C₀).obj X₀) ≫ (𝟭 C₀).map (adj₀'₁.unit.app X₀))
h₂ :
  (F₀₀' ⋙ F₀'₁).map ((𝟭 C₀).map (adj₀'₁.unit.app X₀) ≫ e₀'₀.inv.app ((F₀'₁ ⋙ G₁₀').obj X₀)) =
    (F₀₀' ⋙ F₀'₁).map (e₀'₀.inv.app ((𝟭 C₀).obj X₀) ≫ G₀'₀.map (adj₀'₁.unit.app X₀))
⊢ (adj₀₀'.leftAdjointCompIso adj₀'₁ adj₀'₁ (G₁₀'.isoWhiskerLeft e₀'₀ ≪≫ G₁₀'.rightUnitor)).hom.app X₀ =
    (isoWhiskerRight (adj₀₀'.leftAdjointIdIso e₀'₀) F₀'₁ ≪≫ F₀'₁.leftUnitor).hom.app X₀

Tactic:
simp only [id_obj, comp_obj, Functor.id_map, Functor.comp_map, Functor.map_comp] at h₁ h₂

Goal state after:
C₀ : Type u_1
C₁ : Type u_2
inst✝¹ : Category.{v_1, u_1} C₀
inst✝ : Category.{v_2, u_2} C₁
F₀₀' : C₀ ⥤ C₀
F₀'₁ : C₀ ⥤ C₁
G₀'₀ : C₀ ⥤ C₀
G₁₀' : C₁ ⥤ C₀
adj₀₀' : F₀₀' ⊣ G₀'₀
adj₀'₁ : F₀'₁ ⊣ G₁₀'
e₀'₀ : G₀'₀ ≅ 𝟭 C₀
X₀ : C₀
h₁ :
  F₀'₁.map (F₀₀'.map (G₀'₀.map (adj₀'₁.unit.app X₀))) ≫ F₀'₁.map (adj₀₀'.counit.app (G₁₀'.obj (F₀'₁.obj X₀))) =
    F₀'₁.map (adj₀₀'.counit.app X₀) ≫ F₀'₁.map (adj₀'₁.unit.app X₀)
h₂ :
  F₀'₁.map (F₀₀'.map (adj₀'₁.unit.app X₀)) ≫ F₀'₁.map (F₀₀'.map (e₀'₀.inv.app (G₁₀'.obj (F₀'₁.obj X₀)))) =
    F₀'₁.map (F₀₀'.map (e₀'₀.inv.app X₀)) ≫ F₀'₁.map (F₀₀'.map (G₀'₀.map (adj₀'₁.unit.app X₀)))
⊢ (adj₀₀'.leftAdjointCompIso adj₀'₁ adj₀'₁ (G₁₀'.isoWhiskerLeft e₀'₀ ≪≫ G₁₀'.rightUnitor)).hom.app X₀ =
    (isoWhiskerRight (adj₀₀'.leftAdjointIdIso e₀'₀) F₀'₁ ≪≫ F₀'₁.leftUnitor).hom.app X₀
Module: Mathlib.CategoryTheory.Adjunction.CompositionIso

Goal state before:
pp: C₀ : Type u_1
C₁ : Type u_2
inst✝¹ : Category.{v_1, u_1} C₀
inst✝ : Category.{v_2, u_2} C₁
F₀₀' : C₀ ⥤ C₀
F₀'₁ : C₀ ⥤ C₁
G₀'₀ : C₀ ⥤ C₀
G₁₀' : C₁ ⥤ C₀
adj₀₀' : F₀₀' ⊣ G₀'₀
adj₀'₁ : F₀'₁ ⊣ G₁₀'
e₀₀'₁ : G₁₀' ⋙ G₀'₀ ≅ G₁₀'
e₀'₀ : G₀'₀ ≅ 𝟭 C₀
h : e₀₀'₁ = G₁₀'.isoWhiskerLeft e₀'₀ ≪≫ G₁₀'.rightUnitor
⊢ adj₀₀'.leftAdjointCompIso adj₀'₁ adj₀'₁ e₀₀'₁ = isoWhiskerRight (adj₀₀'.leftAdjointIdIso e₀'₀) F₀'₁ ≪≫ F₀'₁.leftUnitor

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
f : M ⟶ M'
M'' : PresheafOfModules R
cM'' : Cocone M''.presheaf
hcM'' : IsColimit cM''
g : M' ⟶ M''
⊢ map hcR hcM' hcM'' g ∘ₗ map hcR hcM hcM' f = map hcR hcM hcM'' (f ≫ g)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
N : ModuleCat ↑cR.pt
φ' : ModuleCat.of (↑cR.pt) (ModuleColimit hcR hcM') ⟶ N
f : M ⟶ M'
⊢ (homEquiv hcR hcM) (ModuleCat.ofHom (map hcR hcM hcM' f) ≫ φ') = f ≫ (homEquiv hcR hcM') φ'

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.CompositionIso

Goal state before:
pp: C₀ : Type u_1
C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
inst✝³ : Category.{v_1, u_1} C₀
inst✝² : Category.{v_2, u_2} C₁
inst✝¹ : Category.{v_3, u_3} C₂
inst✝ : Category.{v_4, u_4} C₃
F₀₁ : C₀ ⥤ C₁
F₁₂ : C₁ ⥤ C₂
F₂₃ : C₂ ⥤ C₃
F₁₃ : C₁ ⥤ C₃
F₀₃ : C₀ ⥤ C₃
G₁₀ : C₁ ⥤ C₀
G₂₁ : C₂ ⥤ C₁
G₃₂ : C₃ ⥤ C₂
G₃₁ : C₃ ⥤ C₁
G₃₀ : C₃ ⥤ C₀
adj₀₁ : F₀₁ ⊣ G₁₀
adj₁₂ : F₁₂ ⊣ G₂₁
adj₂₃ : F₂₃ ⊣ G₃₂
adj₁₃ : F₁₃ ⊣ G₃₁
adj₀₃ : F₀₃ ⊣ G₃₀
τ₁₂₃ : G₃₁ ⟶ G₃₂ ⋙ G₂₁
τ₀₁₃ : G₃₀ ⟶ G₃₁ ⋙ G₁₀
⊢ F₀₁.whiskerLeft (adj₁₂.leftAdjointCompNatTrans adj₂₃ adj₁₃ τ₁₂₃) ≫ adj₀₁.leftAdjointCompNatTrans adj₁₃ adj₀₃ τ₀₁₃ =
    (conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃))).symm (τ₀₁₃ ≫ whiskerRight τ₁₂₃ G₁₀)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
N : ModuleCat ↑cR.pt
f : M ⟶ M'
g : M' ⟶ (constFunctor cR).obj N
⊢ (homEquiv hcR hcM) ((homEquiv hcR hcM).symm (f ≫ g)) =
    (homEquiv hcR hcM) (ModuleCat.ofHom (map hcR hcM hcM' f) ≫ (homEquiv hcR hcM').symm g)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
X✝ Y✝ Z✝ : PresheafOfModules R
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ModuleCat.ofHom (ModuleColimit.map hcR (colimit.isColimit X✝.presheaf) (colimit.isColimit Z✝.presheaf) (f ≫ g)) =
    ModuleCat.ofHom (ModuleColimit.map hcR (colimit.isColimit X✝.presheaf) (colimit.isColimit Y✝.presheaf) f) ≫
      ModuleCat.ofHom (ModuleColimit.map hcR (colimit.isColimit Y✝.presheaf) (colimit.isColimit Z✝.presheaf) g)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
F : PresheafOfModules R
G : ModuleCat ↑cR.pt
⊢ (colimitAdjunction hcR).homEquiv F G = ↑(ModuleColimit.homEquiv hcR (colimit.isColimit F.presheaf))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
F : PresheafOfModules R
G : ModuleCat ↑cR.pt
β : F ⟶ (constFunctor cR).obj G
X : Cᵒᵖ
m : ↑(F.obj X)
⊢ (ConcreteCategory.hom (((colimitAdjunction hcR).homEquiv F G).symm β)) (ιM m) = (ConcreteCategory.hom (β.app X)) m

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.CompositionIso

Goal state before:
pp: C₀ : Type u_1
C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
inst✝³ : Category.{v_1, u_1} C₀
inst✝² : Category.{v_2, u_2} C₁
inst✝¹ : Category.{v_3, u_3} C₂
inst✝ : Category.{v_4, u_4} C₃
F₀₁ : C₀ ⥤ C₁
F₁₂ : C₁ ⥤ C₂
F₂₃ : C₂ ⥤ C₃
F₀₂ : C₀ ⥤ C₂
F₀₃ : C₀ ⥤ C₃
G₁₀ : C₁ ⥤ C₀
G₂₁ : C₂ ⥤ C₁
G₃₂ : C₃ ⥤ C₂
G₂₀ : C₂ ⥤ C₀
G₃₀ : C₃ ⥤ C₀
adj₀₁ : F₀₁ ⊣ G₁₀
adj₁₂ : F₁₂ ⊣ G₂₁
adj₂₃ : F₂₃ ⊣ G₃₂
adj₀₂ : F₀₂ ⊣ G₂₀
adj₀₃ : F₀₃ ⊣ G₃₀
τ₀₁₂ : G₂₀ ⟶ G₂₁ ⋙ G₁₀
τ₀₂₃ : G₃₀ ⟶ G₃₂ ⋙ G₂₀
⊢ (F₀₁.associator F₁₂ F₂₃).inv ≫
      whiskerRight (adj₀₁.leftAdjointCompNatTrans adj₁₂ adj₀₂ τ₀₁₂) F₂₃ ≫
        adj₀₂.leftAdjointCompNatTrans adj₂₃ adj₀₃ τ₀₂₃ =
    (conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃))).symm
      (τ₀₂₃ ≫ G₃₂.whiskerLeft τ₀₁₂ ≫ (G₃₂.associator G₂₁ G₁₀).inv)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.CompositionIso

Goal state before:
pp: C₀ : Type u_1
C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
inst✝³ : Category.{v_1, u_1} C₀
inst✝² : Category.{v_2, u_2} C₁
inst✝¹ : Category.{v_3, u_3} C₂
inst✝ : Category.{v_4, u_4} C₃
F₀₁ : C₀ ⥤ C₁
F₁₂ : C₁ ⥤ C₂
F₂₃ : C₂ ⥤ C₃
F₀₂ : C₀ ⥤ C₂
F₁₃ : C₁ ⥤ C₃
F₀₃ : C₀ ⥤ C₃
G₁₀ : C₁ ⥤ C₀
G₂₁ : C₂ ⥤ C₁
G₃₂ : C₃ ⥤ C₂
G₂₀ : C₂ ⥤ C₀
G₃₁ : C₃ ⥤ C₁
G₃₀ : C₃ ⥤ C₀
adj₀₁ : F₀₁ ⊣ G₁₀
adj₁₂ : F₁₂ ⊣ G₂₁
adj₂₃ : F₂₃ ⊣ G₃₂
adj₀₂ : F₀₂ ⊣ G₂₀
adj₁₃ : F₁₃ ⊣ G₃₁
adj₀₃ : F₀₃ ⊣ G₃₀
τ₀₁₂ : G₂₀ ⟶ G₂₁ ⋙ G₁₀
τ₁₂₃ : G₃₁ ⟶ G₃₂ ⋙ G₂₁
τ₀₁₃ : G₃₀ ⟶ G₃₁ ⋙ G₁₀
τ₀₂₃ : G₃₀ ⟶ G₃₂ ⋙ G₂₀
h : τ₀₂₃ ≫ G₃₂.whiskerLeft τ₀₁₂ = τ₀₁₃ ≫ whiskerRight τ₁₂₃ G₁₀ ≫ (G₃₂.associator G₂₁ G₁₀).hom
⊢ F₀₁.whiskerLeft (adj₁₂.leftAdjointCompNatTrans adj₂₃ adj₁₃ τ₁₂₃) ≫ adj₀₁.leftAdjointCompNatTrans adj₁₃ adj₀₃ τ₀₁₃ =
    (F₀₁.associator F₁₂ F₂₃).inv ≫
      whiskerRight (adj₀₁.leftAdjointCompNatTrans adj₁₂ adj₀₂ τ₀₁₂) F₂₃ ≫ adj₀₂.leftAdjointCompNatTrans adj₂₃ adj₀₃ τ₀₂₃

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.CompositionIso

Goal state before:
pp: C₀ : Type u_1
C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
inst✝³ : Category.{v_1, u_1} C₀
inst✝² : Category.{v_2, u_2} C₁
inst✝¹ : Category.{v_3, u_3} C₂
inst✝ : Category.{v_4, u_4} C₃
F₀₁ : C₀ ⥤ C₁
F₁₂ : C₁ ⥤ C₂
F₂₃ : C₂ ⥤ C₃
F₀₂ : C₀ ⥤ C₂
F₁₃ : C₁ ⥤ C₃
F₀₃ : C₀ ⥤ C₃
G₁₀ : C₁ ⥤ C₀
G₂₁ : C₂ ⥤ C₁
G₃₂ : C₃ ⥤ C₂
G₂₀ : C₂ ⥤ C₀
G₃₁ : C₃ ⥤ C₁
G₃₀ : C₃ ⥤ C₀
adj₀₁ : F₀₁ ⊣ G₁₀
adj₁₂ : F₁₂ ⊣ G₂₁
adj₂₃ : F₂₃ ⊣ G₃₂
adj₀₂ : F₀₂ ⊣ G₂₀
adj₁₃ : F₁₃ ⊣ G₃₁
adj₀₃ : F₀₃ ⊣ G₃₀
e₀₁₂ : G₂₁ ⋙ G₁₀ ≅ G₂₀
e₁₂₃ : G₃₂ ⋙ G₂₁ ≅ G₃₁
e₀₁₃ : G₃₁ ⋙ G₁₀ ≅ G₃₀
e₀₂₃ : G₃₂ ⋙ G₂₀ ≅ G₃₀
h : G₃₂.isoWhiskerLeft e₀₁₂ ≪≫ e₀₂₃ = (G₃₂.associator G₂₁ G₁₀).symm ≪≫ isoWhiskerRight e₁₂₃ G₁₀ ≪≫ e₀₁₃
⊢ e₀₂₃.symm.hom ≫ G₃₂.whiskerLeft e₀₁₂.symm.hom =
    e₀₁₃.symm.hom ≫ whiskerRight e₁₂₃.symm.hom G₁₀ ≫ (G₃₂.associator G₂₁ G₁₀).hom

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback

Goal state before:
pp: C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
S : Cᵒᵖ ⥤ RingCat
φ : S ⟶ F.op ⋙ R
X : C
M N : PresheafOfModules R
g : M ⟶ N
f : (free R).obj (yoneda.obj (F.obj X)) ⟶ M
⊢ freeYonedaEquiv ((freeYonedaEquiv.trans freeYonedaEquiv.symm) (f ≫ g)) =
    freeYonedaEquiv
      ((ConcreteCategory.hom ((pushforward φ ⋙ coyoneda.obj (op ((free S).obj (yoneda.obj X)))).map g))
        ((freeYonedaEquiv.trans freeYonedaEquiv.symm) f))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.CompositionIso

Goal state before:
pp: C₀ : Type u_1
C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
inst✝³ : Category.{v_1, u_1} C₀
inst✝² : Category.{v_2, u_2} C₁
inst✝¹ : Category.{v_3, u_3} C₂
inst✝ : Category.{v_4, u_4} C₃
F₀₁ : C₀ ⥤ C₁
F₁₂ : C₁ ⥤ C₂
F₂₃ : C₂ ⥤ C₃
F₀₂ : C₀ ⥤ C₂
F₁₃ : C₁ ⥤ C₃
F₀₃ : C₀ ⥤ C₃
G₁₀ : C₁ ⥤ C₀
G₂₁ : C₂ ⥤ C₁
G₃₂ : C₃ ⥤ C₂
G₂₀ : C₂ ⥤ C₀
G₃₁ : C₃ ⥤ C₁
G₃₀ : C₃ ⥤ C₀
adj₀₁ : F₀₁ ⊣ G₁₀
adj₁₂ : F₁₂ ⊣ G₂₁
adj₂₃ : F₂₃ ⊣ G₃₂
adj₀₂ : F₀₂ ⊣ G₂₀
adj₁₃ : F₁₃ ⊣ G₃₁
adj₀₃ : F₀₃ ⊣ G₃₀
e₀₁₂ : G₂₁ ⋙ G₁₀ ≅ G₂₀
e₁₂₃ : G₃₂ ⋙ G₂₁ ≅ G₃₁
e₀₁₃ : G₃₁ ⋙ G₁₀ ≅ G₃₀
e₀₂₃ : G₃₂ ⋙ G₂₀ ≅ G₃₀
h : G₃₂.isoWhiskerLeft e₀₁₂ ≪≫ e₀₂₃ = (G₃₂.associator G₂₁ G₁₀).symm ≪≫ isoWhiskerRight e₁₂₃ G₁₀ ≪≫ e₀₁₃
⊢ F₀₁.isoWhiskerLeft (adj₁₂.leftAdjointCompIso adj₂₃ adj₁₃ e₁₂₃) ≪≫ adj₀₁.leftAdjointCompIso adj₁₃ adj₀₃ e₀₁₃ =
    (F₀₁.associator F₁₂ F₂₃).symm ≪≫
      isoWhiskerRight (adj₀₁.leftAdjointCompIso adj₁₂ adj₀₂ e₀₁₂) F₂₃ ≪≫ adj₀₂.leftAdjointCompIso adj₂₃ adj₀₃ e₀₂₃

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
E' : Type u₄
inst✝ : Category.{v₄, u₄} E'
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
M : PresheafOfModules R
X : Cᵒᵖ
x : ↑(M.obj (F.op.obj X))
⊢ (ConcreteCategory.hom (M.map (𝟙 (F.op.obj X)))) x =
    (ModuleCat.Hom.hom
        ((ModuleCat.restrictScalarsId' (RingCat.Hom.hom ((F.op ⋙ R).map (𝟙 X))) ⋯).inv.app
          (ModuleCat.of ↑((F.op ⋙ R).obj X) ↑(M.obj (F.op.obj X)))))
      x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.PushforwardZeroMonoidal

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
R : Dᵒᵖ ⥤ CommRingCat
x✝² x✝¹ x✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
⊢ (isoMk (fun x ↦ Iso.refl (((pushforward₀OfCommRingCat F R).obj x✝² ⊗ (pushforward₀OfCommRingCat F R).obj x✝¹).obj x))
            ⋯).hom ▷
        (pushforward₀OfCommRingCat F R).obj x✝ ≫
      (isoMk
            (fun x ↦
              Iso.refl
                (((pushforward₀OfCommRingCat F R).obj (x✝² ⊗ x✝¹) ⊗ (pushforward₀OfCommRingCat F R).obj x✝).obj x))
            ⋯).hom ≫
        (pushforward₀OfCommRingCat F R).map (α_ x✝² x✝¹ x✝).hom =
    (α_ ((pushforward₀OfCommRingCat F R).obj x✝²) ((pushforward₀OfCommRingCat F R).obj x✝¹)
          ((pushforward₀OfCommRingCat F R).obj x✝)).hom ≫
      (pushforward₀OfCommRingCat F R).obj x✝² ◁
          (isoMk
              (fun x ↦
                Iso.refl (((pushforward₀OfCommRingCat F R).obj x✝¹ ⊗ (pushforward₀OfCommRingCat F R).obj x✝).obj x))
              ⋯).hom ≫
        (isoMk
            (fun x ↦
              Iso.refl
                (((pushforward₀OfCommRingCat F R).obj x✝² ⊗ (pushforward₀OfCommRingCat F R).obj (x✝¹ ⊗ x✝)).obj x))
            ⋯).hom

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.PushforwardZeroMonoidal

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
R : Dᵒᵖ ⥤ CommRingCat
x✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
⊢ (λ_ ((pushforward₀OfCommRingCat F R).obj x✝)).hom =
    (Iso.refl (𝟙_ (PresheafOfModules ((F.op ⋙ R) ⋙ forget₂ CommRingCat RingCat)))).hom ▷
        (pushforward₀OfCommRingCat F R).obj x✝ ≫
      (isoMk
            (fun x ↦
              Iso.refl
                (((pushforward₀OfCommRingCat F R).obj (𝟙_ (PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat))) ⊗
                      (pushforward₀OfCommRingCat F R).obj x✝).obj
                  x))
            ⋯).hom ≫
        (pushforward₀OfCommRingCat F R).map (λ_ x✝).hom

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback

Goal state before:
pp: C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
S : Cᵒᵖ ⥤ RingCat
φ : S ⟶ F.op ⋙ R
⊢ pullbackObjIsDefined φ = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
E' : Type u₄
inst✝ : Category.{v₄, u₄} E'
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
M : PresheafOfModules R
X : Cᵒᵖ
⊢ M.map (F.op.map (𝟙 X)) =
    (ModuleCat.restrictScalarsId' (RingCat.Hom.hom ((F.op ⋙ R).map (𝟙 X))) ⋯).inv.app
      (ModuleCat.of ↑((F.op ⋙ R).obj X) ↑(M.obj (F.op.obj X)))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.PushforwardZeroMonoidal

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
R : Dᵒᵖ ⥤ CommRingCat
x✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
⊢ (ρ_ ((pushforward₀OfCommRingCat F R).obj x✝)).hom =
    (pushforward₀OfCommRingCat F R).obj x✝ ◁
        (Iso.refl (𝟙_ (PresheafOfModules ((F.op ⋙ R) ⋙ forget₂ CommRingCat RingCat)))).hom ≫
      (isoMk
            (fun x ↦
              Iso.refl
                (((pushforward₀OfCommRingCat F R).obj x✝ ⊗
                      (pushforward₀OfCommRingCat F R).obj
                        (𝟙_ (PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)))).obj
                  x))
            ⋯).hom ≫
        (pushforward₀OfCommRingCat F R).map (ρ_ x✝).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F✝ F' F'' : C ⥤ Type w
G✝ G' F G : Subfunctor F✝
U✝ V✝ : C
x✝¹ : U✝ ⟶ V✝
x✝ : F✝.obj U✝
⊢ x✝ ∈ F.obj U✝ ⊔ G.obj U✝ → x✝ ∈ ⇑(hom (F✝.map x✝¹)) ⁻¹' (F.obj V✝ ⊔ G.obj V✝)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' F'' : C ⥤ Type w
G G' x✝² x✝¹ : Subfunctor F
x✝ : C
⊢ x✝².obj x✝ ⊆ { obj := fun U ↦ x✝².obj U ⊔ x✝¹.obj U, map := ⋯ }.obj x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' F'' : C ⥤ Type w
G G' x✝² x✝¹ : Subfunctor F
x✝ : C
⊢ x✝¹.obj x✝ ⊆ { obj := fun U ↦ x✝².obj U ⊔ x✝¹.obj U, map := ⋯ }.obj x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F✝ F' F'' : C ⥤ Type w
G✝ G' F G H : Subfunctor F✝
h₁ : F ≤ H
h₂ : G ≤ H
U : C
⊢ { obj := fun U ↦ F.obj U ⊔ G.obj U, map := ⋯ }.obj U ⊆ H.obj U

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' F'' : C ⥤ Type w
G G' : Subfunctor F
S : Set (Subfunctor F)
U✝ V✝ : C
f : U✝ ⟶ V✝
x : F.obj U✝
hx : x ∈ sSup ((fun T ↦ T.obj U✝) '' S)
⊢ x ∈ ⇑(hom (F.map f)) ⁻¹' sSup ((fun T ↦ T.obj V✝) '' S)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' F'' : C ⥤ Type w
G G' : Subfunctor F
x✝⁴ : Set (Subfunctor F)
x✝³ : Subfunctor F
x✝² : x✝³ ∈ x✝⁴
x✝¹ : C
x✝ : F.obj x✝¹
⊢ x✝ ∈ x✝³.obj x✝¹ → x✝ ∈ { obj := fun U ↦ sSup ((fun T ↦ T.obj U) '' x✝⁴), map := ⋯ }.obj x✝¹

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' F'' : C ⥤ Type w
G G' : Subfunctor F
x✝³ : Set (Subfunctor F)
x✝² : Subfunctor F
x✝¹ : x✝² ∈ upperBounds x✝³
x✝ : C
⊢ { obj := fun U ↦ sSup ((fun T ↦ T.obj U) '' x✝³), map := ⋯ }.obj x✝ ⊆ x✝².obj x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' F'' : C ⥤ Type w
G G' : Subfunctor F
S : Set (Subfunctor F)
U✝ V✝ : C
f : U✝ ⟶ V✝
x : F.obj U✝
hx : x ∈ sInf ((fun T ↦ T.obj U✝) '' S)
⊢ x ∈ ⇑(hom (F.map f)) ⁻¹' sInf ((fun T ↦ T.obj V✝) '' S)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' F'' : C ⥤ Type w
G G' : Subfunctor F
x✝⁴ : Set (Subfunctor F)
x✝³ : Subfunctor F
x✝² : x✝³ ∈ x✝⁴
x✝¹ : C
x✝ : F.obj x✝¹
⊢ x✝ ∈ { obj := fun U ↦ sInf ((fun T ↦ T.obj U) '' x✝⁴), map := ⋯ }.obj x✝¹ → x✝ ∈ x✝³.obj x✝¹

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' F'' : C ⥤ Type w
G G' : Subfunctor F
x✝³ : Set (Subfunctor F)
x✝² : Subfunctor F
x✝¹ : x✝² ∈ lowerBounds x✝³
x✝ : C
⊢ x✝².obj x✝ ⊆ { obj := fun U ↦ sInf ((fun T ↦ T.obj U) '' x✝³), map := ⋯ }.obj x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' F'' : C ⥤ Type w
G G' : Subfunctor F
⊢ ∀ {U V : C} (i : U ⟶ V), ⊤ ⊆ ⇑(hom (F.map i)) ⁻¹' ⊤

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' F'' : C ⥤ Type w
G G' : Subfunctor F
⊢ ∀ {U V : C} (i : U ⟶ V), ⊥ ⊆ ⇑(hom (F.map i)) ⁻¹' ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
E' : Type u₄
inst✝ : Category.{v₄, u₄} E'
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
M : PresheafOfModules R
X✝ Y✝ Z✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
x : ↑(M.obj (F.op.obj X✝))
⊢ (ConcreteCategory.hom (M.map (F.op.map f ≫ F.op.map g))) x =
    (ModuleCat.Hom.hom
        (M.map (F.op.map f) ≫
          (ModuleCat.restrictScalars (RingCat.Hom.hom ((F.op ⋙ R).map f))).map (M.map (F.op.map g)) ≫
            (ModuleCat.restrictScalarsComp' (RingCat.Hom.hom ((F.op ⋙ R).map f)) (RingCat.Hom.hom ((F.op ⋙ R).map g))
                    (RingCat.Hom.hom ((F.op ⋙ R).map (f ≫ g))) ⋯).inv.app
              (ModuleCat.of ↑((F.op ⋙ R).obj Z✝) ↑(M.obj (F.op.obj Z✝)))))
      x

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
ι : Sort u_1
S : ι → Subfunctor F
U : C
⊢ (⨆ i, S i).obj U = ⋃ i, (S i).obj U

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
ι : Sort u_1
S : ι → Subfunctor F
U : C
⊢ (⨅ i, S i).obj U = ⋂ i, (S i).obj U

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
E' : Type u₄
inst✝ : Category.{v₄, u₄} E'
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
M : PresheafOfModules R
X✝ Y✝ Z✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ M.map (F.op.map (f ≫ g)) =
    M.map (F.op.map f) ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom ((F.op ⋙ R).map f))).map (M.map (F.op.map g)) ≫
        (ModuleCat.restrictScalarsComp' (RingCat.Hom.hom ((F.op ⋙ R).map f)) (RingCat.Hom.hom ((F.op ⋙ R).map g))
                (RingCat.Hom.hom ((F.op ⋙ R).map (f ≫ g))) ⋯).inv.app
          (ModuleCat.of ↑((F.op ⋙ R).obj Z✝) ↑(M.obj (F.op.obj Z✝)))

Tactic:
by

Goal state after: