Theorem: Sieve.Yoneda_sheaf_iff_colimit (ExtrDisc/Topologies.lean)

State before:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
⊢ (∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows) ↔ Nonempty (IsColimit (cocone S.arrows))
Tactic:
constructor
State after:
case mp
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
⊢ (∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows) → Nonempty (IsColimit (cocone S.arrows))

case mpr
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
⊢ Nonempty (IsColimit (cocone S.arrows)) → ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows

State before:
case mp
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
⊢ (∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows) → Nonempty (IsColimit (cocone S.arrows))
Tactic:
intro H
State after:
case mp
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
H : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
⊢ Nonempty (IsColimit (cocone S.arrows))

State before:
case mp
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
H : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
⊢ Nonempty (IsColimit (cocone S.arrows))
Tactic:
refine Nonempty.intro ?mp.val
State after:
case mp.val
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
H : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
⊢ IsColimit (cocone S.arrows)

State before:
case mp.val
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
H : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
⊢ IsColimit (cocone S.arrows)
Tactic:
exact {
desc := fun s => H s.pt (yonedaFamilyOfElements_fromCocone S s)
    (yonedaFamily_fromCocone_compatible S s) |>.choose
fac := by
  intro s f
  replace H := H s.pt (yonedaFamilyOfElements_fromCocone S s)
     (yonedaFamily_fromCocone_compatible S s)
  have ht := H.choose_spec.1 f.obj.hom f.property
  aesop_cat
uniq := by
  intro s Fs HFs
  replace H := H s.pt (yonedaFamilyOfElements_fromCocone S s)
      (yonedaFamily_fromCocone_compatible S s)
  apply H.choose_spec.2 Fs
  exact fun _ f hf => HFs ⟨Over.mk f, hf⟩
}
State after:
no goals

State before:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
H : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
⊢ ∀ (s : Cocone (diagram S.arrows)) (j : FullSubcategory fun f => S.arrows f.hom),
    (cocone S.arrows).ι.app j ≫
        (fun s => Exists.choose (_ : ∃! t, FamilyOfElements.IsAmalgamation (yonedaFamilyOfElements_fromCocone S s) t))
          s =
      s.ι.app j
Tactic:
intro s f
State after:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
H : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
s : Cocone (diagram S.arrows)
f : FullSubcategory fun f => S.arrows f.hom
⊢ (cocone S.arrows).ι.app f ≫
      (fun s => Exists.choose (_ : ∃! t, FamilyOfElements.IsAmalgamation (yonedaFamilyOfElements_fromCocone S s) t)) s =
    s.ι.app f

State before:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
H : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
s : Cocone (diagram S.arrows)
f : FullSubcategory fun f => S.arrows f.hom
⊢ (cocone S.arrows).ι.app f ≫
      (fun s => Exists.choose (_ : ∃! t, FamilyOfElements.IsAmalgamation (yonedaFamilyOfElements_fromCocone S s) t)) s =
    s.ι.app f
Tactic:
replace H := H s.pt (yonedaFamilyOfElements_fromCocone S s)
   (yonedaFamily_fromCocone_compatible S s)
State after:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
H✝ : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
s : Cocone (diagram S.arrows)
f : FullSubcategory fun f => S.arrows f.hom
H : ∃! t, FamilyOfElements.IsAmalgamation (yonedaFamilyOfElements_fromCocone S s) t
⊢ (cocone S.arrows).ι.app f ≫
      (fun s => Exists.choose (_ : ∃! t, FamilyOfElements.IsAmalgamation (yonedaFamilyOfElements_fromCocone S s) t)) s =
    s.ι.app f

State before:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
H✝ : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
s : Cocone (diagram S.arrows)
f : FullSubcategory fun f => S.arrows f.hom
H : ∃! t, FamilyOfElements.IsAmalgamation (yonedaFamilyOfElements_fromCocone S s) t
⊢ (cocone S.arrows).ι.app f ≫
      (fun s => Exists.choose (_ : ∃! t, FamilyOfElements.IsAmalgamation (yonedaFamilyOfElements_fromCocone S s) t)) s =
    s.ι.app f
Tactic:
have ht := H.choose_spec.1 f.obj.hom f.property
State after:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
H✝ : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
s : Cocone (diagram S.arrows)
f : FullSubcategory fun f => S.arrows f.hom
H : ∃! t, FamilyOfElements.IsAmalgamation (yonedaFamilyOfElements_fromCocone S s) t
ht :
  (yoneda.obj s.pt).map f.obj.hom.op (Exists.choose H) =
    yonedaFamilyOfElements_fromCocone S s f.obj.hom (_ : S.arrows f.obj.hom)
