case intro
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
ht : FamilyOfElements.IsAmalgamation x t
⊢ FamilyOfElements.Compatible x
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
h : ∃ t, FamilyOfElements.IsAmalgamation x t
⊢ FamilyOfElements.Compatible x
cases' h with t ht
case intro
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
ht : FamilyOfElements.IsAmalgamation x t
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : R f₁
h₂ : R f₂
comm : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ P.map g₁.op (x f₁ h₁) = P.map g₂.op (x f₂ h₂)
case intro
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
ht : FamilyOfElements.IsAmalgamation x t
⊢ FamilyOfElements.Compatible x
intro Y₁ Y₂ Z g₁ g₂ f₁ f₂ h₁ h₂ comm
case intro
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
ht : FamilyOfElements.IsAmalgamation x t
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : R f₁
h₂ : R f₂
comm : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ P.map (g₂ ≫ f₂).op t = P.map g₂.op (P.map f₂.op t)
case intro
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
ht : FamilyOfElements.IsAmalgamation x t
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : R f₁
h₂ : R f₂
comm : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ P.map g₁.op (x f₁ h₁) = P.map g₂.op (x f₂ h₂)
rw [← ht _ h₁, ← ht _ h₂, ← FunctorToTypes.map_comp_apply, ← op_comp, comm]
no goals
case intro
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
ht : FamilyOfElements.IsAmalgamation x t
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : R f₁
h₂ : R f₂
comm : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ P.map (g₂ ≫ f₂).op t = P.map g₂.op (P.map f₂.op t)
simp