case a
C D : Type u
inst✝³ : Category C
inst✝² : Category D
A : Type w
inst✝¹ : Category A
inst✝ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
hu : CoverLifting J K G
ℱ : Sheaf J A
X : A
U : D
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves K U
x : FamilyOfElements ((ran (Functor.op G)).obj ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
Y : StructuredArrow U.op (Functor.op G)
y : ((𝟭 (Cᵒᵖ ⥤ A)).obj ℱ.val ⋙ coyoneda.obj X.op).obj Y.right.unop.op
H : IsAmalgamation (pulledbackFamily ℱ S x Y) y
⊢ IsAmalgamation (pulledbackFamily ℱ S x Y) y

case a
C D : Type u
inst✝³ : Category C
inst✝² : Category D
A : Type w
inst✝¹ : Category A
inst✝ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
hu : CoverLifting J K G
ℱ : Sheaf J A
X : A
U : D
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves K U
x : FamilyOfElements ((ran (Functor.op G)).obj ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
Y : StructuredArrow U.op (Functor.op G)
y : ((𝟭 (Cᵒᵖ ⥤ A)).obj ℱ.val ⋙ coyoneda.obj X.op).obj Y.right.unop.op
H : IsAmalgamation (pulledbackFamily ℱ S x Y) y
⊢ IsAmalgamation (pulledbackFamily ℱ S x Y) (getSection hu ℱ hS hx Y)

C D : Type u
inst✝³ : Category C
inst✝² : Category D
A : Type w
inst✝¹ : Category A
inst✝ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
hu : CoverLifting J K G
ℱ : Sheaf J A
X : A
U : D
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves K U
x : FamilyOfElements ((ran (Functor.op G)).obj ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
Y : StructuredArrow U.op (Functor.op G)
y : ((𝟭 (Cᵒᵖ ⥤ A)).obj ℱ.val ⋙ coyoneda.obj X.op).obj Y.right.unop.op
H : IsAmalgamation (pulledbackFamily ℱ S x Y) y
⊢ IsSheafFor ((𝟭 (Cᵒᵖ ⥤ A)).obj ℱ.val ⋙ coyoneda.obj X.op)
    (Presieve.functorPullback G (Sieve.pullback Y.hom.unop S).arrows)
C D : Type u
inst✝³ : Category C
inst✝² : Category D
A : Type w
inst✝¹ : Category A
inst✝ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
hu : CoverLifting J K G
ℱ : Sheaf J A
X : A
U : D
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves K U
x : FamilyOfElements ((ran (Functor.op G)).obj ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
Y : StructuredArrow U.op (Functor.op G)
y : ((𝟭 (Cᵒᵖ ⥤ A)).obj ℱ.val ⋙ coyoneda.obj X.op).obj Y.right.unop.op
H : IsAmalgamation (pulledbackFamily ℱ S x Y) y
⊢ y = getSection hu ℱ hS hx Y
apply IsSheafFor.isSeparatedFor _ (pulledbackFamily ℱ S x Y)
no goals
case a
C D : Type u
inst✝³ : Category C
inst✝² : Category D
A : Type w
inst✝¹ : Category A
inst✝ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
hu : CoverLifting J K G
ℱ : Sheaf J A
X : A
U : D
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves K U
x : FamilyOfElements ((ran (Functor.op G)).obj ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
Y : StructuredArrow U.op (Functor.op G)
y : ((𝟭 (Cᵒᵖ ⥤ A)).obj ℱ.val ⋙ coyoneda.obj X.op).obj Y.right.unop.op
H : IsAmalgamation (pulledbackFamily ℱ S x Y) y
⊢ IsAmalgamation (pulledbackFamily ℱ S x Y) y
exact H
no goals
case a
C D : Type u
inst✝³ : Category C
inst✝² : Category D
A : Type w
inst✝¹ : Category A
inst✝ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
hu : CoverLifting J K G
ℱ : Sheaf J A
X : A
U : D
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves K U
x : FamilyOfElements ((ran (Functor.op G)).obj ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
Y : StructuredArrow U.op (Functor.op G)
y : ((𝟭 (Cᵒᵖ ⥤ A)).obj ℱ.val ⋙ coyoneda.obj X.op).obj Y.right.unop.op
H : IsAmalgamation (pulledbackFamily ℱ S x Y) y
⊢ IsAmalgamation (pulledbackFamily ℱ S x Y) (getSection hu ℱ hS hx Y)
apply getSection_isAmalgamation
no goals
C D : Type u
inst✝³ : Category C
inst✝² : Category D
A : Type w
inst✝¹ : Category A
inst✝ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
hu : CoverLifting J K G
ℱ : Sheaf J A
X : A
U : D
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves K U
x : FamilyOfElements ((ran (Functor.op G)).obj ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
Y : StructuredArrow U.op (Functor.op G)
y : ((𝟭 (Cᵒᵖ ⥤ A)).obj ℱ.val ⋙ coyoneda.obj X.op).obj Y.right.unop.op
H : IsAmalgamation (pulledbackFamily ℱ S x Y) y
⊢ IsSheafFor ((𝟭 (Cᵒᵖ ⥤ A)).obj ℱ.val ⋙ coyoneda.obj X.op)
    (Presieve.functorPullback G (Sieve.pullback Y.hom.unop S).arrows)
exact ℱ.2 X _ (hu.cover_lift (K.pullback_stable Y.hom.unop hS))