⊢ (cocone S.arrows).ι.app f ≫
      (fun s => Exists.choose (_ : ∃! t, FamilyOfElements.IsAmalgamation (yonedaFamilyOfElements_fromCocone S s) t)) s =
    s.ι.app f

State before:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
H✝ : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
s : Cocone (diagram S.arrows)
f : FullSubcategory fun f => S.arrows f.hom
H : ∃! t, FamilyOfElements.IsAmalgamation (yonedaFamilyOfElements_fromCocone S s) t
ht :
  (yoneda.obj s.pt).map f.obj.hom.op (Exists.choose H) =
    yonedaFamilyOfElements_fromCocone S s f.obj.hom (_ : S.arrows f.obj.hom)
⊢ (cocone S.arrows).ι.app f ≫
      (fun s => Exists.choose (_ : ∃! t, FamilyOfElements.IsAmalgamation (yonedaFamilyOfElements_fromCocone S s) t)) s =
    s.ι.app f
Tactic:
aesop_cat
State after:
no goals

State before:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
H : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
⊢ ∀ (s : Cocone (diagram S.arrows)) (m : (cocone S.arrows).pt ⟶ s.pt),
    (∀ (j : FullSubcategory fun f => S.arrows f.hom), (cocone S.arrows).ι.app j ≫ m = s.ι.app j) →
      m =
        (fun s => Exists.choose (_ : ∃! t, FamilyOfElements.IsAmalgamation (yonedaFamilyOfElements_fromCocone S s) t)) s
Tactic:
intro s Fs HFs
State after:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
H : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
s : Cocone (diagram S.arrows)
Fs : (cocone S.arrows).pt ⟶ s.pt
HFs : ∀ (j : FullSubcategory fun f => S.arrows f.hom), (cocone S.arrows).ι.app j ≫ Fs = s.ι.app j
⊢ Fs = (fun s => Exists.choose (_ : ∃! t, FamilyOfElements.IsAmalgamation (yonedaFamilyOfElements_fromCocone S s) t)) s

State before:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
H : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
s : Cocone (diagram S.arrows)
Fs : (cocone S.arrows).pt ⟶ s.pt
HFs : ∀ (j : FullSubcategory fun f => S.arrows f.hom), (cocone S.arrows).ι.app j ≫ Fs = s.ι.app j
⊢ Fs = (fun s => Exists.choose (_ : ∃! t, FamilyOfElements.IsAmalgamation (yonedaFamilyOfElements_fromCocone S s) t)) s
Tactic:
replace H := H s.pt (yonedaFamilyOfElements_fromCocone S s)
    (yonedaFamily_fromCocone_compatible S s)
State after:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
H✝ : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
s : Cocone (diagram S.arrows)
Fs : (cocone S.arrows).pt ⟶ s.pt
HFs : ∀ (j : FullSubcategory fun f => S.arrows f.hom), (cocone S.arrows).ι.app j ≫ Fs = s.ι.app j
H : ∃! t, FamilyOfElements.IsAmalgamation (yonedaFamilyOfElements_fromCocone S s) t
⊢ Fs = (fun s => Exists.choose (_ : ∃! t, FamilyOfElements.IsAmalgamation (yonedaFamilyOfElements_fromCocone S s) t)) s

State before:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
H✝ : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
s : Cocone (diagram S.arrows)
Fs : (cocone S.arrows).pt ⟶ s.pt
HFs : ∀ (j : FullSubcategory fun f => S.arrows f.hom), (cocone S.arrows).ι.app j ≫ Fs = s.ι.app j
H : ∃! t, FamilyOfElements.IsAmalgamation (yonedaFamilyOfElements_fromCocone S s) t
⊢ Fs = (fun s => Exists.choose (_ : ∃! t, FamilyOfElements.IsAmalgamation (yonedaFamilyOfElements_fromCocone S s) t)) s
Tactic:
apply H.choose_spec.2 Fs
State after:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
H✝ : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
s : Cocone (diagram S.arrows)
Fs : (cocone S.arrows).pt ⟶ s.pt
HFs : ∀ (j : FullSubcategory fun f => S.arrows f.hom), (cocone S.arrows).ι.app j ≫ Fs = s.ι.app j
H : ∃! t, FamilyOfElements.IsAmalgamation (yonedaFamilyOfElements_fromCocone S s) t
⊢ FamilyOfElements.IsAmalgamation (yonedaFamilyOfElements_fromCocone S s) Fs

