[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
J : Type v
inst✝ : Category.{v, v} J
F : J ⥤ SheafedSpace C
X Y : SheafedSpace C
f g : X ⟶ Y
⊢ Epi (coequalizer.π f g).base
[PROOFSTEP]
erw [← show _ = (coequalizer.π f g).base from ι_comp_coequalizerComparison f g (SheafedSpace.forget C)]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
J : Type v
inst✝ : Category.{v, v} J
F : J ⥤ SheafedSpace C
X Y : SheafedSpace C
f g : X ⟶ Y
⊢ Epi (coequalizer.π ((forget C).map f) ((forget C).map g) ≫ coequalizerComparison f g (forget C))
[PROOFSTEP]
rw [← PreservesCoequalizer.iso_hom]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
J : Type v
inst✝ : Category.{v, v} J
F : J ⥤ SheafedSpace C
X Y : SheafedSpace C
f g : X ⟶ Y
⊢ Epi (coequalizer.π ((forget C).map f) ((forget C).map g) ≫ (PreservesCoequalizer.iso (forget C) f g).hom)
[PROOFSTEP]
apply epi_comp
[GOAL]
ι : Type u
F : Discrete ι ⥤ LocallyRingedSpace
x : ↑↑(colimit (F ⋙ forgetToSheafedSpace)).toPresheafedSpace
⊢ LocalRing ↑(TopCat.Presheaf.stalk (colimit (F ⋙ forgetToSheafedSpace)).toPresheafedSpace.presheaf x)
[PROOFSTEP]
obtain ⟨i, y, ⟨⟩⟩ := SheafedSpace.colimit_exists_rep (F ⋙ forgetToSheafedSpace) x
[GOAL]
case intro.intro.refl
ι : Type u
F : Discrete ι ⥤ LocallyRingedSpace
i : Discrete ι
y : ↑↑((F ⋙ forgetToSheafedSpace).obj i).toPresheafedSpace
⊢ LocalRing
    ↑(TopCat.Presheaf.stalk (colimit (F ⋙ forgetToSheafedSpace)).toPresheafedSpace.presheaf
        (↑(colimit.ι (F ⋙ forgetToSheafedSpace) i).base y))
[PROOFSTEP]
haveI : LocalRing (((F ⋙ forgetToSheafedSpace).obj i).toPresheafedSpace.stalk y) := (F.obj i).localRing _
[GOAL]
case intro.intro.refl
ι : Type u
F : Discrete ι ⥤ LocallyRingedSpace
i : Discrete ι
y : ↑↑((F ⋙ forgetToSheafedSpace).obj i).toPresheafedSpace
this : LocalRing ↑(PresheafedSpace.stalk ((F ⋙ forgetToSheafedSpace).obj i).toPresheafedSpace y)
⊢ LocalRing
    ↑(TopCat.Presheaf.stalk (colimit (F ⋙ forgetToSheafedSpace)).toPresheafedSpace.presheaf
        (↑(colimit.ι (F ⋙ forgetToSheafedSpace) i).base y))
[PROOFSTEP]
exact
  (asIso
      (PresheafedSpace.stalkMap
        (colimit.ι (C := SheafedSpace.{u + 1, u, u} CommRingCatMax.{u, u}) (F ⋙ forgetToSheafedSpace) i : _)
        y)).symm.commRingCatIsoToRingEquiv.localRing
[GOAL]
ι : Type u
F : Discrete ι ⥤ LocallyRingedSpace
x✝² x✝¹ : Discrete ι
j j' : ι
x✝ : { as := j } ⟶ { as := j' }
f : j = j'
⊢ F.map { down := { down := f } } ≫
      (fun j =>
          { val := colimit.ι (F ⋙ forgetToSheafedSpace) j,
            prop :=
              (_ :
                ∀ (x : ↑↑(F.obj j).toPresheafedSpace),
                  IsLocalRingHom (PresheafedSpace.stalkMap (colimit.ι (F ⋙ forgetToSheafedSpace) j) x)) })
        { as := j' } =
    (fun j =>
          { val := colimit.ι (F ⋙ forgetToSheafedSpace) j,
            prop :=
              (_ :
                ∀ (x : ↑↑(F.obj j).toPresheafedSpace),
                  IsLocalRingHom (PresheafedSpace.stalkMap (colimit.ι (F ⋙ forgetToSheafedSpace) j) x)) })
        { as := j } ≫
      ((Functor.const (Discrete ι)).obj (coproduct F)).map { down := { down := f } }
[PROOFSTEP]
subst f
[GOAL]
ι : Type u
F : Discrete ι ⥤ LocallyRingedSpace
x✝² x✝¹ : Discrete ι
j : ι
x✝ : { as := j } ⟶ { as := j }
⊢ F.map { down := { down := (_ : j = j) } } ≫
      (fun j =>
          { val := colimit.ι (F ⋙ forgetToSheafedSpace) j,
            prop :=
              (_ :
                ∀ (x : ↑↑(F.obj j).toPresheafedSpace),
                  IsLocalRingHom (PresheafedSpace.stalkMap (colimit.ι (F ⋙ forgetToSheafedSpace) j) x)) })
        { as := j } =
    (fun j =>
          { val := colimit.ι (F ⋙ forgetToSheafedSpace) j,
            prop :=
              (_ :
                ∀ (x : ↑↑(F.obj j).toPresheafedSpace),
                  IsLocalRingHom (PresheafedSpace.stalkMap (colimit.ι (F ⋙ forgetToSheafedSpace) j) x)) })
        { as := j } ≫
      ((Functor.const (Discrete ι)).obj (coproduct F)).map { down := { down := (_ : j = j) } }
[PROOFSTEP]
aesop
[GOAL]
ι : Type u
F : Discrete ι ⥤ LocallyRingedSpace
s : Cocone F
⊢ ∀ (x : ↑↑(coproductCofan F).pt.toPresheafedSpace),
    IsLocalRingHom
      (PresheafedSpace.stalkMap (colimit.desc (F ⋙ forgetToSheafedSpace) (forgetToSheafedSpace.mapCocone s)) x)
[PROOFSTEP]
intro x
[GOAL]
ι : Type u
F : Discrete ι ⥤ LocallyRingedSpace
s : Cocone F
x : ↑↑(coproductCofan F).pt.toPresheafedSpace
⊢ IsLocalRingHom
    (PresheafedSpace.stalkMap (colimit.desc (F ⋙ forgetToSheafedSpace) (forgetToSheafedSpace.mapCocone s)) x)
[PROOFSTEP]
obtain ⟨i, y, ⟨⟩⟩ := SheafedSpace.colimit_exists_rep (F ⋙ forgetToSheafedSpace) x
[GOAL]
case intro.intro.refl
ι : Type u
F : Discrete ι ⥤ LocallyRingedSpace
s : Cocone F
i : Discrete ι
y : ↑↑((F ⋙ forgetToSheafedSpace).obj i).toPresheafedSpace
⊢ IsLocalRingHom
    (PresheafedSpace.stalkMap (colimit.desc (F ⋙ forgetToSheafedSpace) (forgetToSheafedSpace.mapCocone s))
      (↑(colimit.ι (F ⋙ forgetToSheafedSpace) i).base y))
[PROOFSTEP]
have :=
  PresheafedSpace.stalkMap.comp
    (colimit.ι (C := SheafedSpace.{u + 1, u, u} CommRingCatMax.{u, u}) (F ⋙ forgetToSheafedSpace) i)
    (colimit.desc (C := SheafedSpace.{u + 1, u, u} CommRingCatMax.{u, u}) (F ⋙ forgetToSheafedSpace)
      (forgetToSheafedSpace.mapCocone s))
    y
[GOAL]
case intro.intro.refl
ι : Type u
F : Discrete ι ⥤ LocallyRingedSpace
s : Cocone F
i : Discrete ι
y : ↑↑((F ⋙ forgetToSheafedSpace).obj i).toPresheafedSpace
this :
  PresheafedSpace.stalkMap
      (colimit.ι (F ⋙ forgetToSheafedSpace) i ≫
        colimit.desc (F ⋙ forgetToSheafedSpace) (forgetToSheafedSpace.mapCocone s))
      y =
    PresheafedSpace.stalkMap (colimit.desc (F ⋙ forgetToSheafedSpace) (forgetToSheafedSpace.mapCocone s))
        (↑(colimit.ι (F ⋙ forgetToSheafedSpace) i).base y) ≫
      PresheafedSpace.stalkMap (colimit.ι (F ⋙ forgetToSheafedSpace) i) y
⊢ IsLocalRingHom
    (PresheafedSpace.stalkMap (colimit.desc (F ⋙ forgetToSheafedSpace) (forgetToSheafedSpace.mapCocone s))
      (↑(colimit.ι (F ⋙ forgetToSheafedSpace) i).base y))
[PROOFSTEP]
rw [← IsIso.comp_inv_eq] at this
[GOAL]
case intro.intro.refl
ι : Type u
F : Discrete ι ⥤ LocallyRingedSpace
s : Cocone F
i : Discrete ι
y : ↑↑((F ⋙ forgetToSheafedSpace).obj i).toPresheafedSpace
this :
  PresheafedSpace.stalkMap
        (colimit.ι (F ⋙ forgetToSheafedSpace) i ≫
          colimit.desc (F ⋙ forgetToSheafedSpace) (forgetToSheafedSpace.mapCocone s))
        y ≫
      inv (PresheafedSpace.stalkMap (colimit.ι (F ⋙ forgetToSheafedSpace) i) y) =
    PresheafedSpace.stalkMap (colimit.desc (F ⋙ forgetToSheafedSpace) (forgetToSheafedSpace.mapCocone s))
      (↑(colimit.ι (F ⋙ forgetToSheafedSpace) i).base y)
⊢ IsLocalRingHom
    (PresheafedSpace.stalkMap (colimit.desc (F ⋙ forgetToSheafedSpace) (forgetToSheafedSpace.mapCocone s))
      (↑(colimit.ι (F ⋙ forgetToSheafedSpace) i).base y))
[PROOFSTEP]
erw [← this,
  PresheafedSpace.stalkMap.congr_hom _ _
    (colimit.ι_desc (C := SheafedSpace.{u + 1, u, u} CommRingCatMax.{u, u}) (forgetToSheafedSpace.mapCocone s) i : _)]
[GOAL]
case intro.intro.refl
ι : Type u
F : Discrete ι ⥤ LocallyRingedSpace
s : Cocone F
i : Discrete ι
y : ↑↑((F ⋙ forgetToSheafedSpace).obj i).toPresheafedSpace
this :
  PresheafedSpace.stalkMap
        (colimit.ι (F ⋙ forgetToSheafedSpace) i ≫
          colimit.desc (F ⋙ forgetToSheafedSpace) (forgetToSheafedSpace.mapCocone s))
        y ≫
      inv (PresheafedSpace.stalkMap (colimit.ι (F ⋙ forgetToSheafedSpace) i) y) =
    PresheafedSpace.stalkMap (colimit.desc (F ⋙ forgetToSheafedSpace) (forgetToSheafedSpace.mapCocone s))
      (↑(colimit.ι (F ⋙ forgetToSheafedSpace) i).base y)
⊢ IsLocalRingHom
    ((eqToHom
          (_ :
            PresheafedSpace.stalk (forgetToSheafedSpace.mapCocone s).pt.toPresheafedSpace
                (↑(colimit.ι (F ⋙ forgetToSheafedSpace) i ≫
                        colimit.desc (F ⋙ forgetToSheafedSpace) (forgetToSheafedSpace.mapCocone s)).base
                  y) =
              PresheafedSpace.stalk (forgetToSheafedSpace.mapCocone s).pt.toPresheafedSpace
                (↑(NatTrans.app (forgetToSheafedSpace.mapCocone s).ι i).base y)) ≫
        PresheafedSpace.stalkMap (NatTrans.app (forgetToSheafedSpace.mapCocone s).ι i) y) ≫
      inv (PresheafedSpace.stalkMap (colimit.ι (F ⋙ forgetToSheafedSpace) i) y))
[PROOFSTEP]
haveI : IsLocalRingHom (PresheafedSpace.stalkMap ((forgetToSheafedSpace.mapCocone s).ι.app i) y) := (s.ι.app i).2 y
[GOAL]
case intro.intro.refl
ι : Type u
F : Discrete ι ⥤ LocallyRingedSpace
s : Cocone F
i : Discrete ι
y : ↑↑((F ⋙ forgetToSheafedSpace).obj i).toPresheafedSpace
this✝ :
  PresheafedSpace.stalkMap
        (colimit.ι (F ⋙ forgetToSheafedSpace) i ≫
          colimit.desc (F ⋙ forgetToSheafedSpace) (forgetToSheafedSpace.mapCocone s))
        y ≫
      inv (PresheafedSpace.stalkMap (colimit.ι (F ⋙ forgetToSheafedSpace) i) y) =
    PresheafedSpace.stalkMap (colimit.desc (F ⋙ forgetToSheafedSpace) (forgetToSheafedSpace.mapCocone s))
      (↑(colimit.ι (F ⋙ forgetToSheafedSpace) i).base y)
this : IsLocalRingHom (PresheafedSpace.stalkMap (NatTrans.app (forgetToSheafedSpace.mapCocone s).ι i) y)
⊢ IsLocalRingHom
    ((eqToHom
          (_ :
            PresheafedSpace.stalk (forgetToSheafedSpace.mapCocone s).pt.toPresheafedSpace
                (↑(colimit.ι (F ⋙ forgetToSheafedSpace) i ≫
                        colimit.desc (F ⋙ forgetToSheafedSpace) (forgetToSheafedSpace.mapCocone s)).base
                  y) =
              PresheafedSpace.stalk (forgetToSheafedSpace.mapCocone s).pt.toPresheafedSpace
                (↑(NatTrans.app (forgetToSheafedSpace.mapCocone s).ι i).base y)) ≫
        PresheafedSpace.stalkMap (NatTrans.app (forgetToSheafedSpace.mapCocone s).ι i) y) ≫
      inv (PresheafedSpace.stalkMap (colimit.ι (F ⋙ forgetToSheafedSpace) i) y))
[PROOFSTEP]
infer_instance
[GOAL]
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace
⊢ IsLocalRingHom (NatTrans.app (coequalizer.π f.val g.val).c (op U))
[PROOFSTEP]
have := ι_comp_coequalizerComparison f.1 g.1 SheafedSpace.forgetToPresheafedSpace
[GOAL]
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace
this :
  coequalizer.π (SheafedSpace.forgetToPresheafedSpace.map f.val) (SheafedSpace.forgetToPresheafedSpace.map g.val) ≫
      coequalizerComparison f.val g.val SheafedSpace.forgetToPresheafedSpace =
    SheafedSpace.forgetToPresheafedSpace.map (coequalizer.π f.val g.val)
⊢ IsLocalRingHom (NatTrans.app (coequalizer.π f.val g.val).c (op U))
[PROOFSTEP]
rw [← PreservesCoequalizer.iso_hom] at this
[GOAL]
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace
this :
  coequalizer.π (SheafedSpace.forgetToPresheafedSpace.map f.val) (SheafedSpace.forgetToPresheafedSpace.map g.val) ≫
      (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace f.val g.val).hom =
    SheafedSpace.forgetToPresheafedSpace.map (coequalizer.π f.val g.val)
⊢ IsLocalRingHom (NatTrans.app (coequalizer.π f.val g.val).c (op U))
[PROOFSTEP]
erw [SheafedSpace.congr_app this.symm (op U)]
[GOAL]
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace
this :
  coequalizer.π (SheafedSpace.forgetToPresheafedSpace.map f.val) (SheafedSpace.forgetToPresheafedSpace.map g.val) ≫
      (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace f.val g.val).hom =
    SheafedSpace.forgetToPresheafedSpace.map (coequalizer.π f.val g.val)
⊢ IsLocalRingHom
    (NatTrans.app
        (coequalizer.π (SheafedSpace.forgetToPresheafedSpace.map f.val)
              (SheafedSpace.forgetToPresheafedSpace.map g.val) ≫
            (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace f.val g.val).hom).c
        (op U) ≫
      Y.presheaf.map
        (eqToHom
          (_ :
            (Opens.map
                      (coequalizer.π (SheafedSpace.forgetToPresheafedSpace.map f.val)
                            (SheafedSpace.forgetToPresheafedSpace.map g.val) ≫
                          (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace f.val g.val).hom).base).op.obj
                (op U) =
              (Opens.map (SheafedSpace.forgetToPresheafedSpace.map (coequalizer.π f.val g.val)).base).op.obj (op U))))
[PROOFSTEP]
rw [PresheafedSpace.comp_c_app, ← PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit_hom_π]
  -- Porting note : this instance has to be manually added
[GOAL]
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace
this :
  coequalizer.π (SheafedSpace.forgetToPresheafedSpace.map f.val) (SheafedSpace.forgetToPresheafedSpace.map g.val) ≫
      (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace f.val g.val).hom =
    SheafedSpace.forgetToPresheafedSpace.map (coequalizer.π f.val g.val)
⊢ IsLocalRingHom
    ((NatTrans.app (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace f.val g.val).hom.c (op U) ≫
        (PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit
              (parallelPair (SheafedSpace.forgetToPresheafedSpace.map f.val)
                (SheafedSpace.forgetToPresheafedSpace.map g.val))
              ((Opens.map (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace f.val g.val).hom.base).obj
                (op U).unop)).hom ≫
          limit.π
            (PresheafedSpace.componentwiseDiagram
              (parallelPair (SheafedSpace.forgetToPresheafedSpace.map f.val)
                (SheafedSpace.forgetToPresheafedSpace.map g.val))
              ((Opens.map (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace f.val g.val).hom.base).obj
                (op U).unop))
            (op WalkingParallelPair.one)) ≫
      Y.presheaf.map
        (eqToHom
          (_ :
            (Opens.map
                      (coequalizer.π (SheafedSpace.forgetToPresheafedSpace.map f.val)
                            (SheafedSpace.forgetToPresheafedSpace.map g.val) ≫
                          (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace f.val g.val).hom).base).op.obj
                (op U) =
              (Opens.map (SheafedSpace.forgetToPresheafedSpace.map (coequalizer.π f.val g.val)).base).op.obj (op U))))
[PROOFSTEP]
haveI : IsIso (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace f.val g.val).hom.c :=
  PresheafedSpace.c_isIso_of_iso _
[GOAL]
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace
this✝ :
  coequalizer.π (SheafedSpace.forgetToPresheafedSpace.map f.val) (SheafedSpace.forgetToPresheafedSpace.map g.val) ≫
      (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace f.val g.val).hom =
    SheafedSpace.forgetToPresheafedSpace.map (coequalizer.π f.val g.val)
this : IsIso (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace f.val g.val).hom.c
⊢ IsLocalRingHom
    ((NatTrans.app (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace f.val g.val).hom.c (op U) ≫
        (PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit
              (parallelPair (SheafedSpace.forgetToPresheafedSpace.map f.val)
                (SheafedSpace.forgetToPresheafedSpace.map g.val))
              ((Opens.map (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace f.val g.val).hom.base).obj
                (op U).unop)).hom ≫
          limit.π
            (PresheafedSpace.componentwiseDiagram
              (parallelPair (SheafedSpace.forgetToPresheafedSpace.map f.val)
                (SheafedSpace.forgetToPresheafedSpace.map g.val))
              ((Opens.map (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace f.val g.val).hom.base).obj
                (op U).unop))
            (op WalkingParallelPair.one)) ≫
      Y.presheaf.map
        (eqToHom
          (_ :
            (Opens.map
                      (coequalizer.π (SheafedSpace.forgetToPresheafedSpace.map f.val)
                            (SheafedSpace.forgetToPresheafedSpace.map g.val) ≫
                          (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace f.val g.val).hom).base).op.obj
                (op U) =
              (Opens.map (SheafedSpace.forgetToPresheafedSpace.map (coequalizer.π f.val g.val)).base).op.obj (op U))))
[PROOFSTEP]
infer_instance
[GOAL]
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace
s : ↑((coequalizer f.val g.val).toPresheafedSpace.presheaf.obj (op U))
⊢ ↑(coequalizer.π f.val g.val).base ⁻¹' (↑(coequalizer.π f.val g.val).base '' (imageBasicOpen f g U s).carrier) =
    (imageBasicOpen f g U s).carrier
[PROOFSTEP]
fapply
  Types.coequalizer_preimage_image_eq_of_preimage_eq (f.1.base : X.carrier.1 ⟶ Y.carrier.1)
    (g.1.base : X.carrier.1 ⟶ Y.carrier.1)
[GOAL]
case e
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace
s : ↑((coequalizer f.val g.val).toPresheafedSpace.presheaf.obj (op U))
⊢ ↑f.val.base ≫ ↑(coequalizer.π f.val g.val).base = ↑g.val.base ≫ ↑(coequalizer.π f.val g.val).base
[PROOFSTEP]
ext
[GOAL]
case e.h
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace
s : ↑((coequalizer f.val g.val).toPresheafedSpace.presheaf.obj (op U))
a✝ : (forget TopCat).obj ↑X.toPresheafedSpace
⊢ (↑f.val.base ≫ ↑(coequalizer.π f.val g.val).base) a✝ = (↑g.val.base ≫ ↑(coequalizer.π f.val g.val).base) a✝
[PROOFSTEP]
simp_rw [types_comp_apply, ← TopCat.comp_app, ← PresheafedSpace.comp_base]
[GOAL]
case e.h
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace
s : ↑((coequalizer f.val g.val).toPresheafedSpace.presheaf.obj (op U))
a✝ : (forget TopCat).obj ↑X.toPresheafedSpace
⊢ ↑(f.val ≫ coequalizer.π f.val g.val).base a✝ = ↑(g.val ≫ coequalizer.π f.val g.val).base a✝
[PROOFSTEP]
congr 2
[GOAL]
case e.h.e_a.e_self
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace
s : ↑((coequalizer f.val g.val).toPresheafedSpace.presheaf.obj (op U))
a✝ : (forget TopCat).obj ↑X.toPresheafedSpace
⊢ f.val ≫ coequalizer.π f.val g.val = g.val ≫ coequalizer.π f.val g.val
[PROOFSTEP]
exact coequalizer.condition f.1 g.1
[GOAL]
case h
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace
s : ↑((coequalizer f.val g.val).toPresheafedSpace.presheaf.obj (op U))
⊢ IsColimit
    (Cofork.ofπ ↑(coequalizer.π f.val g.val).base
      (_ : ↑f.val.base ≫ ↑(coequalizer.π f.val g.val).base = ↑g.val.base ≫ ↑(coequalizer.π f.val g.val).base))
[PROOFSTEP]
apply isColimitCoforkMapOfIsColimit (forget TopCat)
[GOAL]
case h.l
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace
s : ↑((coequalizer f.val g.val).toPresheafedSpace.presheaf.obj (op U))
⊢ IsColimit (Cofork.ofπ (coequalizer.π f.val g.val).base ?h.w)
case h.w
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace
s : ↑((coequalizer f.val g.val).toPresheafedSpace.presheaf.obj (op U))
⊢ f.val.base ≫ (coequalizer.π f.val g.val).base = g.val.base ≫ (coequalizer.π f.val g.val).base
[PROOFSTEP]
apply isColimitCoforkMapOfIsColimit (SheafedSpace.forget _)
[GOAL]
case h.l.l
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace
s : ↑((coequalizer f.val g.val).toPresheafedSpace.presheaf.obj (op U))
⊢ IsColimit (Cofork.ofπ (coequalizer.π f.val g.val) ?h.l.w)
case h.l.w
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace
s : ↑((coequalizer f.val g.val).toPresheafedSpace.presheaf.obj (op U))
⊢ f.val ≫ coequalizer.π f.val g.val = g.val ≫ coequalizer.π f.val g.val
[PROOFSTEP]
exact coequalizerIsCoequalizer f.1 g.1
[GOAL]
case H
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace
s : ↑((coequalizer f.val g.val).toPresheafedSpace.presheaf.obj (op U))
⊢ ↑f.val.base ⁻¹' (imageBasicOpen f g U s).carrier = ↑g.val.base ⁻¹' (imageBasicOpen f g U s).carrier
[PROOFSTEP]
suffices
  (TopologicalSpace.Opens.map f.1.base).obj (imageBasicOpen f g U s) =
    (TopologicalSpace.Opens.map g.1.base).obj (imageBasicOpen f g U s)
  by injection this
[GOAL]
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace
s : ↑((coequalizer f.val g.val).toPresheafedSpace.presheaf.obj (op U))
this : (Opens.map f.val.base).obj (imageBasicOpen f g U s) = (Opens.map g.val.base).obj (imageBasicOpen f g U s)
⊢ ↑f.val.base ⁻¹' (imageBasicOpen f g U s).carrier = ↑g.val.base ⁻¹' (imageBasicOpen f g U s).carrier
[PROOFSTEP]
injection this
[GOAL]
case H
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace
s : ↑((coequalizer f.val g.val).toPresheafedSpace.presheaf.obj (op U))
⊢ (Opens.map f.val.base).obj (imageBasicOpen f g U s) = (Opens.map g.val.base).obj (imageBasicOpen f g U s)
[PROOFSTEP]
delta imageBasicOpen
[GOAL]
case H
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace
s : ↑((coequalizer f.val g.val).toPresheafedSpace.presheaf.obj (op U))
⊢ (Opens.map f.val.base).obj
      (RingedSpace.basicOpen (toRingedSpace Y)
        (let_fun this := ↑(NatTrans.app (coequalizer.π f.val g.val).c (op U)) s;
        this)) =
    (Opens.map g.val.base).obj
      (RingedSpace.basicOpen (toRingedSpace Y)
        (let_fun this := ↑(NatTrans.app (coequalizer.π f.val g.val).c (op U)) s;
        this))
[PROOFSTEP]
rw [preimage_basicOpen f, preimage_basicOpen g]
[GOAL]
case H
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace
s : ↑((coequalizer f.val g.val).toPresheafedSpace.presheaf.obj (op U))
⊢ RingedSpace.basicOpen (toRingedSpace X)
      (↑(NatTrans.app f.val.c
            (op
              {
                  unop :=
                    { carrier := ↑(coequalizer.π f.val g.val).base ⁻¹' ↑(op U).unop,
                      is_open' := (_ : IsOpen (↑(coequalizer.π f.val g.val).base ⁻¹' ↑(op U).unop)) } }.unop))
        (let_fun this := ↑(NatTrans.app (coequalizer.π f.val g.val).c (op U)) s;
        this)) =
    RingedSpace.basicOpen (toRingedSpace X)
      (↑(NatTrans.app g.val.c
            (op
              {
                  unop :=
                    { carrier := ↑(coequalizer.π f.val g.val).base ⁻¹' ↑(op U).unop,
                      is_open' := (_ : IsOpen (↑(coequalizer.π f.val g.val).base ⁻¹' ↑(op U).unop)) } }.unop))
        (let_fun this := ↑(NatTrans.app (coequalizer.π f.val g.val).c (op U)) s;
        this))
