mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Spec.map (X.presheaf.map (homOfLE ⋯).op) = Spec.map (X.presheaf.map (homOfLE ⋯).op)

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
s : Set ↑(X.presheaf.obj (op ⊤))
this : ∀ i ∈ s, (↑(X.toRingedSpace.basicOpen i))ᶜ = ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' (basicOpen i).carrierᶜ
⊢ ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' zeroLocus s =
    ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' zeroLocus (⋃ i ∈ s, {i})

Tactic:
]

Goal state after:
X : LocallyRingedSpace
s : Set ↑(X.presheaf.obj (op ⊤))
this : ∀ i ∈ s, (↑(X.toRingedSpace.basicOpen i))ᶜ = ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' (basicOpen i).carrierᶜ
⊢ ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' zeroLocus s =
    ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' zeroLocus (⋃ i ∈ s, {i})
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
x : ↑(PrimeSpectrum.Top R)
hxU : x ∈ U
⊢ CommRingCat.ofHom (algebraMap R ((structureSheafInType R R).obj.obj (op U))) ≫
      (structurePresheafInCommRingCat R).germ U x hxU =
    CommRingCat.ofHom (algebraMap R ((structureSheafInType R R).obj.obj (op ⊤))) ≫
      (structurePresheafInCommRingCat R).map (homOfLE ⋯).op ≫ (structurePresheafInCommRingCat R).germ U x hxU

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
x : ↑(PrimeSpectrum.Top R)
hxU : x ∈ U
⊢ CommRingCat.ofHom (algebraMap R ((structureSheafInType R R).obj.obj (op U))) ≫
      (structurePresheafInCommRingCat R).germ U x hxU =
    CommRingCat.ofHom (algebraMap R ((structureSheafInType R R).obj.obj (op ⊤))) ≫
      (structurePresheafInCommRingCat R).map (homOfLE ⋯).op ≫ (structurePresheafInCommRingCat R).germ U x hxU
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
U : Opens ↑(PrimeSpectrum.Top R)
x : ↑(PrimeSpectrum.Top R)
hxU : x ∈ U
r : R
m : (structureSheafInType R M).obj.obj (op U)
⊢ (↑(AddCommGrpCat.Hom.hom (Presheaf.germ (moduleStructurePresheaf R M).presheaf U x hxU))).toFun (r • m) =
    (ConcreteCategory.hom ((structurePresheafInCommRingCat R).germ U x hxU))
        ((algebraMap R ((structureSheafInType R R).obj.obj (op U))) ((RingHom.id R) r)) •
      (ConcreteCategory.hom (Presheaf.germ (moduleStructurePresheaf R M).presheaf U x hxU)) m

Tactic:
]

Goal state after:
R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
U : Opens ↑(PrimeSpectrum.Top R)
x : ↑(PrimeSpectrum.Top R)
hxU : x ∈ U
r : R
m : (structureSheafInType R M).obj.obj (op U)
⊢ (↑(AddCommGrpCat.Hom.hom (Presheaf.germ (moduleStructurePresheaf R M).presheaf U x hxU))).toFun (r • m) =
    (ConcreteCategory.hom ((structurePresheafInCommRingCat R).germ U x hxU))
        ((algebraMap R ((structureSheafInType R R).obj.obj (op U))) ((RingHom.id R) r)) •
      (ConcreteCategory.hom (Presheaf.germ (moduleStructurePresheaf R M).presheaf U x hxU)) m
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
R : CommRingCat
f : R ⟶ Γ.obj (op X)
β : X ⟶ Spec.locallyRingedSpaceObj R
w : X.toΓSpec.base ≫ (Spec.locallyRingedSpaceMap f).base = β.base
h :
  ∀ (r : ↑R),
    f ≫ X.presheaf.map (homOfLE ⋯).op =
      CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op (basicOpen r)))) ≫
        β.c.app (op (basicOpen r))
