S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
s : S.obj α.op
⊢ ∀ ⦃Y : Type u⦄ ⦃f : Y ⟶ α⦄, discretePresieve α f → S.map f.op (typesGlue S hs α (eval S α s)) = S.map f.op s
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
s : S.obj α.op
⊢ typesGlue S hs α (eval S α s) = s
apply (hs.isSheafFor _ _ (generate_discretePresieve_mem α)).isSeparatedFor.ext
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
s : S.obj α.op
β : Type u
f : β ⟶ α
hf : discretePresieve α f
⊢ S.map f.op (typesGlue S hs α (eval S α s)) = S.map f.op s
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
s : S.obj α.op
⊢ ∀ ⦃Y : Type u⦄ ⦃f : Y ⟶ α⦄, discretePresieve α f → S.map f.op (typesGlue S hs α (eval S α s)) = S.map f.op s
intro β f hf
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
s : S.obj α.op
β : Type u
f : β ⟶ α
hf : discretePresieve α f
⊢ S.map (↾fun x => PUnit.unit).op (eval S α s (f (Classical.choose hf))) = S.map f.op s
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
s : S.obj α.op
β : Type u
f : β ⟶ α
hf : discretePresieve α f
⊢ S.map f.op (typesGlue S hs α (eval S α s)) = S.map f.op s
apply (IsSheafFor.valid_glue _ _ _ hf).trans
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
s : S.obj α.op
β : Type u
f : β ⟶ α
hf : discretePresieve α f
⊢ S.map ((↾fun x => f (Classical.choose hf)).op ≫ (↾fun x => PUnit.unit).op) s = S.map f.op s
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
s : S.obj α.op
β : Type u
f : β ⟶ α
hf : discretePresieve α f
⊢ S.map (↾fun x => PUnit.unit).op (eval S α s (f (Classical.choose hf))) = S.map f.op s
apply (FunctorToTypes.map_comp_apply _ _ _ _).symm.trans
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
s : S.obj α.op
β : Type u
f : β ⟶ α
hf : discretePresieve α f
⊢ S.map ((↾fun x => PUnit.unit) ≫ ↾fun x => f (Classical.choose hf)).op s = S.map f.op s
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
s : S.obj α.op
β : Type u
f : β ⟶ α
hf : discretePresieve α f
⊢ S.map ((↾fun x => f (Classical.choose hf)).op ≫ (↾fun x => PUnit.unit).op) s = S.map f.op s
rw [← op_comp]
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
s : S.obj α.op
β : Type u
f : β ⟶ α
hf : discretePresieve α f
⊢ ((↾fun x => PUnit.unit) ≫ ↾fun x => f (Classical.choose hf)) = f
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
s : S.obj α.op
β : Type u
f : β ⟶ α
hf : discretePresieve α f
⊢ S.map ((↾fun x => PUnit.unit) ≫ ↾fun x => f (Classical.choose hf)).op s = S.map f.op s
suffices ((↾fun _ ↦ PUnit.unit) ≫ ↾fun _ ↦ f (Classical.choose hf)) = f by rw [this]
case h
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
s : S.obj α.op
β : Type u
f : β ⟶ α
hf : discretePresieve α f
x : β
⊢ ((↾fun x => PUnit.unit) ≫ ↾fun x => f (Classical.choose hf)) x = f x
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
s : S.obj α.op
β : Type u
f : β ⟶ α
hf : discretePresieve α f
⊢ ((↾fun x => PUnit.unit) ≫ ↾fun x => f (Classical.choose hf)) = f
funext x
no goals
case h
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
s : S.obj α.op
β : Type u
f : β ⟶ α
hf : discretePresieve α f
x : β
⊢ ((↾fun x => PUnit.unit) ≫ ↾fun x => f (Classical.choose hf)) x = f x
exact congr_arg f (Classical.choose_spec hf x).symm
no goals
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
s : S.obj α.op
β : Type u
f : β ⟶ α
hf : discretePresieve α f
this : ((↾fun x => PUnit.unit) ≫ ↾fun x => f (Classical.choose hf)) = f
⊢ S.map ((↾fun x => PUnit.unit) ≫ ↾fun x => f (Classical.choose hf)).op s = S.map f.op s
rw [this]