Module: Mathlib.AlgebraicGeometry.Modules.Sheaf

Goal state before:
pp: case refine_2
X Y Z T : Scheme
M N K : X.Modules
φ✝ : M ⟶ N
U V : X.Opens
R S : CommRingCat
φ : R ⟶ S
⊢ ∀ {X Y : Sheaf (Opens.grothendieckTopology ↥(Spec S)) (ModuleCat ↑Γ(Spec S, ⊤))} (f : X ⟶ Y),
    (sheafCompose (Opens.grothendieckTopology ↥(Spec S))
                (ModuleCat.restrictScalars (CommRingCat.Hom.hom (Hom.appTop (Spec.map φ)))) ⋙
              TopCat.Sheaf.pushforward (ModuleCat ↑Γ(Spec R, ⊤)) (Spec.map φ).base ⋙
                sheafCompose (Opens.grothendieckTopology ↥(Spec R))
                  (ModuleCat.restrictScalars (CommRingCat.Hom.hom (ΓSpecIso R).inv))).map
          f ≫
        (ObjectProperty.isoMk (Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R)))
            (NatIso.ofComponents
              (fun U ↦
                (ModuleCat.restrictScalarsComp'App (CommRingCat.Hom.hom (ΓSpecIso R).inv)
                      (CommRingCat.Hom.hom (Hom.appTop (Spec.map φ)))
                      ((CommRingCat.Hom.hom (ΓSpecIso S).inv).comp (CommRingCat.Hom.hom φ)) ⋯
                      (((sheafToPresheaf (Opens.grothendieckTopology ↥(Spec S)) (ModuleCat ↑Γ(Spec S, ⊤))).obj Y).obj
                        ((Opens.map (Spec.map φ).base).op.obj U))).symm ≪≫
                  (ModuleCat.restrictScalarsComp (CommRingCat.Hom.hom φ) (CommRingCat.Hom.hom (ΓSpecIso S).inv)).app
                    (((sheafToPresheaf (Opens.grothendieckTopology ↥(Spec S)) (ModuleCat ↑Γ(Spec S, ⊤))).obj Y).obj
                      ((Opens.map (Spec.map φ).base).op.obj U)))
              ⋯)).hom =
      (ObjectProperty.isoMk (Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R)))
            (NatIso.ofComponents
              (fun U ↦
                (ModuleCat.restrictScalarsComp'App (CommRingCat.Hom.hom (ΓSpecIso R).inv)
                      (CommRingCat.Hom.hom (Hom.appTop (Spec.map φ)))
                      ((CommRingCat.Hom.hom (ΓSpecIso S).inv).comp (CommRingCat.Hom.hom φ)) ⋯
                      (((sheafToPresheaf (Opens.grothendieckTopology ↥(Spec S)) (ModuleCat ↑Γ(Spec S, ⊤))).obj X).obj
                        ((Opens.map (Spec.map φ).base).op.obj U))).symm ≪≫
                  (ModuleCat.restrictScalarsComp (CommRingCat.Hom.hom φ) (CommRingCat.Hom.hom (ΓSpecIso S).inv)).app
                    (((sheafToPresheaf (Opens.grothendieckTopology ↥(Spec S)) (ModuleCat ↑Γ(Spec S, ⊤))).obj X).obj
                      ((Opens.map (Spec.map φ).base).op.obj U)))
              ⋯)).hom ≫
        (sheafCompose (Opens.grothendieckTopology ↥(Spec S))
                (ModuleCat.restrictScalars (CommRingCat.Hom.hom (ΓSpecIso S).inv)) ⋙
              TopCat.Sheaf.pushforward (ModuleCat ↑S) (Spec.map φ).base ⋙
                sheafCompose (Opens.grothendieckTopology ↥(Spec R))
                  (ModuleCat.restrictScalars (CommRingCat.Hom.hom φ))).map
          f

Tactic:
·

Goal state after:
case refine_2
X Y Z T : Scheme
M N K : X.Modules
φ✝ : M ⟶ N
U V : X.Opens
R S : CommRingCat
φ : R ⟶ S
⊢ ∀ {X Y : Sheaf (Opens.grothendieckTopology ↥(Spec S)) (ModuleCat ↑Γ(Spec S, ⊤))} (f : X ⟶ Y),
    (sheafCompose (Opens.grothendieckTopology ↥(Spec S))
                (ModuleCat.restrictScalars (CommRingCat.Hom.hom (Hom.appTop (Spec.map φ)))) ⋙
              TopCat.Sheaf.pushforward (ModuleCat ↑Γ(Spec R, ⊤)) (Spec.map φ).base ⋙
                sheafCompose (Opens.grothendieckTopology ↥(Spec R))
                  (ModuleCat.restrictScalars (CommRingCat.Hom.hom (ΓSpecIso R).inv))).map
          f ≫
        (ObjectProperty.isoMk (Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R)))
            (NatIso.ofComponents
              (fun U ↦
                (ModuleCat.restrictScalarsComp'App (CommRingCat.Hom.hom (ΓSpecIso R).inv)
                      (CommRingCat.Hom.hom (Hom.appTop (Spec.map φ)))
                      ((CommRingCat.Hom.hom (ΓSpecIso S).inv).comp (CommRingCat.Hom.hom φ)) ⋯
                      (((sheafToPresheaf (Opens.grothendieckTopology ↥(Spec S)) (ModuleCat ↑Γ(Spec S, ⊤))).obj Y).obj
                        ((Opens.map (Spec.map φ).base).op.obj U))).symm ≪≫
                  (ModuleCat.restrictScalarsComp (CommRingCat.Hom.hom φ) (CommRingCat.Hom.hom (ΓSpecIso S).inv)).app
                    (((sheafToPresheaf (Opens.grothendieckTopology ↥(Spec S)) (ModuleCat ↑Γ(Spec S, ⊤))).obj Y).obj
                      ((Opens.map (Spec.map φ).base).op.obj U)))
              ⋯)).hom =
      (ObjectProperty.isoMk (Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R)))
            (NatIso.ofComponents
              (fun U ↦
                (ModuleCat.restrictScalarsComp'App (CommRingCat.Hom.hom (ΓSpecIso R).inv)
                      (CommRingCat.Hom.hom (Hom.appTop (Spec.map φ)))
                      ((CommRingCat.Hom.hom (ΓSpecIso S).inv).comp (CommRingCat.Hom.hom φ)) ⋯
                      (((sheafToPresheaf (Opens.grothendieckTopology ↥(Spec S)) (ModuleCat ↑Γ(Spec S, ⊤))).obj X).obj
                        ((Opens.map (Spec.map φ).base).op.obj U))).symm ≪≫
                  (ModuleCat.restrictScalarsComp (CommRingCat.Hom.hom φ) (CommRingCat.Hom.hom (ΓSpecIso S).inv)).app
                    (((sheafToPresheaf (Opens.grothendieckTopology ↥(Spec S)) (ModuleCat ↑Γ(Spec S, ⊤))).obj X).obj
                      ((Opens.map (Spec.map φ).base).op.obj U)))
              ⋯)).hom ≫
        (sheafCompose (Opens.grothendieckTopology ↥(Spec S))
                (ModuleCat.restrictScalars (CommRingCat.Hom.hom (ΓSpecIso S).inv)) ⋙
              TopCat.Sheaf.pushforward (ModuleCat ↑S) (Spec.map φ).base ⋙
                sheafCompose (Opens.grothendieckTopology ↥(Spec R))
                  (ModuleCat.restrictScalars (CommRingCat.Hom.hom φ))).map
          f