C : Type u₁
inst✝ : Category C
P Q U : Cᵒᵖ ⥤ Type w
X Y✝ : C
S : Sieve X
R : Presieve X
J J₂ : GrothendieckTopology C
x : FamilyOfElements P R
t : P.obj X.op
f : P ⟶ Q
h : IsAmalgamation x t
Y : C
g : Y ⟶ X
hg : R g
⊢ Q.map g.op (f.app X.op t) = FamilyOfElements.compPresheafMap f x g hg
C : Type u₁
inst✝ : Category C
P Q U : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
R : Presieve X
J J₂ : GrothendieckTopology C
x : FamilyOfElements P R
t : P.obj X.op
f : P ⟶ Q
h : IsAmalgamation x t
⊢ IsAmalgamation (FamilyOfElements.compPresheafMap f x) (f.app X.op t)
intro Y g hg
C : Type u₁
inst✝ : Category C
P Q U : Cᵒᵖ ⥤ Type w
X Y✝ : C
S : Sieve X
R : Presieve X
J J₂ : GrothendieckTopology C
x : FamilyOfElements P R
t : P.obj X.op
f : P ⟶ Q
h : IsAmalgamation x t
Y : C
g : Y ⟶ X
hg : R g
⊢ Q.map g.op (f.app X.op t) = f.app Y.op (x g hg)
C : Type u₁
inst✝ : Category C
P Q U : Cᵒᵖ ⥤ Type w
X Y✝ : C
S : Sieve X
R : Presieve X
J J₂ : GrothendieckTopology C
x : FamilyOfElements P R
t : P.obj X.op
f : P ⟶ Q
h : IsAmalgamation x t
Y : C
g : Y ⟶ X
hg : R g
⊢ Q.map g.op (f.app X.op t) = FamilyOfElements.compPresheafMap f x g hg
dsimp [FamilyOfElements.compPresheafMap]
C : Type u₁
inst✝ : Category C
P Q U : Cᵒᵖ ⥤ Type w
X Y✝ : C
S : Sieve X
R : Presieve X
J J₂ : GrothendieckTopology C
x : FamilyOfElements P R
t : P.obj X.op
f : P ⟶ Q
h : IsAmalgamation x t
Y : C
g : Y ⟶ X
hg : R g
⊢ (f.app X.op ≫ Q.map g.op) t = f.app Y.op (x g hg)
C : Type u₁
inst✝ : Category C
P Q U : Cᵒᵖ ⥤ Type w
X Y✝ : C
S : Sieve X
R : Presieve X
J J₂ : GrothendieckTopology C
x : FamilyOfElements P R
t : P.obj X.op
f : P ⟶ Q
h : IsAmalgamation x t
Y : C
g : Y ⟶ X
hg : R g
⊢ Q.map g.op (f.app X.op t) = f.app Y.op (x g hg)
change (f.app _ ≫ Q.map _) _ = _
no goals
C : Type u₁
inst✝ : Category C
P Q U : Cᵒᵖ ⥤ Type w
X Y✝ : C
S : Sieve X
R : Presieve X
J J₂ : GrothendieckTopology C
x : FamilyOfElements P R
t : P.obj X.op
f : P ⟶ Q
h : IsAmalgamation x t
Y : C
g : Y ⟶ X
hg : R g
⊢ (f.app X.op ≫ Q.map g.op) t = f.app Y.op (x g hg)
rw [← f.naturality, types_comp_apply, h g hg]