r : ↑R
U : Opens (PrimeSpectrum ↑R) := basicOpen r
⊢ (CommRingCat.ofHom (CommRingCat.Hom.hom f) ≫
        CommRingCat.ofHom
            (algebraMap ↑(Γ.obj (op X))
              ↑((structureSheaf ↑(Γ.obj (op X))).obj.obj
                  (op
                    ((Opens.comap { toFun := PrimeSpectrum.comap (CommRingCat.Hom.hom f), continuous_toFun := ⋯ })
                      U)))) ≫
          { hom := X.toΓSpecSheafedSpace.hom }.hom.c.app
            (op ((Opens.map { hom := (Spec.sheafedSpaceMap f).hom }.hom.base).obj (unop (op U))))) ≫
      (forgetToSheafedSpace.obj X).presheaf.map (eqToHom ⋯) =
    CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op U))) ≫
      (forgetToSheafedSpace.map β).hom.c.app (op U)

Tactic:
]

Goal state after:
X : LocallyRingedSpace
R : CommRingCat
f : R ⟶ Γ.obj (op X)
β : X ⟶ Spec.locallyRingedSpaceObj R
w : X.toΓSpec.base ≫ (Spec.locallyRingedSpaceMap f).base = β.base
h :
  ∀ (r : ↑R),
    f ≫ X.presheaf.map (homOfLE ⋯).op =
      CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op (basicOpen r)))) ≫
        β.c.app (op (basicOpen r))
r : ↑R
U : Opens (PrimeSpectrum ↑R) := basicOpen r
⊢ (CommRingCat.ofHom (CommRingCat.Hom.hom f) ≫
        CommRingCat.ofHom
            (algebraMap ↑(Γ.obj (op X))
              ↑((structureSheaf ↑(Γ.obj (op X))).obj.obj
                  (op
                    ((Opens.comap { toFun := PrimeSpectrum.comap (CommRingCat.Hom.hom f), continuous_toFun := ⋯ })
                      U)))) ≫
          { hom := X.toΓSpecSheafedSpace.hom }.hom.c.app
            (op ((Opens.map { hom := (Spec.sheafedSpaceMap f).hom }.hom.base).obj (unop (op U))))) ≫
      (forgetToSheafedSpace.obj X).presheaf.map (eqToHom ⋯) =
    CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op U))) ≫
      (forgetToSheafedSpace.map β).hom.c.app (op U)
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
f : op U ⟶ op V
this✝ : IsAffine ↑U
this : IsAffine ↑V
⊢ Spec.map (X.presheaf.map ((eqToHom ⋯).op ≫ f)) ≫ (↑U).isoSpec.inv ≫ U.ι =
    Spec.map (X.presheaf.map ((homOfLE ⋯).op ≫ (eqToHom ⋯).op)) ≫ (↑U).isoSpec.inv ≫ U.ι

Tactic:
]

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
f : op U ⟶ op V
this✝ : IsAffine ↑U
this : IsAffine ↑V
⊢ Spec.map (X.presheaf.map ((eqToHom ⋯).op ≫ f)) ≫ (↑U).isoSpec.inv ≫ U.ι =
    Spec.map (X.presheaf.map ((homOfLE ⋯).op ≫ (eqToHom ⋯).op)) ≫ (↑U).isoSpec.inv ≫ U.ι
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
R : CommRingCat
f : R ⟶ Γ.obj (op X)
β : X ⟶ Spec.locallyRingedSpaceObj R
w : X.toΓSpec.base ≫ (Spec.locallyRingedSpaceMap f).base = β.base
h :
  ∀ (r : ↑R),
    f ≫ X.presheaf.map (homOfLE ⋯).op =
      CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op (basicOpen r)))) ≫
        β.c.app (op (basicOpen r))
r : ↑R
U : Opens (PrimeSpectrum ↑R) := basicOpen r
⊢ CommRingCat.ofHom (CommRingCat.Hom.hom f) ≫
      (CommRingCat.ofHom
            (algebraMap ↑(X.presheaf.obj (op ⊤))
              ↑((structureSheaf ↑(X.presheaf.obj (op ⊤))).obj.obj
                  (op
                    ((Opens.comap { toFun := PrimeSpectrum.comap (CommRingCat.Hom.hom f), continuous_toFun := ⋯ })
                      U)))) ≫
          X.toΓSpecSheafedSpace.hom.c.app (op ((Opens.map (Spec.sheafedSpaceMap f).hom.base).obj U))) ≫
        (forgetToSheafedSpace.obj X).presheaf.map (eqToHom ⋯) =
    CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op U))) ≫
      (forgetToSheafedSpace.map β).hom.c.app (op U)

Tactic:
]