State before:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
H✝ : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
s : Cocone (diagram S.arrows)
Fs : (cocone S.arrows).pt ⟶ s.pt
HFs : ∀ (j : FullSubcategory fun f => S.arrows f.hom), (cocone S.arrows).ι.app j ≫ Fs = s.ι.app j
H : ∃! t, FamilyOfElements.IsAmalgamation (yonedaFamilyOfElements_fromCocone S s) t
⊢ FamilyOfElements.IsAmalgamation (yonedaFamilyOfElements_fromCocone S s) Fs
Tactic:
exact fun _ f hf => HFs ⟨Over.mk f, hf⟩
State after:
no goals

State before:
case mpr
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
⊢ Nonempty (IsColimit (cocone S.arrows)) → ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
Tactic:
intro H W x hx
State after:
case mpr
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
H : Nonempty (IsColimit (cocone S.arrows))
W : C
x : FamilyOfElements (yoneda.obj W) S.arrows
hx : FamilyOfElements.Compatible x
⊢ ∃! t, FamilyOfElements.IsAmalgamation x t

State before:
case mpr
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
H : Nonempty (IsColimit (cocone S.arrows))
W : C
x : FamilyOfElements (yoneda.obj W) S.arrows
hx : FamilyOfElements.Compatible x
⊢ ∃! t, FamilyOfElements.IsAmalgamation x t
Tactic:
replace H := Classical.choice H
State after:
case mpr
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
W : C
x : FamilyOfElements (yoneda.obj W) S.arrows
hx : FamilyOfElements.Compatible x
H : IsColimit (cocone S.arrows)
⊢ ∃! t, FamilyOfElements.IsAmalgamation x t

State before:
case mpr
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
W : C
x : FamilyOfElements (yoneda.obj W) S.arrows
hx : FamilyOfElements.Compatible x
H : IsColimit (cocone S.arrows)
⊢ ∃! t, FamilyOfElements.IsAmalgamation x t
Tactic:
let s := Sieve.yonedafamily_toCocone W S x hx
State after:
case mpr
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
W : C
x : FamilyOfElements (yoneda.obj W) S.arrows
hx : FamilyOfElements.Compatible x
H : IsColimit (cocone S.arrows)
s : Cocone (diagram S.arrows) := yonedafamily_toCocone W S.arrows x hx
⊢ ∃! t, FamilyOfElements.IsAmalgamation x t

State before:
case mpr
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
W : C
x : FamilyOfElements (yoneda.obj W) S.arrows
hx : FamilyOfElements.Compatible x
H : IsColimit (cocone S.arrows)
s : Cocone (diagram S.arrows) := yonedafamily_toCocone W S.arrows x hx
⊢ ∃! t, FamilyOfElements.IsAmalgamation x t
Tactic:
use H.desc s
State after:
case mpr
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
W : C
x : FamilyOfElements (yoneda.obj W) S.arrows
hx : FamilyOfElements.Compatible x
H : IsColimit (cocone S.arrows)
s : Cocone (diagram S.arrows) := yonedafamily_toCocone W S.arrows x hx
⊢ (fun t => FamilyOfElements.IsAmalgamation x t) (IsColimit.desc H s) ∧
    ∀ (y : (yoneda.obj W).obj X.op), (fun t => FamilyOfElements.IsAmalgamation x t) y → y = IsColimit.desc H s

State before:
case mpr
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
W : C
x : FamilyOfElements (yoneda.obj W) S.arrows
hx : FamilyOfElements.Compatible x
H : IsColimit (cocone S.arrows)
s : Cocone (diagram S.arrows) := yonedafamily_toCocone W S.arrows x hx
⊢ (fun t => FamilyOfElements.IsAmalgamation x t) (IsColimit.desc H s) ∧
    ∀ (y : (yoneda.obj W).obj X.op), (fun t => FamilyOfElements.IsAmalgamation x t) y → y = IsColimit.desc H s
Tactic:
constructor
State after:
case mpr.left
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
W : C
x : FamilyOfElements (yoneda.obj W) S.arrows
hx : FamilyOfElements.Compatible x
H : IsColimit (cocone S.arrows)
s : Cocone (diagram S.arrows) := yonedafamily_toCocone W S.arrows x hx
⊢ (fun t => FamilyOfElements.IsAmalgamation x t) (IsColimit.desc H s)

case mpr.right
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
W : C
x : FamilyOfElements (yoneda.obj W) S.arrows
hx : FamilyOfElements.Compatible x
H : IsColimit (cocone S.arrows)
s : Cocone (diagram S.arrows) := yonedafamily_toCocone W S.arrows x hx
⊢ ∀ (y : (yoneda.obj W).obj X.op), (fun t => FamilyOfElements.IsAmalgamation x t) y → y = IsColimit.desc H s

