C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows
hx : SieveCompatible x
⊢ Nonempty (IsLimit (P.mapCone (Cocone.op (cocone S.arrows)))) ↔
    ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows), Compatible x → ∃! t, IsAmalgamation x t
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows
hx : SieveCompatible x
⊢ Nonempty (IsLimit (P.mapCone (Cocone.op (cocone S.arrows)))) ↔ ∀ (E : Aᵒᵖ), IsSheafFor (P ⋙ coyoneda.obj E) S.arrows
dsimp [IsSheafFor]
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows
hx : SieveCompatible x
⊢ Nonempty (IsLimit (P.mapCone (Cocone.op (cocone S.arrows)))) ↔
    ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows), SieveCompatible x → ∃! t, IsAmalgamation x t
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows
hx : SieveCompatible x
⊢ Nonempty (IsLimit (P.mapCone (Cocone.op (cocone S.arrows)))) ↔
    ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows), Compatible x → ∃! t, IsAmalgamation x t
simp_rw [compatible_iff_sieveCompatible]
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows
hx : SieveCompatible x
⊢ Nonempty ((X_1 : Cone (Functor.op (diagram S.arrows) ⋙ P)) → Unique (X_1 ⟶ P.mapCone (Cocone.op (cocone S.arrows)))) ↔
    ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows), SieveCompatible x → ∃! t, IsAmalgamation x t
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows
hx : SieveCompatible x
⊢ Nonempty (IsLimit (P.mapCone (Cocone.op (cocone S.arrows)))) ↔
    ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows), SieveCompatible x → ∃! t, IsAmalgamation x t
rw [((Cone.isLimitEquivIsTerminal _).trans (isTerminalEquivUnique _ _)).nonempty_congr]
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows
hx : SieveCompatible x
⊢ (∀ (i : Cone (Functor.op (diagram S.arrows) ⋙ P)), Nonempty (Unique (i ⟶ P.mapCone (Cocone.op (cocone S.arrows))))) ↔
    ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows), SieveCompatible x → ∃! t, IsAmalgamation x t
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows
hx : SieveCompatible x
⊢ Nonempty ((X_1 : Cone (Functor.op (diagram S.arrows) ⋙ P)) → Unique (X_1 ⟶ P.mapCone (Cocone.op (cocone S.arrows)))) ↔
    ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows), SieveCompatible x → ∃! t, IsAmalgamation x t
rw [Classical.nonempty_pi]
case mp
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows
hx : SieveCompatible x
⊢ (∀ (i : Cone (Functor.op (diagram S.arrows) ⋙ P)), Nonempty (Unique (i ⟶ P.mapCone (Cocone.op (cocone S.arrows))))) →
    ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows), SieveCompatible x → ∃! t, IsAmalgamation x t

case mpr
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows
hx : SieveCompatible x
⊢ (∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows), SieveCompatible x → ∃! t, IsAmalgamation x t) →
    ∀ (i : Cone (Functor.op (diagram S.arrows) ⋙ P)), Nonempty (Unique (i ⟶ P.mapCone (Cocone.op (cocone S.arrows))))
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows
hx : SieveCompatible x
⊢ (∀ (i : Cone (Functor.op (diagram S.arrows) ⋙ P)), Nonempty (Unique (i ⟶ P.mapCone (Cocone.op (cocone S.arrows))))) ↔
    ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows), SieveCompatible x → ∃! t, IsAmalgamation x t
constructor
case mp
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E✝ : Aᵒᵖ
x✝ : FamilyOfElements (P ⋙ coyoneda.obj E✝) S.arrows
hx✝ : SieveCompatible x✝
hu : ∀ (i : Cone (Functor.op (diagram S.arrows) ⋙ P)), Nonempty (Unique (i ⟶ P.mapCone (Cocone.op (cocone S.arrows))))
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows
hx : SieveCompatible x
⊢ ∃! t, IsAmalgamation x t
case mp
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows
hx : SieveCompatible x
⊢ (∀ (i : Cone (Functor.op (diagram S.arrows) ⋙ P)), Nonempty (Unique (i ⟶ P.mapCone (Cocone.op (cocone S.arrows))))) →
    ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows), SieveCompatible x → ∃! t, IsAmalgamation x t