[PROOFSTEP]
dsimp only [Functor.op, unop_op]
  -- Porting note : change `rw` to `erw`
[GOAL]
case H
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace
s : ↑((coequalizer f.val g.val).toPresheafedSpace.presheaf.obj (op U))
⊢ RingedSpace.basicOpen (toRingedSpace X)
      (↑(NatTrans.app f.val.c
            (op
              { carrier := ↑(coequalizer.π f.val g.val).base ⁻¹' ↑U,
                is_open' := (_ : IsOpen (↑(coequalizer.π f.val g.val).base ⁻¹' ↑(op U).unop)) }))
        (↑(NatTrans.app (coequalizer.π f.val g.val).c (op U)) s)) =
    RingedSpace.basicOpen (toRingedSpace X)
      (↑(NatTrans.app g.val.c
            (op
              { carrier := ↑(coequalizer.π f.val g.val).base ⁻¹' ↑U,
                is_open' := (_ : IsOpen (↑(coequalizer.π f.val g.val).base ⁻¹' ↑(op U).unop)) }))
        (↑(NatTrans.app (coequalizer.π f.val g.val).c (op U)) s))
[PROOFSTEP]
erw [← comp_apply, ← SheafedSpace.comp_c_app', ← comp_apply, ← SheafedSpace.comp_c_app',
  SheafedSpace.congr_app (coequalizer.condition f.1 g.1), comp_apply, X.toRingedSpace.basicOpen_res]
