Module: Mathlib.Algebra.Category.ModuleCat.Stalk

Goal state before:
pp: C : Type u_1
inst✝² : SmallCategory C
inst✝¹ : IsFiltered C
R : C ⥤ RingCat
M : C ⥤ Ab
inst✝ : (i : C) → Module ↑(R.obj i) ↑(M.obj i)
H :
  ∀ {i j : C} (f : i ⟶ j) (r : ↑(R.obj i)) (m : ↑(M.obj i)),
    (ConcreteCategory.hom (M.map f)) (r • m) = (ConcreteCategory.hom (R.map f)) r • (ConcreteCategory.hom (M.map f)) m
r : ↑(RingCat.FilteredColimits.colimit R)
m n : ↑(AddCommGrpCat.FilteredColimits.colimit M)
U : C
a : (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj U
V₁ : C
b₁ : (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).obj V₁
V₂ : C
b₂ : (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).obj V₂
s : C
α : IsFiltered.max (IsFiltered.max U V₁) (IsFiltered.max U V₂) ⟶ s
β : IsFiltered.max U (IsFiltered.max V₁ V₂) ⟶ s
h₁ :
  (leftToMax U V₁ ≫ leftToMax (IsFiltered.max U V₁) (IsFiltered.max U V₂)) ≫ α = leftToMax U (IsFiltered.max V₁ V₂) ≫ β
h₂ :
  (leftToMax U V₂ ≫ rightToMax (IsFiltered.max U V₁) (IsFiltered.max U V₂)) ≫ α = leftToMax U (IsFiltered.max V₁ V₂) ≫ β
h₃ :
  (rightToMax U V₁ ≫ leftToMax (IsFiltered.max U V₁) (IsFiltered.max U V₂)) ≫ α =
    (leftToMax V₁ V₂ ≫ rightToMax U (IsFiltered.max V₁ V₂)) ≫ β
h₄ :
  (rightToMax U V₂ ≫ rightToMax (IsFiltered.max U V₁) (IsFiltered.max U V₂)) ≫ α =
    (rightToMax V₁ V₂ ≫ rightToMax U (IsFiltered.max V₁ V₂)) ≫ β
⊢ Quot.mk (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨U, a⟩ •
      (Quot.mk (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).ColimitTypeRel
          ⟨V₁, b₁⟩ +
        Quot.mk
          (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).ColimitTypeRel
          ⟨V₂, b₂⟩) =
    Quot.mk (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨U, a⟩ •
        Quot.mk
          (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).ColimitTypeRel
          ⟨V₁, b₁⟩ +
      Quot.mk (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨U, a⟩ •
        Quot.mk
          (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).ColimitTypeRel
          ⟨V₂, b₂⟩

Tactic:
refine Functor.ιColimitType_eq_of_map_eq_map _ _ _ β α ?_

Goal state after:
C : Type u_1
inst✝² : SmallCategory C
inst✝¹ : IsFiltered C
R : C ⥤ RingCat
M : C ⥤ Ab
inst✝ : (i : C) → Module ↑(R.obj i) ↑(M.obj i)
H :
  ∀ {i j : C} (f : i ⟶ j) (r : ↑(R.obj i)) (m : ↑(M.obj i)),
    (ConcreteCategory.hom (M.map f)) (r • m) = (ConcreteCategory.hom (R.map f)) r • (ConcreteCategory.hom (M.map f)) m
r : ↑(RingCat.FilteredColimits.colimit R)
m n : ↑(AddCommGrpCat.FilteredColimits.colimit M)
U : C
a : (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj U
V₁ : C
b₁ : (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).obj V₁
V₂ : C
b₂ : (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).obj V₂
s : C
α : IsFiltered.max (IsFiltered.max U V₁) (IsFiltered.max U V₂) ⟶ s
β : IsFiltered.max U (IsFiltered.max V₁ V₂) ⟶ s
h₁ :
  (leftToMax U V₁ ≫ leftToMax (IsFiltered.max U V₁) (IsFiltered.max U V₂)) ≫ α = leftToMax U (IsFiltered.max V₁ V₂) ≫ β
h₂ :
  (leftToMax U V₂ ≫ rightToMax (IsFiltered.max U V₁) (IsFiltered.max U V₂)) ≫ α = leftToMax U (IsFiltered.max V₁ V₂) ≫ β
h₃ :
  (rightToMax U V₁ ≫ leftToMax (IsFiltered.max U V₁) (IsFiltered.max U V₂)) ≫ α =
    (leftToMax V₁ V₂ ≫ rightToMax U (IsFiltered.max V₁ V₂)) ≫ β
h₄ :
  (rightToMax U V₂ ≫ rightToMax (IsFiltered.max U V₁) (IsFiltered.max U V₂)) ≫ α =
    (rightToMax V₁ V₂ ≫ rightToMax U (IsFiltered.max V₁ V₂)) ≫ β
⊢ (ConcreteCategory.hom ((M ⋙ forget Ab).map β))
      ((ConcreteCategory.hom
            (R.map
              (leftToMax ⟨U, a⟩.fst
                ⟨⟨IsFiltered.max ⟨V₁, b₁⟩.fst ⟨V₂, b₂⟩.fst,
                        (ConcreteCategory.hom
                              (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat).map
                                (leftToMax ⟨V₁, b₁⟩.fst ⟨V₂, b₂⟩.fst)))
                            ⟨V₁, b₁⟩.snd +
                          (ConcreteCategory.hom
                              (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat).map
                                (rightToMax ⟨V₁, b₁⟩.fst ⟨V₂, b₂⟩.fst)))
                            ⟨V₂, b₂⟩.snd⟩.fst,
                    ⟨IsFiltered.max ⟨V₁, b₁⟩.fst ⟨V₂, b₂⟩.fst,
                        (ConcreteCategory.hom
                              (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat).map
                                (leftToMax ⟨V₁, b₁⟩.fst ⟨V₂, b₂⟩.fst)))
                            ⟨V₁, b₁⟩.snd +
                          (ConcreteCategory.hom
                              (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat).map
                                (rightToMax ⟨V₁, b₁⟩.fst ⟨V₂, b₂⟩.fst)))
                            ⟨V₂, b₂⟩.snd⟩.snd⟩.fst)))
          ⟨U, a⟩.snd •
        (ConcreteCategory.hom
            (M.map
              (rightToMax ⟨U, a⟩.fst
                ⟨⟨IsFiltered.max ⟨V₁, b₁⟩.fst ⟨V₂, b₂⟩.fst,
                        (ConcreteCategory.hom
                              (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat).map
                                (leftToMax ⟨V₁, b₁⟩.fst ⟨V₂, b₂⟩.fst)))
                            ⟨V₁, b₁⟩.snd +
                          (ConcreteCategory.hom
                              (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat).map
                                (rightToMax ⟨V₁, b₁⟩.fst ⟨V₂, b₂⟩.fst)))
                            ⟨V₂, b₂⟩.snd⟩.fst,
                    ⟨IsFiltered.max ⟨V₁, b₁⟩.fst ⟨V₂, b₂⟩.fst,
                        (ConcreteCategory.hom
                              (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat).map
                                (leftToMax ⟨V₁, b₁⟩.fst ⟨V₂, b₂⟩.fst)))
                            ⟨V₁, b₁⟩.snd +
                          (ConcreteCategory.hom
                              (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat).map
                                (rightToMax ⟨V₁, b₁⟩.fst ⟨V₂, b₂⟩.fst)))
                            ⟨V₂, b₂⟩.snd⟩.snd⟩.fst)))
          ⟨⟨IsFiltered.max ⟨V₁, b₁⟩.fst ⟨V₂, b₂⟩.fst,
                  (ConcreteCategory.hom
                        (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat).map
                          (leftToMax ⟨V₁, b₁⟩.fst ⟨V₂, b₂⟩.fst)))
                      ⟨V₁, b₁⟩.snd +
                    (ConcreteCategory.hom
                        (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat).map
                          (rightToMax ⟨V₁, b₁⟩.fst ⟨V₂, b₂⟩.fst)))
                      ⟨V₂, b₂⟩.snd⟩.fst,
              ⟨IsFiltered.max ⟨V₁, b₁⟩.fst ⟨V₂, b₂⟩.fst,
                  (ConcreteCategory.hom
                        (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat).map
                          (leftToMax ⟨V₁, b₁⟩.fst ⟨V₂, b₂⟩.fst)))
                      ⟨V₁, b₁⟩.snd +
                    (ConcreteCategory.hom
                        (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat).map
                          (rightToMax ⟨V₁, b₁⟩.fst ⟨V₂, b₂⟩.fst)))
                      ⟨V₂, b₂⟩.snd⟩.snd⟩.snd) =
    (ConcreteCategory.hom ((M ⋙ forget Ab).map α))
      ⟨IsFiltered.max
            ⟨IsFiltered.max ⟨U, a⟩.fst ⟨V₁, b₁⟩.fst,
                (ConcreteCategory.hom (R.map (leftToMax ⟨U, a⟩.fst ⟨V₁, b₁⟩.fst))) ⟨U, a⟩.snd •
                  (ConcreteCategory.hom (M.map (rightToMax ⟨U, a⟩.fst ⟨V₁, b₁⟩.fst))) ⟨V₁, b₁⟩.snd⟩.fst
            ⟨IsFiltered.max ⟨U, a⟩.fst ⟨V₂, b₂⟩.fst,
                (ConcreteCategory.hom (R.map (leftToMax ⟨U, a⟩.fst ⟨V₂, b₂⟩.fst))) ⟨U, a⟩.snd •
                  (ConcreteCategory.hom (M.map (rightToMax ⟨U, a⟩.fst ⟨V₂, b₂⟩.fst))) ⟨V₂, b₂⟩.snd⟩.fst,
          (ConcreteCategory.hom
                (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat).map
                  (leftToMax
                    ⟨IsFiltered.max ⟨U, a⟩.fst ⟨V₁, b₁⟩.fst,
                        (ConcreteCategory.hom (R.map (leftToMax ⟨U, a⟩.fst ⟨V₁, b₁⟩.fst))) ⟨U, a⟩.snd •
                          (ConcreteCategory.hom (M.map (rightToMax ⟨U, a⟩.fst ⟨V₁, b₁⟩.fst))) ⟨V₁, b₁⟩.snd⟩.fst
                    ⟨IsFiltered.max ⟨U, a⟩.fst ⟨V₂, b₂⟩.fst,
                        (ConcreteCategory.hom (R.map (leftToMax ⟨U, a⟩.fst ⟨V₂, b₂⟩.fst))) ⟨U, a⟩.snd •
                          (ConcreteCategory.hom (M.map (rightToMax ⟨U, a⟩.fst ⟨V₂, b₂⟩.fst))) ⟨V₂, b₂⟩.snd⟩.fst)))
              ⟨IsFiltered.max ⟨U, a⟩.fst ⟨V₁, b₁⟩.fst,
                  (ConcreteCategory.hom (R.map (leftToMax ⟨U, a⟩.fst ⟨V₁, b₁⟩.fst))) ⟨U, a⟩.snd •
                    (ConcreteCategory.hom (M.map (rightToMax ⟨U, a⟩.fst ⟨V₁, b₁⟩.fst))) ⟨V₁, b₁⟩.snd⟩.snd +
            (ConcreteCategory.hom
                (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat).map
                  (rightToMax
                    ⟨IsFiltered.max ⟨U, a⟩.fst ⟨V₁, b₁⟩.fst,
                        (ConcreteCategory.hom (R.map (leftToMax ⟨U, a⟩.fst ⟨V₁, b₁⟩.fst))) ⟨U, a⟩.snd •
                          (ConcreteCategory.hom (M.map (rightToMax ⟨U, a⟩.fst ⟨V₁, b₁⟩.fst))) ⟨V₁, b₁⟩.snd⟩.fst
                    ⟨IsFiltered.max ⟨U, a⟩.fst ⟨V₂, b₂⟩.fst,
                        (ConcreteCategory.hom (R.map (leftToMax ⟨U, a⟩.fst ⟨V₂, b₂⟩.fst))) ⟨U, a⟩.snd •
                          (ConcreteCategory.hom (M.map (rightToMax ⟨U, a⟩.fst ⟨V₂, b₂⟩.fst))) ⟨V₂, b₂⟩.snd⟩.fst)))
              ⟨IsFiltered.max ⟨U, a⟩.fst ⟨V₂, b₂⟩.fst,
                  (ConcreteCategory.hom (R.map (leftToMax ⟨U, a⟩.fst ⟨V₂, b₂⟩.fst))) ⟨U, a⟩.snd •
                    (ConcreteCategory.hom (M.map (rightToMax ⟨U, a⟩.fst ⟨V₂, b₂⟩.fst))) ⟨V₂, b₂⟩.snd⟩.snd⟩.snd