intro hu E x hx
case mp
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E✝ : Aᵒᵖ
x✝ : FamilyOfElements (P ⋙ coyoneda.obj E✝) S.arrows
hx✝ : SieveCompatible x✝
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows
hx : SieveCompatible x
hu : Nonempty (Unique (SieveCompatible.cone hx ⟶ P.mapCone (Cocone.op (cocone S.arrows))))
⊢ ∃! t, IsAmalgamation x t
case mp
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E✝ : Aᵒᵖ
x✝ : FamilyOfElements (P ⋙ coyoneda.obj E✝) S.arrows
hx✝ : SieveCompatible x✝
hu : ∀ (i : Cone (Functor.op (diagram S.arrows) ⋙ P)), Nonempty (Unique (i ⟶ P.mapCone (Cocone.op (cocone S.arrows))))
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows
hx : SieveCompatible x
⊢ ∃! t, IsAmalgamation x t
specialize hu hx.cone
case mp
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E✝ : Aᵒᵖ
x✝ : FamilyOfElements (P ⋙ coyoneda.obj E✝) S.arrows
hx✝ : SieveCompatible x✝
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows
hx : SieveCompatible x
hu : Nonempty (Unique { t // IsAmalgamation x t })
⊢ ∃! t, IsAmalgamation x t
case mp
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E✝ : Aᵒᵖ
x✝ : FamilyOfElements (P ⋙ coyoneda.obj E✝) S.arrows
hx✝ : SieveCompatible x✝
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows
hx : SieveCompatible x
hu : Nonempty (Unique (SieveCompatible.cone hx ⟶ P.mapCone (Cocone.op (cocone S.arrows))))
⊢ ∃! t, IsAmalgamation x t
erw [(homEquivAmalgamation hx).uniqueCongr.nonempty_congr] at hu
no goals
case mp
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E✝ : Aᵒᵖ
x✝ : FamilyOfElements (P ⋙ coyoneda.obj E✝) S.arrows
hx✝ : SieveCompatible x✝
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows
hx : SieveCompatible x
hu : Nonempty (Unique { t // IsAmalgamation x t })
⊢ ∃! t, IsAmalgamation x t
exact (unique_subtype_iff_exists_unique _).1 hu
case mpr.mk
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E✝ : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E✝) S.arrows
hx : SieveCompatible x
h : ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows), SieveCompatible x → ∃! t, IsAmalgamation x t
E : A
π : (Functor.const (FullSubcategory fun f => S.arrows f.hom)ᵒᵖ).obj E ⟶ Functor.op (diagram S.arrows) ⋙ P
⊢ Nonempty (Unique ({ pt := E, π := π } ⟶ P.mapCone (Cocone.op (cocone S.arrows))))
case mpr
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows
hx : SieveCompatible x
⊢ (∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows), SieveCompatible x → ∃! t, IsAmalgamation x t) →
    ∀ (i : Cone (Functor.op (diagram S.arrows) ⋙ P)), Nonempty (Unique (i ⟶ P.mapCone (Cocone.op (cocone S.arrows))))
rintro h ⟨E, π⟩
case mpr.mk
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E✝ : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E✝) S.arrows
hx : SieveCompatible x
h : ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows), SieveCompatible x → ∃! t, IsAmalgamation x t
E : A
π : (Functor.const (FullSubcategory fun f => S.arrows f.hom)ᵒᵖ).obj E ⟶ Functor.op (diagram S.arrows) ⋙ P
eqv : (Functor.cones (Functor.op (diagram S.arrows) ⋙ P)).obj E.op ≃ { x // SieveCompatible x } :=
  conesEquivSieveCompatibleFamily P S E.op
⊢ Nonempty (Unique ({ pt := E, π := π } ⟶ P.mapCone (Cocone.op (cocone S.arrows))))
case mpr.mk
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E✝ : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E✝) S.arrows
hx : SieveCompatible x
h : ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows), SieveCompatible x → ∃! t, IsAmalgamation x t
E : A
π : (Functor.const (FullSubcategory fun f => S.arrows f.hom)ᵒᵖ).obj E ⟶ Functor.op (diagram S.arrows) ⋙ P
⊢ Nonempty (Unique ({ pt := E, π := π } ⟶ P.mapCone (Cocone.op (cocone S.arrows))))
let eqv := conesEquivSieveCompatibleFamily P S (op E)
case mpr.mk
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E✝ : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E✝) S.arrows
hx : SieveCompatible x
h : ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows), SieveCompatible x → ∃! t, IsAmalgamation x t
E : A
π : (Functor.const (FullSubcategory fun f => S.arrows f.hom)ᵒᵖ).obj E ⟶ Functor.op (diagram S.arrows) ⋙ P
eqv : (Functor.cones (Functor.op (diagram S.arrows) ⋙ P)).obj E.op ≃ { x // SieveCompatible x } :=
  conesEquivSieveCompatibleFamily P S E.op
⊢ Nonempty (Unique ({ pt := E, π := Equiv.invFun eqv (Equiv.toFun eqv π) } ⟶ P.mapCone (Cocone.op (cocone S.arrows))))
case mpr.mk
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E✝ : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E✝) S.arrows
hx : SieveCompatible x
h : ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows), SieveCompatible x → ∃! t, IsAmalgamation x t
E : A
π : (Functor.const (FullSubcategory fun f => S.arrows f.hom)ᵒᵖ).obj E ⟶ Functor.op (diagram S.arrows) ⋙ P
eqv : (Functor.cones (Functor.op (diagram S.arrows) ⋙ P)).obj E.op ≃ { x // SieveCompatible x } :=
  conesEquivSieveCompatibleFamily P S E.op
⊢ Nonempty (Unique ({ pt := E, π := π } ⟶ P.mapCone (Cocone.op (cocone S.arrows))))
rw [← eqv.left_inv π]
case mpr.mk
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E✝ : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E✝) S.arrows
hx : SieveCompatible x
h : ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows), SieveCompatible x → ∃! t, IsAmalgamation x t
E : A
π : (Functor.const (FullSubcategory fun f => S.arrows f.hom)ᵒᵖ).obj E ⟶ Functor.op (diagram S.arrows) ⋙ P
eqv : (Functor.cones (Functor.op (diagram S.arrows) ⋙ P)).obj E.op ≃ { x // SieveCompatible x } :=
  conesEquivSieveCompatibleFamily P S E.op
⊢ Nonempty (Unique { t // IsAmalgamation (↑(↑eqv π)) t })
case mpr.mk
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E✝ : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E✝) S.arrows
hx : SieveCompatible x
h : ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows), SieveCompatible x → ∃! t, IsAmalgamation x t
E : A
π : (Functor.const (FullSubcategory fun f => S.arrows f.hom)ᵒᵖ).obj E ⟶ Functor.op (diagram S.arrows) ⋙ P
eqv : (Functor.cones (Functor.op (diagram S.arrows) ⋙ P)).obj E.op ≃ { x // SieveCompatible x } :=
  conesEquivSieveCompatibleFamily P S E.op
⊢ Nonempty (Unique ({ pt := E, π := Equiv.invFun eqv (Equiv.toFun eqv π) } ⟶ P.mapCone (Cocone.op (cocone S.arrows))))
erw [(homEquivAmalgamation (eqv π).2).uniqueCongr.nonempty_congr]
case mpr.mk
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E✝ : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E✝) S.arrows
hx : SieveCompatible x
h : ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows), SieveCompatible x → ∃! t, IsAmalgamation x t
E : A
π : (Functor.const (FullSubcategory fun f => S.arrows f.hom)ᵒᵖ).obj E ⟶ Functor.op (diagram S.arrows) ⋙ P
eqv : (Functor.cones (Functor.op (diagram S.arrows) ⋙ P)).obj E.op ≃ { x // SieveCompatible x } :=
  conesEquivSieveCompatibleFamily P S E.op
⊢ ∃! a, IsAmalgamation (↑(↑eqv π)) a
case mpr.mk
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E✝ : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E✝) S.arrows
hx : SieveCompatible x
h : ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows), SieveCompatible x → ∃! t, IsAmalgamation x t
E : A
π : (Functor.const (FullSubcategory fun f => S.arrows f.hom)ᵒᵖ).obj E ⟶ Functor.op (diagram S.arrows) ⋙ P
eqv : (Functor.cones (Functor.op (diagram S.arrows) ⋙ P)).obj E.op ≃ { x // SieveCompatible x } :=
  conesEquivSieveCompatibleFamily P S E.op
⊢ Nonempty (Unique { t // IsAmalgamation (↑(↑eqv π)) t })
rw [unique_subtype_iff_exists_unique]
no goals
case mpr.mk
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E✝ : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E✝) S.arrows
hx : SieveCompatible x
h : ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows), SieveCompatible x → ∃! t, IsAmalgamation x t
E : A
π : (Functor.const (FullSubcategory fun f => S.arrows f.hom)ᵒᵖ).obj E ⟶ Functor.op (diagram S.arrows) ⋙ P
eqv : (Functor.cones (Functor.op (diagram S.arrows) ⋙ P)).obj E.op ≃ { x // SieveCompatible x } :=
  conesEquivSieveCompatibleFamily P S E.op
⊢ ∃! a, IsAmalgamation (↑(↑eqv π)) a
exact h _ _ (eqv π).2