[GOAL]
case H
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace
s : ↑((coequalizer f.val g.val).toPresheafedSpace.presheaf.obj (op U))
⊢ ((Opens.map (f.val ≫ coequalizer.π f.val g.val).base).op.obj (op U)).unop ⊓
      RingedSpace.basicOpen (toRingedSpace X) (↑(NatTrans.app (g.val ≫ coequalizer.π f.val g.val).c (op U)) s) =
    RingedSpace.basicOpen (toRingedSpace X) (↑(NatTrans.app (g.val ≫ coequalizer.π f.val g.val).c (op U)) s)
[PROOFSTEP]
apply inf_eq_right.mpr
[GOAL]
case H
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace
s : ↑((coequalizer f.val g.val).toPresheafedSpace.presheaf.obj (op U))
⊢ RingedSpace.basicOpen (toRingedSpace X) (↑(NatTrans.app (g.val ≫ coequalizer.π f.val g.val).c (op U)) s) ≤
    ((Opens.map (f.val ≫ coequalizer.π f.val g.val).base).op.obj (op U)).unop
[PROOFSTEP]
refine' (RingedSpace.basicOpen_le _ _).trans _
[GOAL]
case H
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace
s : ↑((coequalizer f.val g.val).toPresheafedSpace.presheaf.obj (op U))
⊢ ((Opens.map (g.val ≫ coequalizer.π f.val g.val).base).op.obj (op U)).unop ≤
    ((Opens.map (f.val ≫ coequalizer.π f.val g.val).base).op.obj (op U)).unop
[PROOFSTEP]
rw [coequalizer.condition f.1 g.1]
[GOAL]
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace
s : ↑((coequalizer f.val g.val).toPresheafedSpace.presheaf.obj (op U))
⊢ IsOpen (↑(coequalizer.π f.val g.val).base '' (imageBasicOpen f g U s).carrier)
[PROOFSTEP]
rw [← (TopCat.homeoOfIso (PreservesCoequalizer.iso (SheafedSpace.forget _) f.1 g.1)).isOpen_preimage,
  TopCat.coequalizer_isOpen_iff, ← Set.preimage_comp]
[GOAL]
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace
s : ↑((coequalizer f.val g.val).toPresheafedSpace.presheaf.obj (op U))
⊢ IsOpen
    (↑(TopCat.homeoOfIso (PreservesCoequalizer.iso (SheafedSpace.forget CommRingCat) f.val g.val)) ∘
        ↑(colimit.ι
            (parallelPair ((SheafedSpace.forget CommRingCat).map f.val) ((SheafedSpace.forget CommRingCat).map g.val))
            WalkingParallelPair.one) ⁻¹'
      (↑(coequalizer.π f.val g.val).base '' (imageBasicOpen f g U s).carrier))
[PROOFSTEP]
erw [← coe_comp]
[GOAL]
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace
s : ↑((coequalizer f.val g.val).toPresheafedSpace.presheaf.obj (op U))
⊢ IsOpen
    (↑(colimit.ι
            (parallelPair ((SheafedSpace.forget CommRingCat).map f.val) ((SheafedSpace.forget CommRingCat).map g.val))
            WalkingParallelPair.one ≫
          (PreservesCoequalizer.iso (SheafedSpace.forget CommRingCat) f.val g.val).hom) ⁻¹'
      (↑(coequalizer.π f.val g.val).base '' (imageBasicOpen f g U s).carrier))
[PROOFSTEP]
rw [PreservesCoequalizer.iso_hom, ι_comp_coequalizerComparison]
[GOAL]
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace
s : ↑((coequalizer f.val g.val).toPresheafedSpace.presheaf.obj (op U))
⊢ IsOpen
    (↑((SheafedSpace.forget CommRingCat).map (coequalizer.π f.val g.val)) ⁻¹'
      (↑(coequalizer.π f.val g.val).base '' (imageBasicOpen f g U s).carrier))
[PROOFSTEP]
dsimp only [SheafedSpace.forget]
  -- Porting note : change `rw` to `erw`