Goal state after:
X : LocallyRingedSpace
R : CommRingCat
f : R ⟶ Γ.obj (op X)
β : X ⟶ Spec.locallyRingedSpaceObj R
w : X.toΓSpec.base ≫ (Spec.locallyRingedSpaceMap f).base = β.base
h :
  ∀ (r : ↑R),
    f ≫ X.presheaf.map (homOfLE ⋯).op =
      CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op (basicOpen r)))) ≫
        β.c.app (op (basicOpen r))
r : ↑R
U : Opens (PrimeSpectrum ↑R) := basicOpen r
⊢ CommRingCat.ofHom (CommRingCat.Hom.hom f) ≫
      (CommRingCat.ofHom
            (algebraMap ↑(X.presheaf.obj (op ⊤))
              ↑((structureSheaf ↑(X.presheaf.obj (op ⊤))).obj.obj
                  (op
                    ((Opens.comap { toFun := PrimeSpectrum.comap (CommRingCat.Hom.hom f), continuous_toFun := ⋯ })
                      U)))) ≫
          X.toΓSpecSheafedSpace.hom.c.app (op ((Opens.map (Spec.sheafedSpaceMap f).hom.base).obj U))) ≫
        (forgetToSheafedSpace.obj X).presheaf.map (eqToHom ⋯) =
    CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op U))) ≫
      (forgetToSheafedSpace.map β).hom.c.app (op U)
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
R : CommRingCat
f : R ⟶ Γ.obj (op X)
β : X ⟶ Spec.locallyRingedSpaceObj R
w : X.toΓSpec.base ≫ (Spec.locallyRingedSpaceMap f).base = β.base
h :
  ∀ (r : ↑R),
    f ≫ X.presheaf.map (homOfLE ⋯).op =
      CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op (basicOpen r)))) ≫
        β.c.app (op (basicOpen r))
r : ↑R
U : Opens (PrimeSpectrum ↑R) := basicOpen r
⊢ CommRingCat.ofHom (CommRingCat.Hom.hom f) ≫
      X.presheaf.map ((X.toΓSpecMapBasicOpen ((CommRingCat.Hom.hom f) r)).leTop.op ≫ eqToHom ⋯) =
    CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op U))) ≫
      (forgetToSheafedSpace.map β).hom.c.app (op U)

Tactic:
]

Goal state after:
X : LocallyRingedSpace
R : CommRingCat
f : R ⟶ Γ.obj (op X)
β : X ⟶ Spec.locallyRingedSpaceObj R
w : X.toΓSpec.base ≫ (Spec.locallyRingedSpaceMap f).base = β.base
h :
  ∀ (r : ↑R),
    f ≫ X.presheaf.map (homOfLE ⋯).op =
      CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op (basicOpen r)))) ≫
        β.c.app (op (basicOpen r))
r : ↑R
U : Opens (PrimeSpectrum ↑R) := basicOpen r
⊢ CommRingCat.ofHom (CommRingCat.Hom.hom f) ≫
      X.presheaf.map ((X.toΓSpecMapBasicOpen ((CommRingCat.Hom.hom f) r)).leTop.op ≫ eqToHom ⋯) =
    CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op U))) ≫
      (forgetToSheafedSpace.map β).hom.c.app (op U)
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ↑(PrimeSpectrum.Top R)
r : R
α : Presheaf.stalk (moduleStructurePresheaf R M).presheaf x ≅
  (forget₂ (ModuleCat R) Ab).obj ((structurePresheafInModuleCat R M).stalk x) :=
  Limits.colimit.isoColimitCocone
    {
      cocone :=
        (forget₂ (ModuleCat R) Ab).mapCocone
          (Limits.colimit.cocone ((OpenNhds.inclusion x).op ⋙ structurePresheafInModuleCat R M)),
      isColimit :=
        Limits.isColimitOfPreserves (forget₂ (ModuleCat R) Ab)
          (Limits.colimit.isColimit ((OpenNhds.inclusion x).op ⋙ structurePresheafInModuleCat R M)) }
U : Opens ↑(PrimeSpectrum.Top R)
hxU : x ∈ U
s : ToType ((moduleStructurePresheaf R M).presheaf.obj (op U))
this✝ :
  Presheaf.germ (moduleStructurePresheaf R M).presheaf U x hxU ≫ α.hom =
    (forget₂ (ModuleCat R) Ab).map ((structurePresheafInModuleCat R M).germ U x hxU)
