C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι : Type v
U : ι → Opens ↑X
Fsh✝ : IsSheaf F
Fsh : IsSheafEqualizerProducts F
⊢ IsSheafUniqueGluing F
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι : Type v
U : ι → Opens ↑X
Fsh : IsSheaf F
⊢ IsSheafUniqueGluing F
rw [isSheaf_iff_isSheafEqualizerProducts] at Fsh
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι✝ : Type v
U✝ : ι✝ → Opens ↑X
Fsh✝ : IsSheaf F
Fsh : IsSheafEqualizerProducts F
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type v)).obj (F.obj (U i).op)
hsf : IsCompatible F U sf
⊢ ∃! s, IsGluing F U sf s
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι : Type v
U : ι → Opens ↑X
Fsh✝ : IsSheaf F
Fsh : IsSheafEqualizerProducts F
⊢ IsSheafUniqueGluing F
intro ι U sf hsf
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι✝ : Type v
U✝ : ι✝ → Opens ↑X
Fsh✝ : IsSheaf F
Fsh : IsSheafEqualizerProducts F
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type v)).obj (F.obj (U i).op)
hsf : IsCompatible F U sf
sf' : piOpens F U := (piOpensIsoSectionsFamily F U).inv sf
⊢ ∃! s, IsGluing F U sf s
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι✝ : Type v
U✝ : ι✝ → Opens ↑X
Fsh✝ : IsSheaf F
Fsh : IsSheafEqualizerProducts F
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type v)).obj (F.obj (U i).op)
hsf : IsCompatible F U sf
⊢ ∃! s, IsGluing F U sf s
let sf' := (piOpensIsoSectionsFamily F U).inv sf
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι✝ : Type v
U✝ : ι✝ → Opens ↑X
Fsh✝ : IsSheaf F
Fsh : IsSheafEqualizerProducts F
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type v)).obj (F.obj (U i).op)
hsf : IsCompatible F U sf
sf' : piOpens F U := (piOpensIsoSectionsFamily F U).inv sf
hsf' : leftRes F U sf' = rightRes F U sf'
⊢ ∃! s, IsGluing F U sf s
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι✝ : Type v
U✝ : ι✝ → Opens ↑X
Fsh✝ : IsSheaf F
Fsh : IsSheafEqualizerProducts F
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type v)).obj (F.obj (U i).op)
hsf : IsCompatible F U sf
sf' : piOpens F U := (piOpensIsoSectionsFamily F U).inv sf
⊢ ∃! s, IsGluing F U sf s
have hsf' : leftRes F U sf' = rightRes F U sf' := by
  rwa [← compatible_iff_leftRes_eq_rightRes F U sf', inv_hom_id_apply]
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι✝ : Type v
U✝ : ι✝ → Opens ↑X
Fsh✝ : IsSheaf F
Fsh : IsSheafEqualizerProducts F
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type v)).obj (F.obj (U i).op)
hsf : IsCompatible F U sf
sf' : piOpens F U := (piOpensIsoSectionsFamily F U).inv sf
hsf' : leftRes F U sf' = rightRes F U sf'
s : F.obj (iSup U).op
s_spec : res F U s = sf'
s_uniq : ∀ (y : F.obj (iSup U).op), (fun x => res F U x = sf') y → y = s
⊢ ∃! s, IsGluing F U sf s
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι✝ : Type v
U✝ : ι✝ → Opens ↑X
Fsh✝ : IsSheaf F
Fsh : IsSheafEqualizerProducts F
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type v)).obj (F.obj (U i).op)
hsf : IsCompatible F U sf
sf' : piOpens F U := (piOpensIsoSectionsFamily F U).inv sf
hsf' : leftRes F U sf' = rightRes F U sf'
⊢ ∃! s, IsGluing F U sf s
choose s s_spec s_uniq using Types.unique_of_type_equalizer _ _ (Fsh U).some sf' hsf'
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι✝ : Type v
U✝ : ι✝ → Opens ↑X
Fsh✝ : IsSheaf F
Fsh : IsSheafEqualizerProducts F
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type v)).obj (F.obj (U i).op)
hsf : IsCompatible F U sf
sf' : piOpens F U := (piOpensIsoSectionsFamily F U).inv sf
hsf' : leftRes F U sf' = rightRes F U sf'
s : F.obj (iSup U).op
s_spec : res F U s = sf'
s_uniq : ∀ (y : F.obj (iSup U).op), (fun x => res F U x = sf') y → y = s
⊢ (fun s => IsGluing F U sf s) s ∧
    ∀ (y : (forget (Type v)).obj (F.obj (iSup U).op)), (fun s => IsGluing F U sf s) y → y = s
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι✝ : Type v
U✝ : ι✝ → Opens ↑X
Fsh✝ : IsSheaf F
Fsh : IsSheafEqualizerProducts F
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type v)).obj (F.obj (U i).op)
hsf : IsCompatible F U sf
sf' : piOpens F U := (piOpensIsoSectionsFamily F U).inv sf
hsf' : leftRes F U sf' = rightRes F U sf'
s : F.obj (iSup U).op
s_spec : res F U s = sf'
s_uniq : ∀ (y : F.obj (iSup U).op), (fun x => res F U x = sf') y → y = s
⊢ ∃! s, IsGluing F U sf s
use s
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι✝ : Type v
U✝ : ι✝ → Opens ↑X
Fsh✝ : IsSheaf F
Fsh : IsSheafEqualizerProducts F
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type v)).obj (F.obj (U i).op)
hsf : IsCompatible F U sf
sf' : piOpens F U := (piOpensIsoSectionsFamily F U).inv sf
hsf' : leftRes F U sf' = rightRes F U sf'
s : F.obj (iSup U).op
s_spec : res F U s = sf'
s_uniq : ∀ (y : F.obj (iSup U).op), (fun x => res F U x = sf') y → y = s
⊢ IsGluing F U sf s ∧ ∀ (y : (forget (Type v)).obj (F.obj (iSup U).op)), IsGluing F U sf y → y = s
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι✝ : Type v
U✝ : ι✝ → Opens ↑X
Fsh✝ : IsSheaf F
Fsh : IsSheafEqualizerProducts F
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type v)).obj (F.obj (U i).op)
hsf : IsCompatible F U sf
sf' : piOpens F U := (piOpensIsoSectionsFamily F U).inv sf
hsf' : leftRes F U sf' = rightRes F U sf'
s : F.obj (iSup U).op
s_spec : res F U s = sf'
s_uniq : ∀ (y : F.obj (iSup U).op), (fun x => res F U x = sf') y → y = s
⊢ (fun s => IsGluing F U sf s) s ∧
    ∀ (y : (forget (Type v)).obj (F.obj (iSup U).op)), (fun s => IsGluing F U sf s) y → y = s
dsimp
case left
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι✝ : Type v
U✝ : ι✝ → Opens ↑X
Fsh✝ : IsSheaf F
Fsh : IsSheafEqualizerProducts F
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type v)).obj (F.obj (U i).op)
hsf : IsCompatible F U sf
sf' : piOpens F U := (piOpensIsoSectionsFamily F U).inv sf
hsf' : leftRes F U sf' = rightRes F U sf'
s : F.obj (iSup U).op
s_spec : res F U s = sf'
s_uniq : ∀ (y : F.obj (iSup U).op), (fun x => res F U x = sf') y → y = s
⊢ IsGluing F U sf s

case right
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι✝ : Type v
U✝ : ι✝ → Opens ↑X
Fsh✝ : IsSheaf F
Fsh : IsSheafEqualizerProducts F
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type v)).obj (F.obj (U i).op)
hsf : IsCompatible F U sf
sf' : piOpens F U := (piOpensIsoSectionsFamily F U).inv sf
hsf' : leftRes F U sf' = rightRes F U sf'
s : F.obj (iSup U).op
s_spec : res F U s = sf'
s_uniq : ∀ (y : F.obj (iSup U).op), (fun x => res F U x = sf') y → y = s
⊢ ∀ (y : (forget (Type v)).obj (F.obj (iSup U).op)), IsGluing F U sf y → y = s
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι✝ : Type v
U✝ : ι✝ → Opens ↑X
Fsh✝ : IsSheaf F
Fsh : IsSheafEqualizerProducts F
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type v)).obj (F.obj (U i).op)
hsf : IsCompatible F U sf
sf' : piOpens F U := (piOpensIsoSectionsFamily F U).inv sf
hsf' : leftRes F U sf' = rightRes F U sf'
s : F.obj (iSup U).op
s_spec : res F U s = sf'
s_uniq : ∀ (y : F.obj (iSup U).op), (fun x => res F U x = sf') y → y = s
⊢ IsGluing F U sf s ∧ ∀ (y : (forget (Type v)).obj (F.obj (iSup U).op)), IsGluing F U sf y → y = s
constructor
no goals
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι✝ : Type v
U✝ : ι✝ → Opens ↑X
Fsh✝ : IsSheaf F
Fsh : IsSheafEqualizerProducts F
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type v)).obj (F.obj (U i).op)
hsf : IsCompatible F U sf
sf' : piOpens F U := (piOpensIsoSectionsFamily F U).inv sf
⊢ leftRes F U sf' = rightRes F U sf'
rwa [← compatible_iff_leftRes_eq_rightRes F U sf', inv_hom_id_apply]
case h.e'_8
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι✝ : Type v
U✝ : ι✝ → Opens ↑X
Fsh✝ : IsSheaf F
Fsh : IsSheafEqualizerProducts F
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type v)).obj (F.obj (U i).op)
hsf : IsCompatible F U sf
sf' : piOpens F U := (piOpensIsoSectionsFamily F U).inv sf
hsf' : leftRes F U sf' = rightRes F U sf'
s : F.obj (iSup U).op
s_spec : res F U s = sf'
s_uniq : ∀ (y : F.obj (iSup U).op), (fun x => res F U x = sf') y → y = s
⊢ sf = (piOpensIsoSectionsFamily F U).hom sf'
case left
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι✝ : Type v
U✝ : ι✝ → Opens ↑X
Fsh✝ : IsSheaf F
Fsh : IsSheafEqualizerProducts F
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type v)).obj (F.obj (U i).op)
hsf : IsCompatible F U sf
sf' : piOpens F U := (piOpensIsoSectionsFamily F U).inv sf
hsf' : leftRes F U sf' = rightRes F U sf'
s : F.obj (iSup U).op
s_spec : res F U s = sf'
s_uniq : ∀ (y : F.obj (iSup U).op), (fun x => res F U x = sf') y → y = s
⊢ IsGluing F U sf s
convert(isGluing_iff_eq_res F U sf' _).mpr s_spec
no goals
case h.e'_8
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι✝ : Type v
U✝ : ι✝ → Opens ↑X
Fsh✝ : IsSheaf F
Fsh : IsSheafEqualizerProducts F
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type v)).obj (F.obj (U i).op)
hsf : IsCompatible F U sf
sf' : piOpens F U := (piOpensIsoSectionsFamily F U).inv sf
hsf' : leftRes F U sf' = rightRes F U sf'
s : F.obj (iSup U).op
s_spec : res F U s = sf'
s_uniq : ∀ (y : F.obj (iSup U).op), (fun x => res F U x = sf') y → y = s
⊢ sf = (piOpensIsoSectionsFamily F U).hom sf'
rw [inv_hom_id_apply]
case right
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι✝ : Type v
U✝ : ι✝ → Opens ↑X
Fsh✝ : IsSheaf F
Fsh : IsSheafEqualizerProducts F
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type v)).obj (F.obj (U i).op)
hsf : IsCompatible F U sf
sf' : piOpens F U := (piOpensIsoSectionsFamily F U).inv sf
hsf' : leftRes F U sf' = rightRes F U sf'
s : F.obj (iSup U).op
s_spec : res F U s = sf'
s_uniq : ∀ (y : F.obj (iSup U).op), (fun x => res F U x = sf') y → y = s
y : (forget (Type v)).obj (F.obj (iSup U).op)
hy : IsGluing F U sf y
⊢ y = s
case right
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι✝ : Type v
U✝ : ι✝ → Opens ↑X
Fsh✝ : IsSheaf F
Fsh : IsSheafEqualizerProducts F
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type v)).obj (F.obj (U i).op)
hsf : IsCompatible F U sf
sf' : piOpens F U := (piOpensIsoSectionsFamily F U).inv sf
hsf' : leftRes F U sf' = rightRes F U sf'
s : F.obj (iSup U).op
s_spec : res F U s = sf'
s_uniq : ∀ (y : F.obj (iSup U).op), (fun x => res F U x = sf') y → y = s
⊢ ∀ (y : (forget (Type v)).obj (F.obj (iSup U).op)), IsGluing F U sf y → y = s
intro y hy
case right.a
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι✝ : Type v
U✝ : ι✝ → Opens ↑X
Fsh✝ : IsSheaf F
Fsh : IsSheafEqualizerProducts F
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type v)).obj (F.obj (U i).op)
hsf : IsCompatible F U sf
sf' : piOpens F U := (piOpensIsoSectionsFamily F U).inv sf
hsf' : leftRes F U sf' = rightRes F U sf'
s : F.obj (iSup U).op
s_spec : res F U s = sf'
s_uniq : ∀ (y : F.obj (iSup U).op), (fun x => res F U x = sf') y → y = s
y : (forget (Type v)).obj (F.obj (iSup U).op)
hy : IsGluing F U sf y
⊢ res F U y = sf'
case right
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι✝ : Type v
U✝ : ι✝ → Opens ↑X
Fsh✝ : IsSheaf F
Fsh : IsSheafEqualizerProducts F
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type v)).obj (F.obj (U i).op)
hsf : IsCompatible F U sf
sf' : piOpens F U := (piOpensIsoSectionsFamily F U).inv sf
hsf' : leftRes F U sf' = rightRes F U sf'
s : F.obj (iSup U).op
s_spec : res F U s = sf'
s_uniq : ∀ (y : F.obj (iSup U).op), (fun x => res F U x = sf') y → y = s
y : (forget (Type v)).obj (F.obj (iSup U).op)
hy : IsGluing F U sf y
⊢ y = s
apply s_uniq
case right.a
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι✝ : Type v
U✝ : ι✝ → Opens ↑X
Fsh✝ : IsSheaf F
Fsh : IsSheafEqualizerProducts F
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type v)).obj (F.obj (U i).op)
hsf : IsCompatible F U sf
sf' : piOpens F U := (piOpensIsoSectionsFamily F U).inv sf
hsf' : leftRes F U sf' = rightRes F U sf'
s : F.obj (iSup U).op
s_spec : res F U s = sf'
s_uniq : ∀ (y : F.obj (iSup U).op), (fun x => res F U x = sf') y → y = s
y : (forget (Type v)).obj (F.obj (iSup U).op)
hy : IsGluing F U sf y
⊢ IsGluing F U ((piOpensIsoSectionsFamily F U).hom sf') y
case right.a
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι✝ : Type v
U✝ : ι✝ → Opens ↑X
Fsh✝ : IsSheaf F
Fsh : IsSheafEqualizerProducts F
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type v)).obj (F.obj (U i).op)
hsf : IsCompatible F U sf
sf' : piOpens F U := (piOpensIsoSectionsFamily F U).inv sf
hsf' : leftRes F U sf' = rightRes F U sf'
s : F.obj (iSup U).op
s_spec : res F U s = sf'
s_uniq : ∀ (y : F.obj (iSup U).op), (fun x => res F U x = sf') y → y = s
y : (forget (Type v)).obj (F.obj (iSup U).op)
hy : IsGluing F U sf y
⊢ res F U y = sf'
rw [← isGluing_iff_eq_res F U]
case h.e'_8
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι✝ : Type v
U✝ : ι✝ → Opens ↑X
Fsh✝ : IsSheaf F
Fsh : IsSheafEqualizerProducts F
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type v)).obj (F.obj (U i).op)
hsf : IsCompatible F U sf
sf' : piOpens F U := (piOpensIsoSectionsFamily F U).inv sf
hsf' : leftRes F U sf' = rightRes F U sf'
s : F.obj (iSup U).op
s_spec : res F U s = sf'
s_uniq : ∀ (y : F.obj (iSup U).op), (fun x => res F U x = sf') y → y = s
y : (forget (Type v)).obj (F.obj (iSup U).op)
hy : IsGluing F U sf y
⊢ (piOpensIsoSectionsFamily F U).hom sf' = sf
case right.a
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι✝ : Type v
U✝ : ι✝ → Opens ↑X
Fsh✝ : IsSheaf F
Fsh : IsSheafEqualizerProducts F
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type v)).obj (F.obj (U i).op)
hsf : IsCompatible F U sf
sf' : piOpens F U := (piOpensIsoSectionsFamily F U).inv sf
hsf' : leftRes F U sf' = rightRes F U sf'
s : F.obj (iSup U).op
s_spec : res F U s = sf'
s_uniq : ∀ (y : F.obj (iSup U).op), (fun x => res F U x = sf') y → y = s
y : (forget (Type v)).obj (F.obj (iSup U).op)
hy : IsGluing F U sf y
⊢ IsGluing F U ((piOpensIsoSectionsFamily F U).hom sf') y
convert hy
no goals
case h.e'_8
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι✝ : Type v
U✝ : ι✝ → Opens ↑X
Fsh✝ : IsSheaf F
Fsh : IsSheafEqualizerProducts F
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type v)).obj (F.obj (U i).op)
hsf : IsCompatible F U sf
sf' : piOpens F U := (piOpensIsoSectionsFamily F U).inv sf
hsf' : leftRes F U sf' = rightRes F U sf'
s : F.obj (iSup U).op
s_spec : res F U s = sf'
s_uniq : ∀ (y : F.obj (iSup U).op), (fun x => res F U x = sf') y → y = s
y : (forget (Type v)).obj (F.obj (iSup U).op)
hy : IsGluing F U sf y
⊢ (piOpensIsoSectionsFamily F U).hom sf' = sf
rw [inv_hom_id_apply]