State before:
case mpr.left
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
W : C
x : FamilyOfElements (yoneda.obj W) S.arrows
hx : FamilyOfElements.Compatible x
H : IsColimit (cocone S.arrows)
s : Cocone (diagram S.arrows) := yonedafamily_toCocone W S.arrows x hx
⊢ (fun t => FamilyOfElements.IsAmalgamation x t) (IsColimit.desc H s)
Tactic:
exact fun _ f hf => (H.fac s) ⟨Over.mk f, hf⟩
State after:
no goals

State before:
case mpr.right
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
W : C
x : FamilyOfElements (yoneda.obj W) S.arrows
hx : FamilyOfElements.Compatible x
H : IsColimit (cocone S.arrows)
s : Cocone (diagram S.arrows) := yonedafamily_toCocone W S.arrows x hx
⊢ ∀ (y : (yoneda.obj W).obj X.op), (fun t => FamilyOfElements.IsAmalgamation x t) y → y = IsColimit.desc H s
Tactic:
intro g hg
State after:
case mpr.right
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
W : C
x : FamilyOfElements (yoneda.obj W) S.arrows
hx : FamilyOfElements.Compatible x
H : IsColimit (cocone S.arrows)
s : Cocone (diagram S.arrows) := yonedafamily_toCocone W S.arrows x hx
g : (yoneda.obj W).obj X.op
hg : FamilyOfElements.IsAmalgamation x g
⊢ g = IsColimit.desc H s

State before:
case mpr.right
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
W : C
x : FamilyOfElements (yoneda.obj W) S.arrows
hx : FamilyOfElements.Compatible x
H : IsColimit (cocone S.arrows)
s : Cocone (diagram S.arrows) := yonedafamily_toCocone W S.arrows x hx
g : (yoneda.obj W).obj X.op
hg : FamilyOfElements.IsAmalgamation x g
⊢ g = IsColimit.desc H s
Tactic:
apply H.uniq s g
State after:
case mpr.right
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
W : C
x : FamilyOfElements (yoneda.obj W) S.arrows
hx : FamilyOfElements.Compatible x
H : IsColimit (cocone S.arrows)
s : Cocone (diagram S.arrows) := yonedafamily_toCocone W S.arrows x hx
g : (yoneda.obj W).obj X.op
hg : FamilyOfElements.IsAmalgamation x g
⊢ ∀ (j : FullSubcategory fun f => S.arrows f.hom), (cocone S.arrows).ι.app j ≫ g = s.ι.app j

State before:
case mpr.right
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
W : C
x : FamilyOfElements (yoneda.obj W) S.arrows
hx : FamilyOfElements.Compatible x
H : IsColimit (cocone S.arrows)
s : Cocone (diagram S.arrows) := yonedafamily_toCocone W S.arrows x hx
g : (yoneda.obj W).obj X.op
hg : FamilyOfElements.IsAmalgamation x g
⊢ ∀ (j : FullSubcategory fun f => S.arrows f.hom), (cocone S.arrows).ι.app j ≫ g = s.ι.app j
Tactic:
rintro ⟨⟨f, _, hom⟩, hf⟩
State after:
case mpr.right.mk.mk
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
W : C
x : FamilyOfElements (yoneda.obj W) S.arrows
hx : FamilyOfElements.Compatible x
H : IsColimit (cocone S.arrows)
s : Cocone (diagram S.arrows) := yonedafamily_toCocone W S.arrows x hx
g : (yoneda.obj W).obj X.op
hg : FamilyOfElements.IsAmalgamation x g
f : C
right✝ : Discrete PUnit
hom : (𝟭 C).obj f ⟶ (Functor.fromPUnit X).obj right✝
hf : S.arrows { left := f, right := right✝, hom := hom }.hom
⊢ (cocone S.arrows).ι.app { obj := { left := f, right := right✝, hom := hom }, property := hf } ≫ g =
    s.ι.app { obj := { left := f, right := right✝, hom := hom }, property := hf }

State before:
case mpr.right.mk.mk
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
W : C
x : FamilyOfElements (yoneda.obj W) S.arrows
hx : FamilyOfElements.Compatible x
H : IsColimit (cocone S.arrows)
s : Cocone (diagram S.arrows) := yonedafamily_toCocone W S.arrows x hx
g : (yoneda.obj W).obj X.op
hg : FamilyOfElements.IsAmalgamation x g
f : C
right✝ : Discrete PUnit
hom : (𝟭 C).obj f ⟶ (Functor.fromPUnit X).obj right✝
hf : S.arrows { left := f, right := right✝, hom := hom }.hom
⊢ (cocone S.arrows).ι.app { obj := { left := f, right := right✝, hom := hom }, property := hf } ≫ g =
    s.ι.app { obj := { left := f, right := right✝, hom := hom }, property := hf }
Tactic:
apply hg hom hf
State after:
no goals