this :
  ∀ (m : ↑((moduleStructurePresheaf R M).presheaf.obj (op U))),
    (ConcreteCategory.hom α.hom)
        ((ConcreteCategory.hom (Presheaf.germ (moduleStructurePresheaf R M).presheaf U x hxU)) m) =
      (ConcreteCategory.hom ((structurePresheafInModuleCat R M).germ U x hxU)) m
⊢ (ConcreteCategory.hom ((structurePresheafInModuleCat R M).germ U x hxU)) (r • s) =
    r • (ConcreteCategory.hom ((structurePresheafInModuleCat R M).germ U x hxU)) s

Tactic:
]

Goal state after:
R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ↑(PrimeSpectrum.Top R)
r : R
α : Presheaf.stalk (moduleStructurePresheaf R M).presheaf x ≅
  (forget₂ (ModuleCat R) Ab).obj ((structurePresheafInModuleCat R M).stalk x) :=
  Limits.colimit.isoColimitCocone
    {
      cocone :=
        (forget₂ (ModuleCat R) Ab).mapCocone
          (Limits.colimit.cocone ((OpenNhds.inclusion x).op ⋙ structurePresheafInModuleCat R M)),
      isColimit :=
        Limits.isColimitOfPreserves (forget₂ (ModuleCat R) Ab)
          (Limits.colimit.isColimit ((OpenNhds.inclusion x).op ⋙ structurePresheafInModuleCat R M)) }
U : Opens ↑(PrimeSpectrum.Top R)
hxU : x ∈ U
s : ToType ((moduleStructurePresheaf R M).presheaf.obj (op U))
this✝ :
  Presheaf.germ (moduleStructurePresheaf R M).presheaf U x hxU ≫ α.hom =
    (forget₂ (ModuleCat R) Ab).map ((structurePresheafInModuleCat R M).germ U x hxU)
this :
  ∀ (m : ↑((moduleStructurePresheaf R M).presheaf.obj (op U))),
    (ConcreteCategory.hom α.hom)
        ((ConcreteCategory.hom (Presheaf.germ (moduleStructurePresheaf R M).presheaf U x hxU)) m) =
      (ConcreteCategory.hom ((structurePresheafInModuleCat R M).germ U x hxU)) m
⊢ (ConcreteCategory.hom ((structurePresheafInModuleCat R M).germ U x hxU)) (r • s) =
    r • (ConcreteCategory.hom ((structurePresheafInModuleCat R M).germ U x hxU)) s
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
V : X.Opens
U : Y.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
i : V ≤ f ⁻¹ᵁ U
this : IsAffine ↑U
⊢ Spec.map (Y.presheaf.map (eqToHom ⋯).op ≫ Scheme.Hom.appLE f U V i) ≫ (↑U).isoSpec.inv ≫ U.ι =
    Spec.map
        (((Scheme.Hom.appLE f (U.ι ''ᵁ ⊤) (f ⁻¹ᵁ U.ι ''ᵁ ⊤) ⋯ ≫ X.presheaf.map (eqToHom ⋯).op) ≫
            X.presheaf.map (homOfLE ⋯).op) ≫
          X.presheaf.map (eqToHom ⋯).op) ≫
      (↑U).isoSpec.inv ≫ U.ι

Tactic:
Scheme.Hom.appLE_map,

Goal state after:
X Y : Scheme
f : X ⟶ Y
V : X.Opens
U : Y.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
i : V ≤ f ⁻¹ᵁ U
this : IsAffine ↑U
⊢ Spec.map (Y.presheaf.map (eqToHom ⋯).op ≫ Scheme.Hom.appLE f U V i) ≫ (↑U).isoSpec.inv ≫ U.ι =
    Spec.map
        ((Scheme.Hom.appLE f (U.ι ''ᵁ ⊤) ((f ⁻¹ᵁ U).ι ''ᵁ (f ∣_ U) ⁻¹ᵁ ⊤) ⋯ ≫ X.presheaf.map (homOfLE ⋯).op) ≫
          X.presheaf.map (eqToHom ⋯).op) ≫
      (↑U).isoSpec.inv ≫ U.ι
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
V : X.Opens
U : Y.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
i : V ≤ f ⁻¹ᵁ U
this : IsAffine ↑U
⊢ Spec.map (Y.presheaf.map (eqToHom ⋯).op ≫ Scheme.Hom.appLE f U V i) ≫ (↑U).isoSpec.inv ≫ U.ι =
    Spec.map
        ((Scheme.Hom.appLE f (U.ι ''ᵁ ⊤) ((f ⁻¹ᵁ U).ι ''ᵁ (f ∣_ U) ⁻¹ᵁ ⊤) ⋯ ≫ X.presheaf.map (homOfLE ⋯).op) ≫
          X.presheaf.map (eqToHom ⋯).op) ≫
      (↑U).isoSpec.inv ≫ U.ι