[GOAL]
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace
s : ↑((coequalizer f.val g.val).toPresheafedSpace.presheaf.obj (op U))
⊢ IsOpen (↑(coequalizer.π f.val g.val).base ⁻¹' (↑(coequalizer.π f.val g.val).base '' (imageBasicOpen f g U s).carrier))
[PROOFSTEP]
erw [imageBasicOpen_image_preimage]
[GOAL]
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace
s : ↑((coequalizer f.val g.val).toPresheafedSpace.presheaf.obj (op U))
⊢ IsOpen (imageBasicOpen f g U s).carrier
[PROOFSTEP]
exact (imageBasicOpen f g U s).2
[GOAL]
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace
s : ↑((coequalizer f.val g.val).toPresheafedSpace.presheaf.obj (op U))
x : ↑(toTopCat Y)
⊢ IsLocalRingHom (PresheafedSpace.stalkMap (coequalizer.π f.val g.val) x)
[PROOFSTEP]
constructor
[GOAL]
case map_nonunit
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace
s : ↑((coequalizer f.val g.val).toPresheafedSpace.presheaf.obj (op U))
x : ↑(toTopCat Y)
⊢ ∀ (a : ↑(PresheafedSpace.stalk (coequalizer f.val g.val).toPresheafedSpace (↑(coequalizer.π f.val g.val).base x))),
    IsUnit (↑(PresheafedSpace.stalkMap (coequalizer.π f.val g.val) x) a) → IsUnit a
[PROOFSTEP]
rintro a ha
[GOAL]
case map_nonunit
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace
s : ↑((coequalizer f.val g.val).toPresheafedSpace.presheaf.obj (op U))
x : ↑(toTopCat Y)
a : ↑(PresheafedSpace.stalk (coequalizer f.val g.val).toPresheafedSpace (↑(coequalizer.π f.val g.val).base x))
ha : IsUnit (↑(PresheafedSpace.stalkMap (coequalizer.π f.val g.val) x) a)
⊢ IsUnit a
[PROOFSTEP]
rcases TopCat.Presheaf.germ_exist _ _ a with ⟨U, hU, s, rfl⟩
[GOAL]
case map_nonunit.intro.intro.intro
X Y : LocallyRingedSpace
f g : X ⟶ Y
U✝ : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace
s✝ : ↑((coequalizer f.val g.val).toPresheafedSpace.presheaf.obj (op U✝))
x : ↑(toTopCat Y)
U : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace
hU : ↑(coequalizer.π f.val g.val).base x ∈ U
s : (forget CommRingCat).obj ((coequalizer f.val g.val).toPresheafedSpace.presheaf.obj (op U))
ha :
  IsUnit
    (↑(PresheafedSpace.stalkMap (coequalizer.π f.val g.val) x)
      (↑(TopCat.Presheaf.germ (coequalizer f.val g.val).toPresheafedSpace.presheaf
            { val := ↑(coequalizer.π f.val g.val).base x, property := hU })
        s))
⊢ IsUnit
    (↑(TopCat.Presheaf.germ (coequalizer f.val g.val).toPresheafedSpace.presheaf
          { val := ↑(coequalizer.π f.val g.val).base x, property := hU })
      s)
[PROOFSTEP]
erw [PresheafedSpace.stalkMap_germ_apply (coequalizer.π f.1 g.1 : _) U ⟨_, hU⟩] at ha
[GOAL]
case map_nonunit.intro.intro.intro
X Y : LocallyRingedSpace
f g : X ⟶ Y
U✝ : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace
s✝ : ↑((coequalizer f.val g.val).toPresheafedSpace.presheaf.obj (op U✝))
x : ↑(toTopCat Y)
U : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace
hU : ↑(coequalizer.π f.val g.val).base x ∈ U
s : (forget CommRingCat).obj ((coequalizer f.val g.val).toPresheafedSpace.presheaf.obj (op U))
ha :
  IsUnit
    (↑(TopCat.Presheaf.germ Y.presheaf { val := x, property := hU })
      (↑(NatTrans.app (coequalizer.π f.val g.val).c (op U)) s))
⊢ IsUnit
    (↑(TopCat.Presheaf.germ (coequalizer f.val g.val).toPresheafedSpace.presheaf
          { val := ↑(coequalizer.π f.val g.val).base x, property := hU })
      s)
[PROOFSTEP]
let V := imageBasicOpen f g U s
[GOAL]
case map_nonunit.intro.intro.intro
X Y : LocallyRingedSpace
f g : X ⟶ Y
U✝ : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace
s✝ : ↑((coequalizer f.val g.val).toPresheafedSpace.presheaf.obj (op U✝))
x : ↑(toTopCat Y)
U : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace
hU : ↑(coequalizer.π f.val g.val).base x ∈ U
s : (forget CommRingCat).obj ((coequalizer f.val g.val).toPresheafedSpace.presheaf.obj (op U))
ha :
  IsUnit
    (↑(TopCat.Presheaf.germ Y.presheaf { val := x, property := hU })
      (↑(NatTrans.app (coequalizer.π f.val g.val).c (op U)) s))
V : Opens ↑(toTopCat Y) := imageBasicOpen f g U s
⊢ IsUnit
    (↑(TopCat.Presheaf.germ (coequalizer f.val g.val).toPresheafedSpace.presheaf
          { val := ↑(coequalizer.π f.val g.val).base x, property := hU })
      s)
[PROOFSTEP]
have hV : (coequalizer.π f.1 g.1).base ⁻¹' ((coequalizer.π f.1 g.1).base '' V.1) = V.1 :=
  imageBasicOpen_image_preimage f g U s
[GOAL]
case map_nonunit.intro.intro.intro
X Y : LocallyRingedSpace
f g : X ⟶ Y
U✝ : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace
s✝ : ↑((coequalizer f.val g.val).toPresheafedSpace.presheaf.obj (op U✝))
x : ↑(toTopCat Y)
U : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace
hU : ↑(coequalizer.π f.val g.val).base x ∈ U
s : (forget CommRingCat).obj ((coequalizer f.val g.val).toPresheafedSpace.presheaf.obj (op U))
ha :
  IsUnit
    (↑(TopCat.Presheaf.germ Y.presheaf { val := x, property := hU })
      (↑(NatTrans.app (coequalizer.π f.val g.val).c (op U)) s))
V : Opens ↑(toTopCat Y) := imageBasicOpen f g U s
hV : ↑(coequalizer.π f.val g.val).base ⁻¹' (↑(coequalizer.π f.val g.val).base '' V.carrier) = V.carrier
⊢ IsUnit
    (↑(TopCat.Presheaf.germ (coequalizer f.val g.val).toPresheafedSpace.presheaf
          { val := ↑(coequalizer.π f.val g.val).base x, property := hU })
      s)
[PROOFSTEP]
have hV' : V = ⟨(coequalizer.π f.1 g.1).base ⁻¹' ((coequalizer.π f.1 g.1).base '' V.1), hV.symm ▸ V.2⟩ :=
  SetLike.ext' hV.symm
[GOAL]
case map_nonunit.intro.intro.intro
X Y : LocallyRingedSpace
f g : X ⟶ Y
U✝ : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace
s✝ : ↑((coequalizer f.val g.val).toPresheafedSpace.presheaf.obj (op U✝))
x : ↑(toTopCat Y)
U : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace
hU : ↑(coequalizer.π f.val g.val).base x ∈ U
s : (forget CommRingCat).obj ((coequalizer f.val g.val).toPresheafedSpace.presheaf.obj (op U))
ha :
  IsUnit
    (↑(TopCat.Presheaf.germ Y.presheaf { val := x, property := hU })
      (↑(NatTrans.app (coequalizer.π f.val g.val).c (op U)) s))
V : Opens ↑(toTopCat Y) := imageBasicOpen f g U s
hV : ↑(coequalizer.π f.val g.val).base ⁻¹' (↑(coequalizer.π f.val g.val).base '' V.carrier) = V.carrier
hV' :
  V =
    { carrier := ↑(coequalizer.π f.val g.val).base ⁻¹' (↑(coequalizer.π f.val g.val).base '' V.carrier),
      is_open' :=
        (_ : IsOpen (↑(coequalizer.π f.val g.val).base ⁻¹' (↑(coequalizer.π f.val g.val).base '' V.carrier))) }
⊢ IsUnit
    (↑(TopCat.Presheaf.germ (coequalizer f.val g.val).toPresheafedSpace.presheaf
          { val := ↑(coequalizer.π f.val g.val).base x, property := hU })
      s)
[PROOFSTEP]
have V_open : IsOpen ((coequalizer.π f.val g.val).base '' V.1) := imageBasicOpen_image_open f g U s
[GOAL]
case map_nonunit.intro.intro.intro
X Y : LocallyRingedSpace
f g : X ⟶ Y
U✝ : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace
s✝ : ↑((coequalizer f.val g.val).toPresheafedSpace.presheaf.obj (op U✝))
x : ↑(toTopCat Y)
U : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace
hU : ↑(coequalizer.π f.val g.val).base x ∈ U
s : (forget CommRingCat).obj ((coequalizer f.val g.val).toPresheafedSpace.presheaf.obj (op U))
ha :
  IsUnit
    (↑(TopCat.Presheaf.germ Y.presheaf { val := x, property := hU })
      (↑(NatTrans.app (coequalizer.π f.val g.val).c (op U)) s))
V : Opens ↑(toTopCat Y) := imageBasicOpen f g U s
hV : ↑(coequalizer.π f.val g.val).base ⁻¹' (↑(coequalizer.π f.val g.val).base '' V.carrier) = V.carrier
hV' :
  V =
    { carrier := ↑(coequalizer.π f.val g.val).base ⁻¹' (↑(coequalizer.π f.val g.val).base '' V.carrier),
      is_open' :=
        (_ : IsOpen (↑(coequalizer.π f.val g.val).base ⁻¹' (↑(coequalizer.π f.val g.val).base '' V.carrier))) }
V_open : IsOpen (↑(coequalizer.π f.val g.val).base '' V.carrier)
⊢ IsUnit
    (↑(TopCat.Presheaf.germ (coequalizer f.val g.val).toPresheafedSpace.presheaf
          { val := ↑(coequalizer.π f.val g.val).base x, property := hU })
      s)
[PROOFSTEP]
have VleU : (⟨(coequalizer.π f.val g.val).base '' V.1, V_open⟩ : TopologicalSpace.Opens _) ≤ U :=
  Set.image_subset_iff.mpr (Y.toRingedSpace.basicOpen_le _)
[GOAL]
case map_nonunit.intro.intro.intro
X Y : LocallyRingedSpace
f g : X ⟶ Y
U✝ : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace
s✝ : ↑((coequalizer f.val g.val).toPresheafedSpace.presheaf.obj (op U✝))
x : ↑(toTopCat Y)
U : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace
hU : ↑(coequalizer.π f.val g.val).base x ∈ U
s : (forget CommRingCat).obj ((coequalizer f.val g.val).toPresheafedSpace.presheaf.obj (op U))
ha :
  IsUnit
    (↑(TopCat.Presheaf.germ Y.presheaf { val := x, property := hU })
      (↑(NatTrans.app (coequalizer.π f.val g.val).c (op U)) s))
V : Opens ↑(toTopCat Y) := imageBasicOpen f g U s
hV : ↑(coequalizer.π f.val g.val).base ⁻¹' (↑(coequalizer.π f.val g.val).base '' V.carrier) = V.carrier
hV' :
  V =
    { carrier := ↑(coequalizer.π f.val g.val).base ⁻¹' (↑(coequalizer.π f.val g.val).base '' V.carrier),
      is_open' :=
        (_ : IsOpen (↑(coequalizer.π f.val g.val).base ⁻¹' (↑(coequalizer.π f.val g.val).base '' V.carrier))) }
V_open : IsOpen (↑(coequalizer.π f.val g.val).base '' V.carrier)
VleU : { carrier := ↑(coequalizer.π f.val g.val).base '' V.carrier, is_open' := V_open } ≤ U
⊢ IsUnit
    (↑(TopCat.Presheaf.germ (coequalizer f.val g.val).toPresheafedSpace.presheaf
          { val := ↑(coequalizer.π f.val g.val).base x, property := hU })
      s)
[PROOFSTEP]
have hxV : x ∈ V := ⟨⟨_, hU⟩, ha, rfl⟩
[GOAL]
case map_nonunit.intro.intro.intro
X Y : LocallyRingedSpace
f g : X ⟶ Y
U✝ : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace
s✝ : ↑((coequalizer f.val g.val).toPresheafedSpace.presheaf.obj (op U✝))
x : ↑(toTopCat Y)
U : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace
hU : ↑(coequalizer.π f.val g.val).base x ∈ U
s : (forget CommRingCat).obj ((coequalizer f.val g.val).toPresheafedSpace.presheaf.obj (op U))
ha :
  IsUnit
    (↑(TopCat.Presheaf.germ Y.presheaf { val := x, property := hU })
      (↑(NatTrans.app (coequalizer.π f.val g.val).c (op U)) s))
V : Opens ↑(toTopCat Y) := imageBasicOpen f g U s
hV : ↑(coequalizer.π f.val g.val).base ⁻¹' (↑(coequalizer.π f.val g.val).base '' V.carrier) = V.carrier
hV' :
  V =
    { carrier := ↑(coequalizer.π f.val g.val).base ⁻¹' (↑(coequalizer.π f.val g.val).base '' V.carrier),
      is_open' :=
        (_ : IsOpen (↑(coequalizer.π f.val g.val).base ⁻¹' (↑(coequalizer.π f.val g.val).base '' V.carrier))) }
V_open : IsOpen (↑(coequalizer.π f.val g.val).base '' V.carrier)
VleU : { carrier := ↑(coequalizer.π f.val g.val).base '' V.carrier, is_open' := V_open } ≤ U
hxV : x ∈ V
⊢ IsUnit
    (↑(TopCat.Presheaf.germ (coequalizer f.val g.val).toPresheafedSpace.presheaf
          { val := ↑(coequalizer.π f.val g.val).base x, property := hU })
      s)
[PROOFSTEP]
erw [←
  (coequalizer f.val g.val).presheaf.germ_res_apply (homOfLE VleU)
    ⟨_, @Set.mem_image_of_mem _ _ (coequalizer.π f.val g.val).base x V.1 hxV⟩ s]
[GOAL]
case map_nonunit.intro.intro.intro
X Y : LocallyRingedSpace
f g : X ⟶ Y
U✝ : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace
s✝ : ↑((coequalizer f.val g.val).toPresheafedSpace.presheaf.obj (op U✝))
x : ↑(toTopCat Y)
U : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace
hU : ↑(coequalizer.π f.val g.val).base x ∈ U
s : (forget CommRingCat).obj ((coequalizer f.val g.val).toPresheafedSpace.presheaf.obj (op U))
ha :
  IsUnit
    (↑(TopCat.Presheaf.germ Y.presheaf { val := x, property := hU })
      (↑(NatTrans.app (coequalizer.π f.val g.val).c (op U)) s))
V : Opens ↑(toTopCat Y) := imageBasicOpen f g U s
hV : ↑(coequalizer.π f.val g.val).base ⁻¹' (↑(coequalizer.π f.val g.val).base '' V.carrier) = V.carrier
hV' :
  V =
    { carrier := ↑(coequalizer.π f.val g.val).base ⁻¹' (↑(coequalizer.π f.val g.val).base '' V.carrier),
      is_open' :=
        (_ : IsOpen (↑(coequalizer.π f.val g.val).base ⁻¹' (↑(coequalizer.π f.val g.val).base '' V.carrier))) }
V_open : IsOpen (↑(coequalizer.π f.val g.val).base '' V.carrier)
VleU : { carrier := ↑(coequalizer.π f.val g.val).base '' V.carrier, is_open' := V_open } ≤ U
hxV : x ∈ V
⊢ IsUnit
    (↑(TopCat.Presheaf.germ (coequalizer f.val g.val).toPresheafedSpace.presheaf
          { val := ↑(coequalizer.π f.val g.val).base x,
            property := (_ : ↑(coequalizer.π f.val g.val).base x ∈ ↑(coequalizer.π f.val g.val).base '' V.carrier) })
      (↑((coequalizer f.val g.val).toPresheafedSpace.presheaf.map (homOfLE VleU).op) s))
[PROOFSTEP]
apply RingHom.isUnit_map
[GOAL]
case map_nonunit.intro.intro.intro.a
X Y : LocallyRingedSpace
f g : X ⟶ Y
U✝ : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace
s✝ : ↑((coequalizer f.val g.val).toPresheafedSpace.presheaf.obj (op U✝))
x : ↑(toTopCat Y)
U : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace
hU : ↑(coequalizer.π f.val g.val).base x ∈ U
s : (forget CommRingCat).obj ((coequalizer f.val g.val).toPresheafedSpace.presheaf.obj (op U))
ha :
  IsUnit
    (↑(TopCat.Presheaf.germ Y.presheaf { val := x, property := hU })
      (↑(NatTrans.app (coequalizer.π f.val g.val).c (op U)) s))
V : Opens ↑(toTopCat Y) := imageBasicOpen f g U s
hV : ↑(coequalizer.π f.val g.val).base ⁻¹' (↑(coequalizer.π f.val g.val).base '' V.carrier) = V.carrier
hV' :
  V =
    { carrier := ↑(coequalizer.π f.val g.val).base ⁻¹' (↑(coequalizer.π f.val g.val).base '' V.carrier),
      is_open' :=
        (_ : IsOpen (↑(coequalizer.π f.val g.val).base ⁻¹' (↑(coequalizer.π f.val g.val).base '' V.carrier))) }
V_open : IsOpen (↑(coequalizer.π f.val g.val).base '' V.carrier)
VleU : { carrier := ↑(coequalizer.π f.val g.val).base '' V.carrier, is_open' := V_open } ≤ U
hxV : x ∈ V
⊢ IsUnit (↑((coequalizer f.val g.val).toPresheafedSpace.presheaf.map (homOfLE VleU).op) s)
[PROOFSTEP]
rw [← isUnit_map_iff ((coequalizer.π f.val g.val : _).c.app _), ← comp_apply, NatTrans.naturality, comp_apply,
  TopCat.Presheaf.pushforwardObj_map, ← isUnit_map_iff (Y.presheaf.map (eqToHom hV').op)]
  -- Porting note : change `rw` to `erw`
[GOAL]
case map_nonunit.intro.intro.intro.a
X Y : LocallyRingedSpace
f g : X ⟶ Y
U✝ : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace
s✝ : ↑((coequalizer f.val g.val).toPresheafedSpace.presheaf.obj (op U✝))
x : ↑(toTopCat Y)
U : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace
hU : ↑(coequalizer.π f.val g.val).base x ∈ U
s : (forget CommRingCat).obj ((coequalizer f.val g.val).toPresheafedSpace.presheaf.obj (op U))
ha :
  IsUnit
    (↑(TopCat.Presheaf.germ Y.presheaf { val := x, property := hU })
      (↑(NatTrans.app (coequalizer.π f.val g.val).c (op U)) s))
V : Opens ↑(toTopCat Y) := imageBasicOpen f g U s
hV : ↑(coequalizer.π f.val g.val).base ⁻¹' (↑(coequalizer.π f.val g.val).base '' V.carrier) = V.carrier
hV' :
  V =
    { carrier := ↑(coequalizer.π f.val g.val).base ⁻¹' (↑(coequalizer.π f.val g.val).base '' V.carrier),
      is_open' :=
        (_ : IsOpen (↑(coequalizer.π f.val g.val).base ⁻¹' (↑(coequalizer.π f.val g.val).base '' V.carrier))) }
V_open : IsOpen (↑(coequalizer.π f.val g.val).base '' V.carrier)
VleU : { carrier := ↑(coequalizer.π f.val g.val).base '' V.carrier, is_open' := V_open } ≤ U
hxV : x ∈ V
⊢ IsUnit
    (↑(Y.presheaf.map (eqToHom hV').op)
      (↑(Y.presheaf.map ((Opens.map (coequalizer.π f.val g.val).base).op.map (homOfLE VleU).op))
        (↑(NatTrans.app (coequalizer.π f.val g.val).c (op U)) s)))
[PROOFSTEP]
erw [← comp_apply, ← comp_apply, Category.assoc, ← Y.presheaf.map_comp]
[GOAL]
case map_nonunit.intro.intro.intro.a
X Y : LocallyRingedSpace
f g : X ⟶ Y
U✝ : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace
s✝ : ↑((coequalizer f.val g.val).toPresheafedSpace.presheaf.obj (op U✝))
x : ↑(toTopCat Y)
U : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace
hU : ↑(coequalizer.π f.val g.val).base x ∈ U
s : (forget CommRingCat).obj ((coequalizer f.val g.val).toPresheafedSpace.presheaf.obj (op U))
ha :
  IsUnit
    (↑(TopCat.Presheaf.germ Y.presheaf { val := x, property := hU })
      (↑(NatTrans.app (coequalizer.π f.val g.val).c (op U)) s))
V : Opens ↑(toTopCat Y) := imageBasicOpen f g U s
hV : ↑(coequalizer.π f.val g.val).base ⁻¹' (↑(coequalizer.π f.val g.val).base '' V.carrier) = V.carrier
hV' :
  V =
    { carrier := ↑(coequalizer.π f.val g.val).base ⁻¹' (↑(coequalizer.π f.val g.val).base '' V.carrier),
      is_open' :=
        (_ : IsOpen (↑(coequalizer.π f.val g.val).base ⁻¹' (↑(coequalizer.π f.val g.val).base '' V.carrier))) }
V_open : IsOpen (↑(coequalizer.π f.val g.val).base '' V.carrier)
VleU : { carrier := ↑(coequalizer.π f.val g.val).base '' V.carrier, is_open' := V_open } ≤ U
hxV : x ∈ V
⊢ IsUnit
    (↑(NatTrans.app (coequalizer.π f.val g.val).c (op U) ≫
          Y.presheaf.map ((Opens.map (coequalizer.π f.val g.val).base).op.map (homOfLE VleU).op ≫ (eqToHom hV').op))
      s)
[PROOFSTEP]
convert @RingedSpace.isUnit_res_basicOpen Y.toRingedSpace (unop _) (((coequalizer.π f.val g.val).c.app (op U)) s)
[GOAL]
X Y : LocallyRingedSpace
f g : X ⟶ Y
x : ↑↑(Limits.coequalizer f.val g.val).toPresheafedSpace
⊢ LocalRing ↑(TopCat.Presheaf.stalk (Limits.coequalizer f.val g.val).toPresheafedSpace.presheaf x)
[PROOFSTEP]
obtain ⟨y, rfl⟩ := (TopCat.epi_iff_surjective (coequalizer.π f.val g.val).base).mp inferInstance x
[GOAL]
case intro
X Y : LocallyRingedSpace
f g : X ⟶ Y
y : (forget TopCat).obj ↑Y.toPresheafedSpace
⊢ LocalRing
    ↑(TopCat.Presheaf.stalk (Limits.coequalizer f.val g.val).toPresheafedSpace.presheaf
        (↑(coequalizer.π f.val g.val).base y))
[PROOFSTEP]
exact (PresheafedSpace.stalkMap (coequalizer.π f.val g.val : _) y).domain_localRing
[GOAL]
X✝ Y✝ : LocallyRingedSpace
f✝ g✝ : X✝ ⟶ Y✝
X Y : RingedSpace
f g : X ⟶ Y
H : f = g
x : ↑↑X.toPresheafedSpace
h : IsLocalRingHom (PresheafedSpace.stalkMap f x)
⊢ IsLocalRingHom (PresheafedSpace.stalkMap g x)
[PROOFSTEP]
rw [PresheafedSpace.stalkMap.congr_hom _ _ H.symm x]
[GOAL]
X✝ Y✝ : LocallyRingedSpace
f✝ g✝ : X✝ ⟶ Y✝
X Y : RingedSpace
f g : X ⟶ Y
H : f = g
x : ↑↑X.toPresheafedSpace
h : IsLocalRingHom (PresheafedSpace.stalkMap f x)
⊢ IsLocalRingHom
    (eqToHom
        (_ :
          PresheafedSpace.stalk Y.toPresheafedSpace (↑g.base x) =
            PresheafedSpace.stalk Y.toPresheafedSpace (↑f.base x)) ≫
      PresheafedSpace.stalkMap f x)
[PROOFSTEP]
infer_instance
[GOAL]
X Y : LocallyRingedSpace
f g : X ⟶ Y
⊢ IsColimit (coequalizerCofork f g)
[PROOFSTEP]
apply Cofork.IsColimit.mk'
[GOAL]
case create
X Y : LocallyRingedSpace
f g : X ⟶ Y
⊢ (s : Cofork f g) →
    { l //
      Cofork.π (coequalizerCofork f g) ≫ l = Cofork.π s ∧
        ∀
          {m :
            ((Functor.const WalkingParallelPair).obj (coequalizerCofork f g).pt).obj WalkingParallelPair.one ⟶
              ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one},
          Cofork.π (coequalizerCofork f g) ≫ m = Cofork.π s → m = l }
[PROOFSTEP]
intro s
[GOAL]
case create
X Y : LocallyRingedSpace
f g : X ⟶ Y
s : Cofork f g
⊢ { l //
    Cofork.π (coequalizerCofork f g) ≫ l = Cofork.π s ∧
      ∀
        {m :
          ((Functor.const WalkingParallelPair).obj (coequalizerCofork f g).pt).obj WalkingParallelPair.one ⟶
            ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one},
        Cofork.π (coequalizerCofork f g) ≫ m = Cofork.π s → m = l }
[PROOFSTEP]
have e : f.val ≫ s.π.val = g.val ≫ s.π.val := by injection s.condition
[GOAL]
X Y : LocallyRingedSpace
f g : X ⟶ Y
s : Cofork f g
⊢ f.val ≫ (Cofork.π s).val = g.val ≫ (Cofork.π s).val
[PROOFSTEP]
injection s.condition
[GOAL]
case create
X Y : LocallyRingedSpace
f g : X ⟶ Y
s : Cofork f g
e : f.val ≫ (Cofork.π s).val = g.val ≫ (Cofork.π s).val
⊢ { l //
    Cofork.π (coequalizerCofork f g) ≫ l = Cofork.π s ∧
      ∀
        {m :
          ((Functor.const WalkingParallelPair).obj (coequalizerCofork f g).pt).obj WalkingParallelPair.one ⟶
            ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one},
        Cofork.π (coequalizerCofork f g) ≫ m = Cofork.π s → m = l }
[PROOFSTEP]
refine ⟨⟨coequalizer.desc s.π.1 e, ?_⟩, ?_⟩
[GOAL]
case create.refine_1
X Y : LocallyRingedSpace
f g : X ⟶ Y
s : Cofork f g
e : f.val ≫ (Cofork.π s).val = g.val ≫ (Cofork.π s).val
⊢ ∀ (x : ↑↑(coequalizerCofork f g).pt.toPresheafedSpace),
    IsLocalRingHom (PresheafedSpace.stalkMap (coequalizer.desc (Cofork.π s).val e) x)
[PROOFSTEP]
intro x
[GOAL]
case create.refine_1
X Y : LocallyRingedSpace
f g : X ⟶ Y
s : Cofork f g
e : f.val ≫ (Cofork.π s).val = g.val ≫ (Cofork.π s).val
x : ↑↑(coequalizerCofork f g).pt.toPresheafedSpace
⊢ IsLocalRingHom (PresheafedSpace.stalkMap (coequalizer.desc (Cofork.π s).val e) x)
[PROOFSTEP]
rcases(TopCat.epi_iff_surjective (coequalizer.π f.val g.val).base).mp inferInstance x with
  ⟨y, rfl⟩
    -- Porting note : was `apply isLocalRingHom_of_comp _ (PresheafedSpace.stalkMap ...)`, this
        -- used to allow you to provide the proof that `... ≫ ...` is a local ring homomorphism later,
        -- but this is no longer possible
[GOAL]
case create.refine_1.intro
X Y : LocallyRingedSpace
f g : X ⟶ Y
s : Cofork f g
e : f.val ≫ (Cofork.π s).val = g.val ≫ (Cofork.π s).val
y : (forget TopCat).obj ↑Y.toPresheafedSpace
⊢ IsLocalRingHom (PresheafedSpace.stalkMap (coequalizer.desc (Cofork.π s).val e) (↑(coequalizer.π f.val g.val).base y))
[PROOFSTEP]
set h := _
[GOAL]
case create.refine_1.intro
X Y : LocallyRingedSpace
f g : X ⟶ Y
s : Cofork f g
e : f.val ≫ (Cofork.π s).val = g.val ≫ (Cofork.π s).val
y : (forget TopCat).obj ↑Y.toPresheafedSpace
h : ?m.154167 := ?m.154168
⊢ IsLocalRingHom (PresheafedSpace.stalkMap (coequalizer.desc (Cofork.π s).val e) (↑(coequalizer.π f.val g.val).base y))
[PROOFSTEP]
change IsLocalRingHom h
[GOAL]
case create.refine_1.intro
X Y : LocallyRingedSpace
f g : X ⟶ Y
s : Cofork f g
e : f.val ≫ (Cofork.π s).val = g.val ≫ (Cofork.π s).val
y : (forget TopCat).obj ↑Y.toPresheafedSpace
h : ↑(PresheafedSpace.stalk s.pt.toPresheafedSpace
      (↑(coequalizer.desc (Cofork.π s).val e).base (↑(coequalizer.π f.val g.val).base y))) →+*
  ↑(PresheafedSpace.stalk (coequalizerCofork f g).pt.toPresheafedSpace (↑(coequalizer.π f.val g.val).base y)) :=
  PresheafedSpace.stalkMap (coequalizer.desc (Cofork.π s).val e) (↑(coequalizer.π f.val g.val).base y)
⊢ IsLocalRingHom h
[PROOFSTEP]
suffices : IsLocalRingHom ((PresheafedSpace.stalkMap (coequalizerCofork f g).π.1 _).comp h)
[GOAL]
case create.refine_1.intro
X Y : LocallyRingedSpace
f g : X ⟶ Y
s : Cofork f g
e : f.val ≫ (Cofork.π s).val = g.val ≫ (Cofork.π s).val
y : (forget TopCat).obj ↑Y.toPresheafedSpace
h : ↑(PresheafedSpace.stalk s.pt.toPresheafedSpace
      (↑(coequalizer.desc (Cofork.π s).val e).base (↑(coequalizer.π f.val g.val).base y))) →+*
  ↑(PresheafedSpace.stalk (coequalizerCofork f g).pt.toPresheafedSpace (↑(coequalizer.π f.val g.val).base y)) :=
  PresheafedSpace.stalkMap (coequalizer.desc (Cofork.π s).val e) (↑(coequalizer.π f.val g.val).base y)
this : IsLocalRingHom (RingHom.comp (PresheafedSpace.stalkMap (Cofork.π (coequalizerCofork f g)).val y) h)
⊢ IsLocalRingHom h
[PROOFSTEP]
apply isLocalRingHom_of_comp _ (PresheafedSpace.stalkMap (coequalizerCofork f g).π.1 _)
[GOAL]
case this
X Y : LocallyRingedSpace
f g : X ⟶ Y
s : Cofork f g
e : f.val ≫ (Cofork.π s).val = g.val ≫ (Cofork.π s).val
y : (forget TopCat).obj ↑Y.toPresheafedSpace
h : ↑(PresheafedSpace.stalk s.pt.toPresheafedSpace
      (↑(coequalizer.desc (Cofork.π s).val e).base (↑(coequalizer.π f.val g.val).base y))) →+*
  ↑(PresheafedSpace.stalk (coequalizerCofork f g).pt.toPresheafedSpace (↑(coequalizer.π f.val g.val).base y)) :=
  PresheafedSpace.stalkMap (coequalizer.desc (Cofork.π s).val e) (↑(coequalizer.π f.val g.val).base y)
⊢ IsLocalRingHom (RingHom.comp (PresheafedSpace.stalkMap (Cofork.π (coequalizerCofork f g)).val y) h)
[PROOFSTEP]
change IsLocalRingHom (_ ≫ PresheafedSpace.stalkMap (coequalizerCofork f g).π.val y)
[GOAL]
case this
X Y : LocallyRingedSpace
f g : X ⟶ Y
s : Cofork f g
e : f.val ≫ (Cofork.π s).val = g.val ≫ (Cofork.π s).val
y : (forget TopCat).obj ↑Y.toPresheafedSpace
h : ↑(PresheafedSpace.stalk s.pt.toPresheafedSpace
      (↑(coequalizer.desc (Cofork.π s).val e).base (↑(coequalizer.π f.val g.val).base y))) →+*
  ↑(PresheafedSpace.stalk (coequalizerCofork f g).pt.toPresheafedSpace (↑(coequalizer.π f.val g.val).base y)) :=
  PresheafedSpace.stalkMap (coequalizer.desc (Cofork.π s).val e) (↑(coequalizer.π f.val g.val).base y)
⊢ IsLocalRingHom (h ≫ PresheafedSpace.stalkMap (Cofork.π (coequalizerCofork f g)).val y)
[PROOFSTEP]
erw [← PresheafedSpace.stalkMap.comp]
[GOAL]
case this
X Y : LocallyRingedSpace
f g : X ⟶ Y
s : Cofork f g
e : f.val ≫ (Cofork.π s).val = g.val ≫ (Cofork.π s).val
y : (forget TopCat).obj ↑Y.toPresheafedSpace
h : ↑(PresheafedSpace.stalk s.pt.toPresheafedSpace
      (↑(coequalizer.desc (Cofork.π s).val e).base (↑(coequalizer.π f.val g.val).base y))) →+*
  ↑(PresheafedSpace.stalk (coequalizerCofork f g).pt.toPresheafedSpace (↑(coequalizer.π f.val g.val).base y)) :=
  PresheafedSpace.stalkMap (coequalizer.desc (Cofork.π s).val e) (↑(coequalizer.π f.val g.val).base y)
⊢ IsLocalRingHom (PresheafedSpace.stalkMap (coequalizer.π f.val g.val ≫ coequalizer.desc (Cofork.π s).val e) y)
[PROOFSTEP]
apply isLocalRingHom_stalkMap_congr _ _ (coequalizer.π_desc s.π.1 e).symm y
[GOAL]
case this
X Y : LocallyRingedSpace
f g : X ⟶ Y
s : Cofork f g
e : f.val ≫ (Cofork.π s).val = g.val ≫ (Cofork.π s).val
y : (forget TopCat).obj ↑Y.toPresheafedSpace
h : ↑(PresheafedSpace.stalk s.pt.toPresheafedSpace
      (↑(coequalizer.desc (Cofork.π s).val e).base (↑(coequalizer.π f.val g.val).base y))) →+*
  ↑(PresheafedSpace.stalk (coequalizerCofork f g).pt.toPresheafedSpace (↑(coequalizer.π f.val g.val).base y)) :=
  PresheafedSpace.stalkMap (coequalizer.desc (Cofork.π s).val e) (↑(coequalizer.π f.val g.val).base y)
⊢ IsLocalRingHom (PresheafedSpace.stalkMap (Cofork.π s).val y)
[PROOFSTEP]
infer_instance
[GOAL]
case create.refine_2
X Y : LocallyRingedSpace
f g : X ⟶ Y
s : Cofork f g
e : f.val ≫ (Cofork.π s).val = g.val ≫ (Cofork.π s).val
⊢ Cofork.π (coequalizerCofork f g) ≫
        { val := coequalizer.desc (Cofork.π s).val e,
          prop :=
            (_ :
              ∀ (x : ↑↑(coequalizerCofork f g).pt.toPresheafedSpace),
                IsLocalRingHom (PresheafedSpace.stalkMap (coequalizer.desc (Cofork.π s).val e) x)) } =
      Cofork.π s ∧
    ∀
      {m :
        ((Functor.const WalkingParallelPair).obj (coequalizerCofork f g).pt).obj WalkingParallelPair.one ⟶
          ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one},
      Cofork.π (coequalizerCofork f g) ≫ m = Cofork.π s →
        m =
          { val := coequalizer.desc (Cofork.π s).val e,
            prop :=
              (_ :
                ∀ (x : ↑↑(coequalizerCofork f g).pt.toPresheafedSpace),
                  IsLocalRingHom (PresheafedSpace.stalkMap (coequalizer.desc (Cofork.π s).val e) x)) }
[PROOFSTEP]
constructor
[GOAL]
case create.refine_2.left
X Y : LocallyRingedSpace
f g : X ⟶ Y
s : Cofork f g
e : f.val ≫ (Cofork.π s).val = g.val ≫ (Cofork.π s).val
⊢ Cofork.π (coequalizerCofork f g) ≫
      { val := coequalizer.desc (Cofork.π s).val e,
        prop :=
          (_ :
            ∀ (x : ↑↑(coequalizerCofork f g).pt.toPresheafedSpace),
              IsLocalRingHom (PresheafedSpace.stalkMap (coequalizer.desc (Cofork.π s).val e) x)) } =
    Cofork.π s
[PROOFSTEP]
exact LocallyRingedSpace.Hom.ext _ _ (coequalizer.π_desc _ _)
[GOAL]
case create.refine_2.right
X Y : LocallyRingedSpace
f g : X ⟶ Y
s : Cofork f g
e : f.val ≫ (Cofork.π s).val = g.val ≫ (Cofork.π s).val
⊢ ∀
    {m :
      ((Functor.const WalkingParallelPair).obj (coequalizerCofork f g).pt).obj WalkingParallelPair.one ⟶
        ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one},
    Cofork.π (coequalizerCofork f g) ≫ m = Cofork.π s →
      m =
        { val := coequalizer.desc (Cofork.π s).val e,
          prop :=
            (_ :
              ∀ (x : ↑↑(coequalizerCofork f g).pt.toPresheafedSpace),
                IsLocalRingHom (PresheafedSpace.stalkMap (coequalizer.desc (Cofork.π s).val e) x)) }
[PROOFSTEP]
intro m h
[GOAL]
case create.refine_2.right
X Y : LocallyRingedSpace
f g : X ⟶ Y
s : Cofork f g
e : f.val ≫ (Cofork.π s).val = g.val ≫ (Cofork.π s).val
m :
  ((Functor.const WalkingParallelPair).obj (coequalizerCofork f g).pt).obj WalkingParallelPair.one ⟶
    ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
h : Cofork.π (coequalizerCofork f g) ≫ m = Cofork.π s
⊢ m =
    { val := coequalizer.desc (Cofork.π s).val e,
      prop :=
        (_ :
          ∀ (x : ↑↑(coequalizerCofork f g).pt.toPresheafedSpace),
            IsLocalRingHom (PresheafedSpace.stalkMap (coequalizer.desc (Cofork.π s).val e) x)) }
[PROOFSTEP]
replace h : (coequalizerCofork f g).π.1 ≫ m.1 = s.π.1 := by rw [← h]; rfl
[GOAL]
X Y : LocallyRingedSpace
f g : X ⟶ Y
s : Cofork f g
e : f.val ≫ (Cofork.π s).val = g.val ≫ (Cofork.π s).val
m :
  ((Functor.const WalkingParallelPair).obj (coequalizerCofork f g).pt).obj WalkingParallelPair.one ⟶
    ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
h : Cofork.π (coequalizerCofork f g) ≫ m = Cofork.π s
⊢ (Cofork.π (coequalizerCofork f g)).val ≫ m.val = (Cofork.π s).val
[PROOFSTEP]
rw [← h]
[GOAL]
X Y : LocallyRingedSpace
f g : X ⟶ Y
s : Cofork f g
e : f.val ≫ (Cofork.π s).val = g.val ≫ (Cofork.π s).val
m :
  ((Functor.const WalkingParallelPair).obj (coequalizerCofork f g).pt).obj WalkingParallelPair.one ⟶
    ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
h : Cofork.π (coequalizerCofork f g) ≫ m = Cofork.π s
⊢ (Cofork.π (coequalizerCofork f g)).val ≫ m.val = (Cofork.π (coequalizerCofork f g) ≫ m).val
[PROOFSTEP]
rfl
[GOAL]
case create.refine_2.right
X Y : LocallyRingedSpace
f g : X ⟶ Y
s : Cofork f g
e : f.val ≫ (Cofork.π s).val = g.val ≫ (Cofork.π s).val
m :
  ((Functor.const WalkingParallelPair).obj (coequalizerCofork f g).pt).obj WalkingParallelPair.one ⟶
    ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
h : (Cofork.π (coequalizerCofork f g)).val ≫ m.val = (Cofork.π s).val
⊢ m =
    { val := coequalizer.desc (Cofork.π s).val e,
      prop :=
        (_ :
          ∀ (x : ↑↑(coequalizerCofork f g).pt.toPresheafedSpace),
            IsLocalRingHom (PresheafedSpace.stalkMap (coequalizer.desc (Cofork.π s).val e) x)) }
[PROOFSTEP]
apply LocallyRingedSpace.Hom.ext
[GOAL]
case create.refine_2.right.val
X Y : LocallyRingedSpace
f g : X ⟶ Y
s : Cofork f g
e : f.val ≫ (Cofork.π s).val = g.val ≫ (Cofork.π s).val
m :
  ((Functor.const WalkingParallelPair).obj (coequalizerCofork f g).pt).obj WalkingParallelPair.one ⟶
    ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
h : (Cofork.π (coequalizerCofork f g)).val ≫ m.val = (Cofork.π s).val
⊢ m.val =
    { val := coequalizer.desc (Cofork.π s).val e,
        prop :=
          (_ :
            ∀ (x : ↑↑(coequalizerCofork f g).pt.toPresheafedSpace),
              IsLocalRingHom (PresheafedSpace.stalkMap (coequalizer.desc (Cofork.π s).val e) x)) }.val
[PROOFSTEP]
apply (colimit.isColimit (parallelPair f.1 g.1)).uniq (Cofork.ofπ s.π.1 e) m.1
[GOAL]
case create.refine_2.right.val
X Y : LocallyRingedSpace
f g : X ⟶ Y
s : Cofork f g
e : f.val ≫ (Cofork.π s).val = g.val ≫ (Cofork.π s).val
m :
  ((Functor.const WalkingParallelPair).obj (coequalizerCofork f g).pt).obj WalkingParallelPair.one ⟶
    ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
h : (Cofork.π (coequalizerCofork f g)).val ≫ m.val = (Cofork.π s).val
⊢ ∀ (j : WalkingParallelPair),
    NatTrans.app (colimit.cocone (parallelPair f.val g.val)).ι j ≫ m.val =
      NatTrans.app (Cofork.ofπ (Cofork.π s).val e).ι j
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
case create.refine_2.right.val.zero
X Y : LocallyRingedSpace
f g : X ⟶ Y
s : Cofork f g
e : f.val ≫ (Cofork.π s).val = g.val ≫ (Cofork.π s).val
m :
  ((Functor.const WalkingParallelPair).obj (coequalizerCofork f g).pt).obj WalkingParallelPair.one ⟶
    ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
h : (Cofork.π (coequalizerCofork f g)).val ≫ m.val = (Cofork.π s).val
⊢ NatTrans.app (colimit.cocone (parallelPair f.val g.val)).ι WalkingParallelPair.zero ≫ m.val =
    NatTrans.app (Cofork.ofπ (Cofork.π s).val e).ι WalkingParallelPair.zero
[PROOFSTEP]
rw [← (colimit.cocone (parallelPair f.val g.val)).w WalkingParallelPairHom.left, Category.assoc]
[GOAL]
case create.refine_2.right.val.zero
X Y : LocallyRingedSpace
f g : X ⟶ Y
s : Cofork f g
e : f.val ≫ (Cofork.π s).val = g.val ≫ (Cofork.π s).val
m :
  ((Functor.const WalkingParallelPair).obj (coequalizerCofork f g).pt).obj WalkingParallelPair.one ⟶
    ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
h : (Cofork.π (coequalizerCofork f g)).val ≫ m.val = (Cofork.π s).val
⊢ (parallelPair f.val g.val).map WalkingParallelPairHom.left ≫
      NatTrans.app (colimit.cocone (parallelPair f.val g.val)).ι WalkingParallelPair.one ≫ m.val =
    NatTrans.app (Cofork.ofπ (Cofork.π s).val e).ι WalkingParallelPair.zero
[PROOFSTEP]
change _ ≫ _ ≫ _ = _ ≫ _
[GOAL]
case create.refine_2.right.val.zero
X Y : LocallyRingedSpace
f g : X ⟶ Y
s : Cofork f g
e : f.val ≫ (Cofork.π s).val = g.val ≫ (Cofork.π s).val
m :
  ((Functor.const WalkingParallelPair).obj (coequalizerCofork f g).pt).obj WalkingParallelPair.one ⟶
    ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
h : (Cofork.π (coequalizerCofork f g)).val ≫ m.val = (Cofork.π s).val
⊢ (parallelPair f.val g.val).map WalkingParallelPairHom.left ≫
      NatTrans.app (colimit.cocone (parallelPair f.val g.val)).ι WalkingParallelPair.one ≫ m.val =
    f.val ≫ (Cofork.π s).val
[PROOFSTEP]
congr
[GOAL]
case create.refine_2.right.val.one
X Y : LocallyRingedSpace
f g : X ⟶ Y
s : Cofork f g
e : f.val ≫ (Cofork.π s).val = g.val ≫ (Cofork.π s).val
m :
  ((Functor.const WalkingParallelPair).obj (coequalizerCofork f g).pt).obj WalkingParallelPair.one ⟶
    ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
h : (Cofork.π (coequalizerCofork f g)).val ≫ m.val = (Cofork.π s).val
⊢ NatTrans.app (colimit.cocone (parallelPair f.val g.val)).ι WalkingParallelPair.one ≫ m.val =
    NatTrans.app (Cofork.ofπ (Cofork.π s).val e).ι WalkingParallelPair.one
[PROOFSTEP]
exact h
[GOAL]
X Y : LocallyRingedSpace
f g : X ⟶ Y
F : WalkingParallelPair ⥤ LocallyRingedSpace
⊢ PreservesColimit F forgetToSheafedSpace
[PROOFSTEP]
suffices :
  PreservesColimit (parallelPair (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right))
    forgetToSheafedSpace
[GOAL]
X Y : LocallyRingedSpace
f g : X ⟶ Y
F : WalkingParallelPair ⥤ LocallyRingedSpace
this :
  PreservesColimit (parallelPair (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right))
    forgetToSheafedSpace
⊢ PreservesColimit F forgetToSheafedSpace
[PROOFSTEP]
apply preservesColimitOfIsoDiagram _ (diagramIsoParallelPair F).symm
[GOAL]
case this
X Y : LocallyRingedSpace
f g : X ⟶ Y
F : WalkingParallelPair ⥤ LocallyRingedSpace
⊢ PreservesColimit (parallelPair (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right))
    forgetToSheafedSpace
[PROOFSTEP]
apply preservesColimitOfPreservesColimitCocone (coequalizerCoforkIsColimit _ _)
[GOAL]
case this
X Y : LocallyRingedSpace
f g : X ⟶ Y
F : WalkingParallelPair ⥤ LocallyRingedSpace
⊢ IsColimit
    (forgetToSheafedSpace.mapCocone
      (coequalizerCofork (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right)))
[PROOFSTEP]
apply (isColimitMapCoconeCoforkEquiv _ _).symm _
[GOAL]
X Y : LocallyRingedSpace
f g : X ⟶ Y
F : WalkingParallelPair ⥤ LocallyRingedSpace
⊢ IsColimit
    (Cofork.ofπ
      (forgetToSheafedSpace.map
        { val := coequalizer.π (F.map WalkingParallelPairHom.left).val (F.map WalkingParallelPairHom.right).val,
          prop :=
            (_ :
              ∀ (x : ↑(toTopCat (F.obj WalkingParallelPair.one))),
                IsLocalRingHom
                  (PresheafedSpace.stalkMap
                    (coequalizer.π (F.map WalkingParallelPairHom.left).val (F.map WalkingParallelPairHom.right).val)
                    x)) })
      (_ :
        forgetToSheafedSpace.map (F.map WalkingParallelPairHom.left) ≫
            forgetToSheafedSpace.map
              { val := coequalizer.π (F.map WalkingParallelPairHom.left).val (F.map WalkingParallelPairHom.right).val,
                prop :=
                  (_ :
                    ∀ (x : ↑(toTopCat (F.obj WalkingParallelPair.one))),
                      IsLocalRingHom
                        (PresheafedSpace.stalkMap
                          (coequalizer.π (F.map WalkingParallelPairHom.left).val
                            (F.map WalkingParallelPairHom.right).val)
                          x)) } =
          forgetToSheafedSpace.map (F.map WalkingParallelPairHom.right) ≫
            forgetToSheafedSpace.map
              { val := coequalizer.π (F.map WalkingParallelPairHom.left).val (F.map WalkingParallelPairHom.right).val,
                prop :=
                  (_ :
                    ∀ (x : ↑(toTopCat (F.obj WalkingParallelPair.one))),
                      IsLocalRingHom
                        (PresheafedSpace.stalkMap
                          (coequalizer.π (F.map WalkingParallelPairHom.left).val
                            (F.map WalkingParallelPairHom.right).val)
                          x)) }))
[PROOFSTEP]
dsimp only [forgetToSheafedSpace]
[GOAL]
X Y : LocallyRingedSpace
f g : X ⟶ Y
F : WalkingParallelPair ⥤ LocallyRingedSpace
⊢ IsColimit
    (Cofork.ofπ (coequalizer.π (F.map WalkingParallelPairHom.left).val (F.map WalkingParallelPairHom.right).val)
      (_ :
        (F.map WalkingParallelPairHom.left).val ≫
            coequalizer.π (F.map WalkingParallelPairHom.left).val (F.map WalkingParallelPairHom.right).val =
          (F.map WalkingParallelPairHom.right).val ≫
            coequalizer.π (F.map WalkingParallelPairHom.left).val (F.map WalkingParallelPairHom.right).val))
[PROOFSTEP]
exact coequalizerIsCoequalizer _ _


[GOAL]
L : Language
M : Type u_1
inst✝ : Structure L M
N : Substructure L M
⊢ (∃ S, Set.Finite S ∧ LowerAdjoint.toFun (closure L) S = N) → FG N
[PROOFSTEP]
rintro ⟨t', h, rfl⟩
[GOAL]
case intro.intro
L : Language
M : Type u_1
inst✝ : Structure L M
t' : Set M
h : Set.Finite t'
⊢ FG (LowerAdjoint.toFun (closure L) t')
[PROOFSTEP]
rcases Finite.exists_finset_coe h with ⟨t, rfl⟩
[GOAL]
case intro.intro.intro
L : Language
M : Type u_1
inst✝ : Structure L M
t : Finset M
h : Set.Finite ↑t
⊢ FG (LowerAdjoint.toFun (closure L) ↑t)
[PROOFSTEP]
exact ⟨t, rfl⟩
[GOAL]
L : Language
M : Type u_1
inst✝ : Structure L M
N : Substructure L M
⊢ FG N ↔ ∃ n s, LowerAdjoint.toFun (closure L) (range s) = N
[PROOFSTEP]
rw [fg_def]
[GOAL]
L : Language
M : Type u_1
inst✝ : Structure L M
N : Substructure L M
⊢ (∃ S, Set.Finite S ∧ LowerAdjoint.toFun (closure L) S = N) ↔ ∃ n s, LowerAdjoint.toFun (closure L) (range s) = N
[PROOFSTEP]
constructor
[GOAL]
case mp
L : Language
M : Type u_1
inst✝ : Structure L M
N : Substructure L M
⊢ (∃ S, Set.Finite S ∧ LowerAdjoint.toFun (closure L) S = N) → ∃ n s, LowerAdjoint.toFun (closure L) (range s) = N
[PROOFSTEP]
rintro ⟨S, Sfin, hS⟩
[GOAL]
case mp.intro.intro
L : Language
M : Type u_1
inst✝ : Structure L M
N : Substructure L M
S : Set M
Sfin : Set.Finite S
hS : LowerAdjoint.toFun (closure L) S = N
⊢ ∃ n s, LowerAdjoint.toFun (closure L) (range s) = N
[PROOFSTEP]
obtain ⟨n, f, rfl⟩ := Sfin.fin_embedding
[GOAL]
case mp.intro.intro.intro.intro
L : Language
M : Type u_1
inst✝ : Structure L M
N : Substructure L M
n : ℕ
f : Fin n ↪ M
Sfin : Set.Finite (range ↑f)
hS : LowerAdjoint.toFun (closure L) (range ↑f) = N
⊢ ∃ n s, LowerAdjoint.toFun (closure L) (range s) = N
[PROOFSTEP]
exact ⟨n, f, hS⟩
[GOAL]
case mpr
L : Language
M : Type u_1
inst✝ : Structure L M
N : Substructure L M
⊢ (∃ n s, LowerAdjoint.toFun (closure L) (range s) = N) → ∃ S, Set.Finite S ∧ LowerAdjoint.toFun (closure L) S = N
[PROOFSTEP]
rintro ⟨n, s, hs⟩
[GOAL]
case mpr.intro.intro
L : Language
M : Type u_1
inst✝ : Structure L M
N : Substructure L M
n : ℕ
s : Fin n → M
hs : LowerAdjoint.toFun (closure L) (range s) = N
⊢ ∃ S, Set.Finite S ∧ LowerAdjoint.toFun (closure L) S = N
[PROOFSTEP]
refine' ⟨range s, finite_range s, hs⟩
[GOAL]
L : Language
M : Type u_1
inst✝ : Structure L M
⊢ LowerAdjoint.toFun (closure L) ↑∅ = ⊥
[PROOFSTEP]
rw [Finset.coe_empty, closure_empty]
[GOAL]
L : Language
M : Type u_1
inst✝ : Structure L M
s : Set M
hs : Set.Finite s
⊢ LowerAdjoint.toFun (closure L) ↑(Finite.toFinset hs) = LowerAdjoint.toFun (closure L) s
[PROOFSTEP]
rw [hs.coe_toFinset]
[GOAL]
L : Language
M : Type u_1
inst✝ : Structure L M
N₁ N₂ : Substructure L M
hN₁ : FG N₁
hN₂ : FG N₂
t₁ : Set M
ht₁ : Set.Finite t₁ ∧ LowerAdjoint.toFun (closure L) t₁ = N₁
t₂ : Set M
ht₂ : Set.Finite t₂ ∧ LowerAdjoint.toFun (closure L) t₂ = N₂
⊢ LowerAdjoint.toFun (closure L) (t₁ ∪ t₂) = N₁ ⊔ N₂
[PROOFSTEP]
rw [closure_union, ht₁.2, ht₂.2]
[GOAL]
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
inst✝ : Structure L N
f : M →[L] N
s : Substructure L M
hs : FG s
t : Set M
ht : Set.Finite t ∧ LowerAdjoint.toFun (closure L) t = s
⊢ LowerAdjoint.toFun (closure L) (↑f '' t) = Substructure.map f s
[PROOFSTEP]
rw [closure_image, ht.2]
[GOAL]
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
inst✝ : Structure L N
f : M ↪[L] N
s : Substructure L M
hs : FG (Substructure.map (Embedding.toHom f) s)
⊢ FG s
[PROOFSTEP]
rcases hs with ⟨t, h⟩
[GOAL]
case intro
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
inst✝ : Structure L N
f : M ↪[L] N
s : Substructure L M
t : Finset N
h : LowerAdjoint.toFun (closure L) ↑t = Substructure.map (Embedding.toHom f) s
⊢ FG s
[PROOFSTEP]
rw [fg_def]
[GOAL]
case intro
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
inst✝ : Structure L N
f : M ↪[L] N
s : Substructure L M
t : Finset N
h : LowerAdjoint.toFun (closure L) ↑t = Substructure.map (Embedding.toHom f) s
⊢ ∃ S, Set.Finite S ∧ LowerAdjoint.toFun (closure L) S = s
[PROOFSTEP]
refine' ⟨f ⁻¹' t, t.finite_toSet.preimage (f.injective.injOn _), _⟩
[GOAL]
case intro
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
inst✝ : Structure L N
f : M ↪[L] N
s : Substructure L M
t : Finset N
h : LowerAdjoint.toFun (closure L) ↑t = Substructure.map (Embedding.toHom f) s
⊢ LowerAdjoint.toFun (closure L) (↑f ⁻¹' ↑t) = s
[PROOFSTEP]
have hf : Function.Injective f.toHom := f.injective
[GOAL]
case intro
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
inst✝ : Structure L N
f : M ↪[L] N
s : Substructure L M
t : Finset N
h : LowerAdjoint.toFun (closure L) ↑t = Substructure.map (Embedding.toHom f) s
hf : Function.Injective ↑(Embedding.toHom f)
⊢ LowerAdjoint.toFun (closure L) (↑f ⁻¹' ↑t) = s
[PROOFSTEP]
refine' map_injective_of_injective hf _
[GOAL]
case intro
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
inst✝ : Structure L N
f : M ↪[L] N
s : Substructure L M
t : Finset N
h : LowerAdjoint.toFun (closure L) ↑t = Substructure.map (Embedding.toHom f) s
hf : Function.Injective ↑(Embedding.toHom f)
⊢ Substructure.map (Embedding.toHom f) (LowerAdjoint.toFun (closure L) (↑f ⁻¹' ↑t)) =
    Substructure.map (Embedding.toHom f) s
[PROOFSTEP]
rw [← h, map_closure, Embedding.coe_toHom, image_preimage_eq_of_subset]
[GOAL]
case intro
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
inst✝ : Structure L N
f : M ↪[L] N
s : Substructure L M
t : Finset N
h : LowerAdjoint.toFun (closure L) ↑t = Substructure.map (Embedding.toHom f) s
hf : Function.Injective ↑(Embedding.toHom f)
⊢ ↑t ⊆ range ↑f
[PROOFSTEP]
intro x hx
[GOAL]
case intro
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
inst✝ : Structure L N
f : M ↪[L] N
s : Substructure L M
t : Finset N
h : LowerAdjoint.toFun (closure L) ↑t = Substructure.map (Embedding.toHom f) s
hf : Function.Injective ↑(Embedding.toHom f)
x : N
hx : x ∈ ↑t
⊢ x ∈ range ↑f
[PROOFSTEP]
have h' := subset_closure (L := L) hx
[GOAL]
case intro
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
inst✝ : Structure L N
f : M ↪[L] N
s : Substructure L M
t : Finset N
h : LowerAdjoint.toFun (closure L) ↑t = Substructure.map (Embedding.toHom f) s
hf : Function.Injective ↑(Embedding.toHom f)
x : N
hx : x ∈ ↑t
h' : x ∈ ↑(LowerAdjoint.toFun (closure L) ↑t)
⊢ x ∈ range ↑f
[PROOFSTEP]
rw [h] at h'
[GOAL]
case intro
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
inst✝ : Structure L N
f : M ↪[L] N
s : Substructure L M
t : Finset N
h : LowerAdjoint.toFun (closure L) ↑t = Substructure.map (Embedding.toHom f) s
hf : Function.Injective ↑(Embedding.toHom f)
x : N
hx : x ∈ ↑t
h' : x ∈ ↑(Substructure.map (Embedding.toHom f) s)
⊢ x ∈ range ↑f
[PROOFSTEP]
exact Hom.map_le_range h'
[GOAL]
L : Language
M : Type u_1
inst✝ : Structure L M
N : Substructure L M
h : FG N
⊢ CG N
[PROOFSTEP]
obtain ⟨s, hf, rfl⟩ := fg_def.1 h
[GOAL]
case intro.intro
L : Language
M : Type u_1
inst✝ : Structure L M
s : Set M
hf : Set.Finite s
h : FG (LowerAdjoint.toFun (closure L) s)
⊢ CG (LowerAdjoint.toFun (closure L) s)
[PROOFSTEP]
refine' ⟨s, hf.countable, rfl⟩
[GOAL]
L : Language
M : Type u_1
inst✝ : Structure L M
N : Substructure L M
⊢ CG N ↔ ↑N = ∅ ∨ ∃ s, LowerAdjoint.toFun (closure L) (range s) = N
[PROOFSTEP]
rw [cg_def]
[GOAL]
L : Language
M : Type u_1
inst✝ : Structure L M
N : Substructure L M
⊢ (∃ S, Set.Countable S ∧ LowerAdjoint.toFun (closure L) S = N) ↔
    ↑N = ∅ ∨ ∃ s, LowerAdjoint.toFun (closure L) (range s) = N
[PROOFSTEP]
constructor
[GOAL]
case mp
L : Language
M : Type u_1
inst✝ : Structure L M
N : Substructure L M
⊢ (∃ S, Set.Countable S ∧ LowerAdjoint.toFun (closure L) S = N) →
    ↑N = ∅ ∨ ∃ s, LowerAdjoint.toFun (closure L) (range s) = N
[PROOFSTEP]
rintro ⟨S, Scount, hS⟩
[GOAL]
case mp.intro.intro
L : Language
M : Type u_1
inst✝ : Structure L M
N : Substructure L M
S : Set M
Scount : Set.Countable S
hS : LowerAdjoint.toFun (closure L) S = N
⊢ ↑N = ∅ ∨ ∃ s, LowerAdjoint.toFun (closure L) (range s) = N
[PROOFSTEP]
cases' eq_empty_or_nonempty (N : Set M) with h h
[GOAL]
case mp.intro.intro.inl
L : Language
M : Type u_1
inst✝ : Structure L M
N : Substructure L M
S : Set M
Scount : Set.Countable S
hS : LowerAdjoint.toFun (closure L) S = N
h : ↑N = ∅
⊢ ↑N = ∅ ∨ ∃ s, LowerAdjoint.toFun (closure L) (range s) = N
[PROOFSTEP]
exact Or.intro_left _ h
[GOAL]
case mp.intro.intro.inr
L : Language
M : Type u_1
inst✝ : Structure L M
N : Substructure L M
S : Set M
Scount : Set.Countable S
hS : LowerAdjoint.toFun (closure L) S = N
h : Set.Nonempty ↑N
⊢ ↑N = ∅ ∨ ∃ s, LowerAdjoint.toFun (closure L) (range s) = N
[PROOFSTEP]
obtain ⟨f, h'⟩ := (Scount.union (Set.countable_singleton h.some)).exists_eq_range (singleton_nonempty h.some).inr
[GOAL]
case mp.intro.intro.inr.intro
L : Language
M : Type u_1
inst✝ : Structure L M
N : Substructure L M
S : Set M
Scount : Set.Countable S
hS : LowerAdjoint.toFun (closure L) S = N
h : Set.Nonempty ↑N
f : ℕ → M
h' : S ∪ {Set.Nonempty.some h} = range f
⊢ ↑N = ∅ ∨ ∃ s, LowerAdjoint.toFun (closure L) (range s) = N
[PROOFSTEP]
refine' Or.intro_right _ ⟨f, _⟩
[GOAL]
case mp.intro.intro.inr.intro
L : Language
M : Type u_1
inst✝ : Structure L M
N : Substructure L M
S : Set M
Scount : Set.Countable S
hS : LowerAdjoint.toFun (closure L) S = N
h : Set.Nonempty ↑N
f : ℕ → M
h' : S ∪ {Set.Nonempty.some h} = range f
⊢ LowerAdjoint.toFun (closure L) (range f) = N
[PROOFSTEP]
rw [← h', closure_union, hS, sup_eq_left, closure_le]
[GOAL]
case mp.intro.intro.inr.intro
L : Language
M : Type u_1
inst✝ : Structure L M
N : Substructure L M
S : Set M
Scount : Set.Countable S
hS : LowerAdjoint.toFun (closure L) S = N
h : Set.Nonempty ↑N
f : ℕ → M
h' : S ∪ {Set.Nonempty.some h} = range f
⊢ {Set.Nonempty.some h} ⊆ ↑N
[PROOFSTEP]
exact singleton_subset_iff.2 h.some_mem
[GOAL]
case mpr
L : Language
M : Type u_1
inst✝ : Structure L M
N : Substructure L M
⊢ (↑N = ∅ ∨ ∃ s, LowerAdjoint.toFun (closure L) (range s) = N) →
    ∃ S, Set.Countable S ∧ LowerAdjoint.toFun (closure L) S = N
[PROOFSTEP]
intro h
[GOAL]
case mpr
L : Language
M : Type u_1
inst✝ : Structure L M
N : Substructure L M
h : ↑N = ∅ ∨ ∃ s, LowerAdjoint.toFun (closure L) (range s) = N
⊢ ∃ S, Set.Countable S ∧ LowerAdjoint.toFun (closure L) S = N
[PROOFSTEP]
cases' h with h h
[GOAL]
case mpr.inl
L : Language
M : Type u_1
inst✝ : Structure L M
N : Substructure L M
h : ↑N = ∅
⊢ ∃ S, Set.Countable S ∧ LowerAdjoint.toFun (closure L) S = N
[PROOFSTEP]
refine' ⟨∅, countable_empty, closure_eq_of_le (empty_subset _) _⟩
[GOAL]
case mpr.inl
L : Language
M : Type u_1
inst✝ : Structure L M
N : Substructure L M
h : ↑N = ∅
⊢ N ≤ LowerAdjoint.toFun (closure L) ∅
[PROOFSTEP]
rw [← SetLike.coe_subset_coe, h]
[GOAL]
case mpr.inl
L : Language
M : Type u_1
inst✝ : Structure L M
N : Substructure L M
h : ↑N = ∅
⊢ ∅ ⊆ ↑(LowerAdjoint.toFun (closure L) ∅)
[PROOFSTEP]
exact empty_subset _
[GOAL]
case mpr.inr
L : Language
M : Type u_1
inst✝ : Structure L M
N : Substructure L M
h : ∃ s, LowerAdjoint.toFun (closure L) (range s) = N
⊢ ∃ S, Set.Countable S ∧ LowerAdjoint.toFun (closure L) S = N
[PROOFSTEP]
obtain ⟨f, rfl⟩ := h
[GOAL]
case mpr.inr.intro
L : Language
M : Type u_1
inst✝ : Structure L M
f : ℕ → M
⊢ ∃ S, Set.Countable S ∧ LowerAdjoint.toFun (closure L) S = LowerAdjoint.toFun (closure L) (range f)
[PROOFSTEP]
exact ⟨range f, countable_range _, rfl⟩
[GOAL]
L : Language
M : Type u_1
inst✝ : Structure L M
N₁ N₂ : Substructure L M
hN₁ : CG N₁
hN₂ : CG N₂
t₁ : Set M
ht₁ : Set.Countable t₁ ∧ LowerAdjoint.toFun (closure L) t₁ = N₁
t₂ : Set M
ht₂ : Set.Countable t₂ ∧ LowerAdjoint.toFun (closure L) t₂ = N₂
⊢ LowerAdjoint.toFun (closure L) (t₁ ∪ t₂) = N₁ ⊔ N₂
[PROOFSTEP]
rw [closure_union, ht₁.2, ht₂.2]
[GOAL]
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
inst✝ : Structure L N
f : M →[L] N
s : Substructure L M
hs : CG s
t : Set M
ht : Set.Countable t ∧ LowerAdjoint.toFun (closure L) t = s
⊢ LowerAdjoint.toFun (closure L) (↑f '' t) = Substructure.map f s
[PROOFSTEP]
rw [closure_image, ht.2]
[GOAL]
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
inst✝ : Structure L N
f : M ↪[L] N
s : Substructure L M
hs : CG (Substructure.map (Embedding.toHom f) s)
⊢ CG s
[PROOFSTEP]
rcases hs with ⟨t, h1, h2⟩
[GOAL]
case intro.intro
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
inst✝ : Structure L N
f : M ↪[L] N
s : Substructure L M
t : Set N
h1 : Set.Countable t
h2 : LowerAdjoint.toFun (closure L) t = Substructure.map (Embedding.toHom f) s
⊢ CG s
[PROOFSTEP]
rw [cg_def]
[GOAL]
case intro.intro
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
inst✝ : Structure L N
f : M ↪[L] N
s : Substructure L M
t : Set N
h1 : Set.Countable t
h2 : LowerAdjoint.toFun (closure L) t = Substructure.map (Embedding.toHom f) s
⊢ ∃ S, Set.Countable S ∧ LowerAdjoint.toFun (closure L) S = s
[PROOFSTEP]
refine' ⟨f ⁻¹' t, h1.preimage f.injective, _⟩
[GOAL]
case intro.intro
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
inst✝ : Structure L N
f : M ↪[L] N
s : Substructure L M
t : Set N
h1 : Set.Countable t
h2 : LowerAdjoint.toFun (closure L) t = Substructure.map (Embedding.toHom f) s
⊢ LowerAdjoint.toFun (closure L) (↑f ⁻¹' t) = s
[PROOFSTEP]
have hf : Function.Injective f.toHom := f.injective
[GOAL]
case intro.intro
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
inst✝ : Structure L N
f : M ↪[L] N
s : Substructure L M
t : Set N
h1 : Set.Countable t
h2 : LowerAdjoint.toFun (closure L) t = Substructure.map (Embedding.toHom f) s
hf : Function.Injective ↑(Embedding.toHom f)
⊢ LowerAdjoint.toFun (closure L) (↑f ⁻¹' t) = s
[PROOFSTEP]
refine' map_injective_of_injective hf _
[GOAL]
case intro.intro
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
inst✝ : Structure L N
f : M ↪[L] N
s : Substructure L M
t : Set N
h1 : Set.Countable t
h2 : LowerAdjoint.toFun (closure L) t = Substructure.map (Embedding.toHom f) s
hf : Function.Injective ↑(Embedding.toHom f)
⊢ Substructure.map (Embedding.toHom f) (LowerAdjoint.toFun (closure L) (↑f ⁻¹' t)) =
    Substructure.map (Embedding.toHom f) s
[PROOFSTEP]
rw [← h2, map_closure, Embedding.coe_toHom, image_preimage_eq_of_subset]
[GOAL]
case intro.intro
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
inst✝ : Structure L N
f : M ↪[L] N
s : Substructure L M
t : Set N
h1 : Set.Countable t
h2 : LowerAdjoint.toFun (closure L) t = Substructure.map (Embedding.toHom f) s
hf : Function.Injective ↑(Embedding.toHom f)
⊢ t ⊆ range ↑f
[PROOFSTEP]
intro x hx
[GOAL]
case intro.intro
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
inst✝ : Structure L N
f : M ↪[L] N
s : Substructure L M
t : Set N
h1 : Set.Countable t
h2 : LowerAdjoint.toFun (closure L) t = Substructure.map (Embedding.toHom f) s
hf : Function.Injective ↑(Embedding.toHom f)
x : N
hx : x ∈ t
⊢ x ∈ range ↑f
[PROOFSTEP]
have h' := subset_closure (L := L) hx
[GOAL]
case intro.intro
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
inst✝ : Structure L N
f : M ↪[L] N
s : Substructure L M
t : Set N
h1 : Set.Countable t
h2 : LowerAdjoint.toFun (closure L) t = Substructure.map (Embedding.toHom f) s
hf : Function.Injective ↑(Embedding.toHom f)
x : N
hx : x ∈ t
h' : x ∈ ↑(LowerAdjoint.toFun (closure L) t)
⊢ x ∈ range ↑f
[PROOFSTEP]
rw [h2] at h'
[GOAL]
case intro.intro
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
inst✝ : Structure L N
f : M ↪[L] N
s : Substructure L M
t : Set N
h1 : Set.Countable t
h2 : LowerAdjoint.toFun (closure L) t = Substructure.map (Embedding.toHom f) s
hf : Function.Injective ↑(Embedding.toHom f)
x : N
hx : x ∈ t
h' : x ∈ ↑(Substructure.map (Embedding.toHom f) s)
⊢ x ∈ range ↑f
[PROOFSTEP]
exact Hom.map_le_range h'
[GOAL]
L : Language
M : Type u_1
inst✝¹ : Structure L M
inst✝ : Countable ((l : ℕ) × Functions L l)
s : Substructure L M
⊢ CG s ↔ Countable { x // x ∈ s }
[PROOFSTEP]
refine' ⟨_, fun h => ⟨s, h.to_set, s.closure_eq⟩⟩
[GOAL]
L : Language
M : Type u_1
inst✝¹ : Structure L M
inst✝ : Countable ((l : ℕ) × Functions L l)
s : Substructure L M
⊢ CG s → Countable { x // x ∈ s }
[PROOFSTEP]
rintro ⟨s, h, rfl⟩
[GOAL]
case intro.intro
L : Language
M : Type u_1
inst✝¹ : Structure L M
inst✝ : Countable ((l : ℕ) × Functions L l)
s : Set M
h : Set.Countable s
⊢ Countable { x // x ∈ LowerAdjoint.toFun (closure L) s }
[PROOFSTEP]
exact h.substructure_closure L
[GOAL]
L : Language
M : Type u_1
inst✝ : Structure L M
⊢ FG L M ↔ ∃ S, Set.Finite S ∧ LowerAdjoint.toFun (closure L) S = ⊤
[PROOFSTEP]
rw [fg_def, Substructure.fg_def]
[GOAL]
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
inst✝ : Structure L N
h : FG L M
f : M →[L] N
⊢ Substructure.FG (Hom.range f)
[PROOFSTEP]
rw [Hom.range_eq_map]
[GOAL]
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
inst✝ : Structure L N
h : FG L M
f : M →[L] N
⊢ Substructure.FG (map f ⊤)
[PROOFSTEP]
exact (fg_def.1 h).map f
[GOAL]
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
inst✝ : Structure L N
h : FG L M
f : M →[L] N
hs : Function.Surjective ↑f
⊢ FG L N
[PROOFSTEP]
rw [← Hom.range_eq_top] at hs
[GOAL]
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
inst✝ : Structure L N
h : FG L M
f : M →[L] N
hs : Hom.range f = ⊤
⊢ FG L N
[PROOFSTEP]
rw [fg_def, ← hs]
[GOAL]
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
inst✝ : Structure L N
h : FG L M
f : M →[L] N
hs : Hom.range f = ⊤
⊢ Substructure.FG (Hom.range f)
[PROOFSTEP]
exact h.range f
[GOAL]
L : Language
M : Type u_1
inst✝ : Structure L M
⊢ CG L M ↔ ∃ S, Set.Countable S ∧ LowerAdjoint.toFun (closure L) S = ⊤
[PROOFSTEP]
rw [cg_def, Substructure.cg_def]
[GOAL]
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
inst✝ : Structure L N
h : CG L M
f : M →[L] N
⊢ Substructure.CG (Hom.range f)
[PROOFSTEP]
rw [Hom.range_eq_map]
[GOAL]
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
inst✝ : Structure L N
h : CG L M
f : M →[L] N
⊢ Substructure.CG (map f ⊤)
[PROOFSTEP]
exact (cg_def.1 h).map f
[GOAL]
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
inst✝ : Structure L N
h : CG L M
f : M →[L] N
hs : Function.Surjective ↑f
⊢ CG L N
[PROOFSTEP]
rw [← Hom.range_eq_top] at hs
[GOAL]
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
inst✝ : Structure L N
h : CG L M
f : M →[L] N
hs : Hom.range f = ⊤
⊢ CG L N
[PROOFSTEP]
rw [cg_def, ← hs]
[GOAL]
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
inst✝ : Structure L N
h : CG L M
f : M →[L] N
hs : Hom.range f = ⊤
⊢ Substructure.CG (Hom.range f)
[PROOFSTEP]
exact h.range f
[GOAL]
L : Language
M : Type u_1
inst✝¹ : Structure L M
inst✝ : Countable ((l : ℕ) × Functions L l)
⊢ CG L M ↔ Countable M
[PROOFSTEP]
rw [cg_def, Substructure.cg_iff_countable, topEquiv.toEquiv.countable_iff]
[GOAL]
L : Language
M : Type u_1
inst✝ : Structure L M
S : Substructure L M
⊢ FG S ↔ Structure.FG L { x // x ∈ S }
[PROOFSTEP]
rw [Structure.fg_def]
[GOAL]
L : Language
M : Type u_1
inst✝ : Structure L M
S : Substructure L M
⊢ FG S ↔ FG ⊤
[PROOFSTEP]
refine' ⟨fun h => FG.of_map_embedding S.subtype _, fun h => _⟩
[GOAL]
case refine'_1
L : Language
M : Type u_1
inst✝ : Structure L M
S : Substructure L M
h : FG S
⊢ FG (map (Embedding.toHom (subtype S)) ⊤)
[PROOFSTEP]
rw [← Hom.range_eq_map, range_subtype]
[GOAL]
case refine'_1
L : Language
M : Type u_1
inst✝ : Structure L M
S : Substructure L M
h : FG S
⊢ FG S
[PROOFSTEP]
exact h
[GOAL]
case refine'_2
L : Language
M : Type u_1
inst✝ : Structure L M
S : Substructure L M
h : FG ⊤
⊢ FG S
[PROOFSTEP]
have h := h.map S.subtype.toHom
[GOAL]
case refine'_2
L : Language
M : Type u_1
inst✝ : Structure L M
S : Substructure L M
h✝ : FG ⊤
h : FG (map (Embedding.toHom (subtype S)) ⊤)
⊢ FG S
[PROOFSTEP]
rw [← Hom.range_eq_map, range_subtype] at h
[GOAL]
case refine'_2
L : Language
M : Type u_1
inst✝ : Structure L M
S : Substructure L M
h✝ : FG ⊤
h : FG S
⊢ FG S
[PROOFSTEP]
exact h
[GOAL]
L : Language
M : Type u_1
inst✝ : Structure L M
S : Substructure L M
⊢ CG S ↔ Structure.CG L { x // x ∈ S }
[PROOFSTEP]
rw [Structure.cg_def]
[GOAL]
L : Language
M : Type u_1
inst✝ : Structure L M
S : Substructure L M
⊢ CG S ↔ CG ⊤
[PROOFSTEP]
refine' ⟨fun h => CG.of_map_embedding S.subtype _, fun h => _⟩
[GOAL]
case refine'_1
L : Language
M : Type u_1
inst✝ : Structure L M
S : Substructure L M
h : CG S
⊢ CG (map (Embedding.toHom (subtype S)) ⊤)
[PROOFSTEP]
rw [← Hom.range_eq_map, range_subtype]
[GOAL]
case refine'_1
L : Language
M : Type u_1
inst✝ : Structure L M
S : Substructure L M
h : CG S
⊢ CG S
[PROOFSTEP]
exact h
[GOAL]
case refine'_2
L : Language
M : Type u_1
inst✝ : Structure L M
S : Substructure L M
h : CG ⊤
⊢ CG S
[PROOFSTEP]
have h := h.map S.subtype.toHom
[GOAL]
case refine'_2
L : Language
M : Type u_1
inst✝ : Structure L M
S : Substructure L M
h✝ : CG ⊤
h : CG (map (Embedding.toHom (subtype S)) ⊤)
⊢ CG S
[PROOFSTEP]
rw [← Hom.range_eq_map, range_subtype] at h
[GOAL]
case refine'_2
L : Language
M : Type u_1
inst✝ : Structure L M
S : Substructure L M
h✝ : CG ⊤
h : CG S
⊢ CG S
[PROOFSTEP]
exact h