Tactic:
Scheme.Hom.appLE_map,

Goal state after:
X Y : Scheme
f : X ⟶ Y
V : X.Opens
U : Y.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
i : V ≤ f ⁻¹ᵁ U
this : IsAffine ↑U
⊢ Spec.map (Y.presheaf.map (eqToHom ⋯).op ≫ Scheme.Hom.appLE f U V i) ≫ (↑U).isoSpec.inv ≫ U.ι =
    Spec.map (Scheme.Hom.appLE f (U.ι ''ᵁ ⊤) (V.ι ''ᵁ X.homOfLE i ⁻¹ᵁ ⊤) ⋯ ≫ X.presheaf.map (eqToHom ⋯).op) ≫
      (↑U).isoSpec.inv ≫ U.ι
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
V : X.Opens
U : Y.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
i : V ≤ f ⁻¹ᵁ U
this : IsAffine ↑U
⊢ Spec.map (Y.presheaf.map (eqToHom ⋯).op ≫ Scheme.Hom.appLE f U V i) ≫ (↑U).isoSpec.inv ≫ U.ι =
    Spec.map (Scheme.Hom.appLE f (U.ι ''ᵁ ⊤) (V.ι ''ᵁ X.homOfLE i ⁻¹ᵁ ⊤) ⋯ ≫ X.presheaf.map (eqToHom ⋯).op) ≫
      (↑U).isoSpec.inv ≫ U.ι

Tactic:
Scheme.Hom.appLE_map,

Goal state after:
X Y : Scheme
f : X ⟶ Y
V : X.Opens
U : Y.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
i : V ≤ f ⁻¹ᵁ U
this : IsAffine ↑U
⊢ Spec.map (Y.presheaf.map (eqToHom ⋯).op ≫ Scheme.Hom.appLE f U V i) ≫ (↑U).isoSpec.inv ≫ U.ι =
    Spec.map (Scheme.Hom.appLE f (U.ι ''ᵁ ⊤) V ⋯) ≫ (↑U).isoSpec.inv ≫ U.ι
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
V : X.Opens
U : Y.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
i : V ≤ f ⁻¹ᵁ U
this : IsAffine ↑U
⊢ Spec.map (Scheme.Hom.appLE f (U.ι ''ᵁ ⊤) V ⋯) ≫ (↑U).isoSpec.inv ≫ U.ι =
    Spec.map (Scheme.Hom.appLE f (U.ι ''ᵁ ⊤) V ⋯) ≫ (↑U).isoSpec.inv ≫ U.ι

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
inst✝ : IsAffine X
⊢ ⊤.ι = ⋯.isoSpec.hom ≫ X.isoSpec.inv

Tactic:
]

Goal state after:
X : Scheme
inst✝ : IsAffine X
⊢ ⊤.ι = ⋯.isoSpec.hom ≫ X.isoSpec.inv
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : ↑(PrimeSpectrum.Top R)
r : R
m : ↑((structurePresheafInModuleCat R M).stalk x)
⊢ (ConcreteCategory.hom (toStalk R x)) r • (modulePresheafStalkIso R M x).symm m =
    r • (modulePresheafStalkIso R M x).symm m

Tactic:
]

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : ↑(PrimeSpectrum.Top R)
r : R
m : ↑((structurePresheafInModuleCat R M).stalk x)
⊢ (ConcreteCategory.hom (toStalk R x)) r • (modulePresheafStalkIso R M x).symm m =
    r • (modulePresheafStalkIso R M x).symm m
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ U
⊢ ModuleCat.ofHom (toOpenₗ R M U) ≫ (structurePresheafInModuleCat R M).germ U x hx =
    (ModuleCat.ofHom (toOpenₗ R M ⊤) ≫ (structurePresheafInModuleCat R M).map (homOfLE ⋯).op) ≫
      (structurePresheafInModuleCat R M).germ U x hx

Tactic:
]

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ U
⊢ ModuleCat.ofHom (toOpenₗ R M U) ≫ (structurePresheafInModuleCat R M).germ U x hx =
    (ModuleCat.ofHom (toOpenₗ R M ⊤) ≫ (structurePresheafInModuleCat R M).map (homOfLE ⋯).op) ≫
      (structurePresheafInModuleCat R M).germ U x hx
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : ↑(PrimeSpectrum.Top R)
f : R
hf : x ∈ basicOpen f
this :
  Function.Bijective
    ⇑((algebraMap (↑((structurePresheafInCommRingCat R).stalk x))
          (Module.End ↑((structurePresheafInCommRingCat R).stalk x) ↑((structurePresheafInModuleCat R M).stalk x)))
        ((ConcreteCategory.hom (toStalk R x)) f))
⊢ Function.Bijective ⇑((algebraMap R (Module.End R ↑((structurePresheafInModuleCat R M).stalk x))) f)

Tactic:
]

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : ↑(PrimeSpectrum.Top R)
f : R
hf : x ∈ basicOpen f
this :
  Function.Bijective
    ⇑((algebraMap (↑((structurePresheafInCommRingCat R).stalk x))
          (Module.End ↑((structurePresheafInCommRingCat R).stalk x) ↑((structurePresheafInModuleCat R M).stalk x)))
        ((ConcreteCategory.hom (toStalk R x)) f))
⊢ Function.Bijective ⇑((algebraMap R (Module.End R ↑((structurePresheafInModuleCat R M).stalk x))) f)
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : ↑(PrimeSpectrum.Top R)
f : R
hf : x ∈ basicOpen f
this :
  Function.Bijective
    ⇑((algebraMap (↑((structurePresheafInCommRingCat R).stalk x))
          (Module.End ↑((structurePresheafInCommRingCat R).stalk x) ↑((structurePresheafInModuleCat R M).stalk x)))
        ((ConcreteCategory.hom (toStalk R x)) f))
a : ↑((structurePresheafInModuleCat R M).stalk x)
⊢ f • a = f • a

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
h : U ≤ V
this : U.ι ⁻¹ᵁ V = ⊤
⊢ X.presheaf.map (homOfLE ⋯).op ≫
      (↑U).presheaf.map (eqToHom ⋯).op ≫
        (U.topIso.hom ≫ (Scheme.ΓSpecIso Γ(X, U)).inv) ≫ (Spec Γ(X, U)).presheaf.map (eqToHom ⋯).op =
    X.presheaf.map (homOfLE h).op ≫ (Scheme.ΓSpecIso Γ(X, U)).inv ≫ (Spec Γ(X, U)).presheaf.map (homOfLE ⋯).op

Tactic:
]

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
h : U ≤ V
this : U.ι ⁻¹ᵁ V = ⊤
⊢ X.presheaf.map (homOfLE ⋯).op ≫
      (↑U).presheaf.map (eqToHom ⋯).op ≫
        (U.topIso.hom ≫ (Scheme.ΓSpecIso Γ(X, U)).inv) ≫ (Spec Γ(X, U)).presheaf.map (eqToHom ⋯).op =
    X.presheaf.map (homOfLE h).op ≫ (Scheme.ΓSpecIso Γ(X, U)).inv ≫ (Spec Γ(X, U)).presheaf.map (homOfLE ⋯).op
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: case w
X Y : LocallyRingedSpace
f : X ⟶ Y
x : ↑↑((𝟭 LocallyRingedSpace).obj X).toPresheafedSpace
⊢ PrimeSpectrum.comap (CommRingCat.Hom.hom (f.c.app (op ⊤) ≫ X.presheaf.Γgerm x))
      (IsLocalRing.closedPoint ↑(X.presheaf.stalk x)) =
    PrimeSpectrum.comap (CommRingCat.Hom.hom (Y.presheaf.Γgerm ((ConcreteCategory.hom f.base) x) ≫ Hom.stalkMap f x))
      (IsLocalRing.closedPoint ↑(X.presheaf.stalk x))

Tactic:
]

Goal state after:
case w
X Y : LocallyRingedSpace
f : X ⟶ Y
x : ↑↑((𝟭 LocallyRingedSpace).obj X).toPresheafedSpace
⊢ PrimeSpectrum.comap (CommRingCat.Hom.hom (f.c.app (op ⊤) ≫ X.presheaf.Γgerm x))
      (IsLocalRing.closedPoint ↑(X.presheaf.stalk x)) =
    PrimeSpectrum.comap (CommRingCat.Hom.hom (Y.presheaf.Γgerm ((ConcreteCategory.hom f.base) x) ≫ Hom.stalkMap f x))
      (IsLocalRing.closedPoint ↑(X.presheaf.stalk x))
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
U : X.Opens
hU : IsAffineOpen U
f : X ⟶ Y
H : IsOpenImmersion f
⊢ IsAffineOpen U

Tactic:
]

Goal state after:
X Y : Scheme
U : X.Opens
hU : IsAffineOpen U
f : X ⟶ Y
H : IsOpenImmersion f
⊢ IsAffineOpen U
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
U : Y.Opens
hU : IsAffineOpen U
f : X ⟶ Y
inst✝ : IsOpenImmersion f
hU' : U ≤ Scheme.Hom.opensRange f
⊢ IsAffineOpen U

Tactic:
]

Goal state after:
X Y : Scheme
U : Y.Opens
hU : IsAffineOpen U
f : X ⟶ Y
inst✝ : IsOpenImmersion f
hU' : U ≤ Scheme.Hom.opensRange f
⊢ IsAffineOpen U
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : ↑(PrimeSpectrum.Top R)
f : M
s : ↥x.asIdeal.primeCompl
⊢ (ModuleCat.Hom.hom
        (ModuleCat.ofHom (toOpenₗ R M (basicOpen ↑s)) ≫ (structurePresheafInModuleCat R M).germ (basicOpen ↑s) x ⋯))
      f =
    (ConcreteCategory.hom ((structurePresheafInModuleCat R M).germ (basicOpen ↑s) x ⋯))
      (const (↑s • f) (↑s) (basicOpen ↑s) ⋯)

Tactic:
]

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : ↑(PrimeSpectrum.Top R)
f : M
s : ↥x.asIdeal.primeCompl
⊢ (ModuleCat.Hom.hom
        (ModuleCat.ofHom (toOpenₗ R M (basicOpen ↑s)) ≫ (structurePresheafInModuleCat R M).germ (basicOpen ↑s) x ⋯))
      f =
    (ConcreteCategory.hom ((structurePresheafInModuleCat R M).germ (basicOpen ↑s) x ⋯))
      (const (↑s • f) (↑s) (basicOpen ↑s) ⋯)
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Scheme.Hom.app hU.fromSpec U = Scheme.Hom.app hU.fromSpec U

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: case h
X Y : LocallyRingedSpace
f : X ⟶ Y
r : ↑(unop (Γ.rightOp.obj Y))
⊢ (Γ.rightOp.map f).unop ≫ ((𝟭 LocallyRingedSpace).obj X).presheaf.map (homOfLE ⋯).op =
    (CommRingCat.ofHom
          (algebraMap (↑(unop (Γ.rightOp.obj Y)))
            ((structureSheafInType ↑(unop (Γ.rightOp.obj Y)) ↑(unop (Γ.rightOp.obj Y))).obj.obj (op (basicOpen r)))) ≫
        Y.toΓSpec.c.app (op (basicOpen r))) ≫
      ((𝟭 LocallyRingedSpace).map f).c.app (op ((Opens.map Y.toΓSpec.base).obj (unop (op (basicOpen r)))))

Tactic:
]

Goal state after:
case h
X Y : LocallyRingedSpace
f : X ⟶ Y
r : ↑(unop (Γ.rightOp.obj Y))
⊢ (Γ.rightOp.map f).unop ≫ ((𝟭 LocallyRingedSpace).obj X).presheaf.map (homOfLE ⋯).op =
    (CommRingCat.ofHom
          (algebraMap (↑(unop (Γ.rightOp.obj Y)))
            ((structureSheafInType ↑(unop (Γ.rightOp.obj Y)) ↑(unop (Γ.rightOp.obj Y))).obj.obj (op (basicOpen r)))) ≫
        Y.toΓSpec.c.app (op (basicOpen r))) ≫
      ((𝟭 LocallyRingedSpace).map f).c.app (op ((Opens.map Y.toΓSpec.base).obj (unop (op (basicOpen r)))))