internlm/Lean-Github huggingface dataset:
Theorem: Sieve.Yoneda_sheaf_iff_colimit
Proof state before:
case mpr
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
⊢ Nonempty (IsColimit (cocone S.arrows)) → ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
Tactic:
intro H W x hx
Proof state after:
case mpr
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
H : Nonempty (IsColimit (cocone S.arrows))
W : C
x : FamilyOfElements (yoneda.obj W) S.arrows
hx : FamilyOfElements.Compatible x
⊢ ∃! t, FamilyOfElements.IsAmalgamation x t
Theorem: Sieve.Yoneda_sheaf_iff_colimit
Proof state before:
case mpr
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
H : Nonempty (IsColimit (cocone S.arrows))
W : C
x : FamilyOfElements (yoneda.obj W) S.arrows
hx : FamilyOfElements.Compatible x
⊢ ∃! t, FamilyOfElements.IsAmalgamation x t
Tactic:
replace H := Classical.choice H
Proof state after:
case mpr
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
W : C
x : FamilyOfElements (yoneda.obj W) S.arrows
hx : FamilyOfElements.Compatible x
H : IsColimit (cocone S.arrows)
⊢ ∃! t, FamilyOfElements.IsAmalgamation x t
Theorem: Sieve.Yoneda_sheaf_iff_colimit
Proof state before:
case mpr
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
W : C
x : FamilyOfElements (yoneda.obj W) S.arrows
hx : FamilyOfElements.Compatible x
H : IsColimit (cocone S.arrows)
⊢ ∃! t, FamilyOfElements.IsAmalgamation x t
Tactic:
let s := Sieve.yonedafamily_toCocone W S x hx
Proof state after:
case mpr
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
W : C
x : FamilyOfElements (yoneda.obj W) S.arrows
hx : FamilyOfElements.Compatible x
H : IsColimit (cocone S.arrows)
s : Cocone (diagram S.arrows) := yonedafamily_toCocone W S.arrows x hx
⊢ ∃! t, FamilyOfElements.IsAmalgamation x t
Theorem: Sieve.Yoneda_sheaf_iff_colimit
Proof state before:
case mpr
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
W : C
x : FamilyOfElements (yoneda.obj W) S.arrows
hx : FamilyOfElements.Compatible x
H : IsColimit (cocone S.arrows)
s : Cocone (diagram S.arrows) := yonedafamily_toCocone W S.arrows x hx
⊢ ∃! t, FamilyOfElements.IsAmalgamation x t
Tactic:
use H.desc s
Proof state after:
case mpr
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
W : C
x : FamilyOfElements (yoneda.obj W) S.arrows
hx : FamilyOfElements.Compatible x
H : IsColimit (cocone S.arrows)
s : Cocone (diagram S.arrows) := yonedafamily_toCocone W S.arrows x hx
⊢ (fun t => FamilyOfElements.IsAmalgamation x t) (IsColimit.desc H s) ∧
    ∀ (y : (yoneda.obj W).obj X.op), (fun t => FamilyOfElements.IsAmalgamation x t) y → y = IsColimit.desc H s
Theorem: Sieve.Yoneda_sheaf_iff_colimit
Proof state before:
case mpr
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
W : C
x : FamilyOfElements (yoneda.obj W) S.arrows
hx : FamilyOfElements.Compatible x
H : IsColimit (cocone S.arrows)
s : Cocone (diagram S.arrows) := yonedafamily_toCocone W S.arrows x hx
⊢ (fun t => FamilyOfElements.IsAmalgamation x t) (IsColimit.desc H s) ∧
    ∀ (y : (yoneda.obj W).obj X.op), (fun t => FamilyOfElements.IsAmalgamation x t) y → y = IsColimit.desc H s
Tactic:
constructor
Proof state after:
case mpr.left
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
W : C
x : FamilyOfElements (yoneda.obj W) S.arrows
hx : FamilyOfElements.Compatible x
H : IsColimit (cocone S.arrows)
s : Cocone (diagram S.arrows) := yonedafamily_toCocone W S.arrows x hx
⊢ (fun t => FamilyOfElements.IsAmalgamation x t) (IsColimit.desc H s)

case mpr.right
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
W : C
x : FamilyOfElements (yoneda.obj W) S.arrows
hx : FamilyOfElements.Compatible x
H : IsColimit (cocone S.arrows)
s : Cocone (diagram S.arrows) := yonedafamily_toCocone W S.arrows x hx
⊢ ∀ (y : (yoneda.obj W).obj X.op), (fun t => FamilyOfElements.IsAmalgamation x t) y → y = IsColimit.desc H s
Theorem: Sieve.Yoneda_sheaf_iff_colimit
Proof state before:
case mpr.left
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
W : C
x : FamilyOfElements (yoneda.obj W) S.arrows
hx : FamilyOfElements.Compatible x
H : IsColimit (cocone S.arrows)
s : Cocone (diagram S.arrows) := yonedafamily_toCocone W S.arrows x hx
⊢ (fun t => FamilyOfElements.IsAmalgamation x t) (IsColimit.desc H s)
Tactic:
exact fun _ f hf => (H.fac s) ⟨Over.mk f, hf⟩
Proof state after:
no goals
Theorem: Sieve.Yoneda_sheaf_iff_colimit
Proof state before:
case mpr.right
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
W : C
x : FamilyOfElements (yoneda.obj W) S.arrows
hx : FamilyOfElements.Compatible x
H : IsColimit (cocone S.arrows)
s : Cocone (diagram S.arrows) := yonedafamily_toCocone W S.arrows x hx
⊢ ∀ (y : (yoneda.obj W).obj X.op), (fun t => FamilyOfElements.IsAmalgamation x t) y → y = IsColimit.desc H s
Tactic:
intro g hg
Proof state after:
case mpr.right
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
W : C
x : FamilyOfElements (yoneda.obj W) S.arrows
hx : FamilyOfElements.Compatible x
H : IsColimit (cocone S.arrows)
s : Cocone (diagram S.arrows) := yonedafamily_toCocone W S.arrows x hx
g : (yoneda.obj W).obj X.op
hg : FamilyOfElements.IsAmalgamation x g
⊢ g = IsColimit.desc H s
Theorem: Sieve.Yoneda_sheaf_iff_colimit
Proof state before:
case mpr.right
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
W : C
x : FamilyOfElements (yoneda.obj W) S.arrows
hx : FamilyOfElements.Compatible x
H : IsColimit (cocone S.arrows)
s : Cocone (diagram S.arrows) := yonedafamily_toCocone W S.arrows x hx
g : (yoneda.obj W).obj X.op
hg : FamilyOfElements.IsAmalgamation x g
⊢ g = IsColimit.desc H s
Tactic:
apply H.uniq s g
Proof state after:
case mpr.right
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
W : C
x : FamilyOfElements (yoneda.obj W) S.arrows
hx : FamilyOfElements.Compatible x
H : IsColimit (cocone S.arrows)
s : Cocone (diagram S.arrows) := yonedafamily_toCocone W S.arrows x hx
g : (yoneda.obj W).obj X.op
hg : FamilyOfElements.IsAmalgamation x g
⊢ ∀ (j : FullSubcategory fun f => S.arrows f.hom), (cocone S.arrows).ι.app j ≫ g = s.ι.app j
Theorem: Sieve.Yoneda_sheaf_iff_colimit
Proof state before:
case mpr.right
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
W : C
x : FamilyOfElements (yoneda.obj W) S.arrows
hx : FamilyOfElements.Compatible x
H : IsColimit (cocone S.arrows)
s : Cocone (diagram S.arrows) := yonedafamily_toCocone W S.arrows x hx
g : (yoneda.obj W).obj X.op
hg : FamilyOfElements.IsAmalgamation x g
⊢ ∀ (j : FullSubcategory fun f => S.arrows f.hom), (cocone S.arrows).ι.app j ≫ g = s.ι.app j
Tactic:
rintro ⟨⟨f, _, hom⟩, hf⟩
Proof state after:
case mpr.right.mk.mk
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
W : C
x : FamilyOfElements (yoneda.obj W) S.arrows
hx : FamilyOfElements.Compatible x
H : IsColimit (cocone S.arrows)
s : Cocone (diagram S.arrows) := yonedafamily_toCocone W S.arrows x hx
g : (yoneda.obj W).obj X.op
hg : FamilyOfElements.IsAmalgamation x g
f : C
right✝ : Discrete PUnit
hom : (𝟭 C).obj f ⟶ (Functor.fromPUnit X).obj right✝
hf : S.arrows { left := f, right := right✝, hom := hom }.hom
⊢ (cocone S.arrows).ι.app { obj := { left := f, right := right✝, hom := hom }, property := hf } ≫ g =
    s.ι.app { obj := { left := f, right := right✝, hom := hom }, property := hf }
Theorem: Sieve.Yoneda_sheaf_iff_colimit
Proof state before:
case mpr.right.mk.mk
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
W : C
x : FamilyOfElements (yoneda.obj W) S.arrows
hx : FamilyOfElements.Compatible x
H : IsColimit (cocone S.arrows)
s : Cocone (diagram S.arrows) := yonedafamily_toCocone W S.arrows x hx
g : (yoneda.obj W).obj X.op
hg : FamilyOfElements.IsAmalgamation x g
f : C
right✝ : Discrete PUnit
hom : (𝟭 C).obj f ⟶ (Functor.fromPUnit X).obj right✝
hf : S.arrows { left := f, right := right✝, hom := hom }.hom
⊢ (cocone S.arrows).ι.app { obj := { left := f, right := right✝, hom := hom }, property := hf } ≫ g =
    s.ι.app { obj := { left := f, right := right✝, hom := hom }, property := hf }
Tactic:
apply hg hom hf
Proof state after:
no goals
Theorem: coherentTopology.isSheaf_Yoneda
Proof state before:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X W : C
⊢ IsSheaf (coherentTopology C) (yoneda.obj W)
Tactic:
rw [isSheaf_coherent]
Proof state after:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X W : C
⊢ ∀ (B : C) (α : Type) [inst : Fintype α] (X : α → C) (π : (a : α) → X a ⟶ B),
    EffectiveEpiFamily X π → IsSheafFor (yoneda.obj W) (ofArrows X π)
Theorem: coherentTopology.isSheaf_Yoneda
Proof state before:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X W : C
⊢ ∀ (B : C) (α : Type) [inst : Fintype α] (X : α → C) (π : (a : α) → X a ⟶ B),
    EffectiveEpiFamily X π → IsSheafFor (yoneda.obj W) (ofArrows X π)
Tactic:
intro X α _ Y π H
Proof state after:
C : Type u
inst✝² : Category C
inst✝¹ : Precoherent C
X✝ W X : C
α : Type
inst✝ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
⊢ IsSheafFor (yoneda.obj W) (ofArrows Y π)
Theorem: coherentTopology.isSheaf_Yoneda
Proof state before:
C : Type u
inst✝² : Category C
inst✝¹ : Precoherent C
X✝ W X : C
α : Type
inst✝ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
⊢ IsSheafFor (yoneda.obj W) (ofArrows Y π)
Tactic:
have h_colim:= isColimitOfEffectiveEpiFamilyStruct Y π H.effectiveEpiFamily.some
Proof state after:
C : Type u
inst✝² : Category C
inst✝¹ : Precoherent C
X✝ W X : C
α : Type
inst✝ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : IsColimit (cocone (Sieve.generateFamily Y π).arrows)
⊢ IsSheafFor (yoneda.obj W) (ofArrows Y π)
Theorem: coherentTopology.isSheaf_Yoneda
Proof state before:
C : Type u
inst✝² : Category C
inst✝¹ : Precoherent C
X✝ W X : C
α : Type
inst✝ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : IsColimit (cocone (Sieve.generateFamily Y π).arrows)
⊢ IsSheafFor (yoneda.obj W) (ofArrows Y π)
Tactic:
rw [←Sieve.generateFamily_eq] at h_colim
Proof state after:
C : Type u
inst✝² : Category C
inst✝¹ : Precoherent C
X✝ W X : C
α : Type
inst✝ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : IsColimit (cocone (Sieve.generate (ofArrows Y π)).arrows)
⊢ IsSheafFor (yoneda.obj W) (ofArrows Y π)
Theorem: coherentTopology.isSheaf_Yoneda
Proof state before:
C : Type u
inst✝² : Category C
inst✝¹ : Precoherent C
X✝ W X : C
α : Type
inst✝ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : IsColimit (cocone (Sieve.generate (ofArrows Y π)).arrows)
⊢ IsSheafFor (yoneda.obj W) (ofArrows Y π)
Tactic:
intro x hx
Proof state after:
C : Type u
inst✝² : Category C
inst✝¹ : Precoherent C
X✝ W X : C
α : Type
inst✝ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : IsColimit (cocone (Sieve.generate (ofArrows Y π)).arrows)
x : FamilyOfElements (yoneda.obj W) (ofArrows Y π)
hx : FamilyOfElements.Compatible x
⊢ ∃! t, FamilyOfElements.IsAmalgamation x t
Theorem: coherentTopology.isSheaf_Yoneda
Proof state before:
C : Type u
inst✝² : Category C
inst✝¹ : Precoherent C
X✝ W X : C
α : Type
inst✝ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : IsColimit (cocone (Sieve.generate (ofArrows Y π)).arrows)
x : FamilyOfElements (yoneda.obj W) (ofArrows Y π)
hx : FamilyOfElements.Compatible x
⊢ ∃! t, FamilyOfElements.IsAmalgamation x t
Tactic:
let x_ext := FamilyOfElements.sieveExtend x
Proof state after:
C : Type u
inst✝² : Category C
inst✝¹ : Precoherent C
X✝ W X : C
α : Type
inst✝ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : IsColimit (cocone (Sieve.generate (ofArrows Y π)).arrows)
x : FamilyOfElements (yoneda.obj W) (ofArrows Y π)
hx : FamilyOfElements.Compatible x
x_ext : FamilyOfElements (yoneda.obj W) (Sieve.generate (ofArrows Y π)).arrows := FamilyOfElements.sieveExtend x
⊢ ∃! t, FamilyOfElements.IsAmalgamation x t
Theorem: coherentTopology.isSheaf_Yoneda
Proof state before:
C : Type u
inst✝² : Category C
inst✝¹ : Precoherent C
X✝ W X : C
α : Type
inst✝ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : IsColimit (cocone (Sieve.generate (ofArrows Y π)).arrows)
x : FamilyOfElements (yoneda.obj W) (ofArrows Y π)
hx : FamilyOfElements.Compatible x
x_ext : FamilyOfElements (yoneda.obj W) (Sieve.generate (ofArrows Y π)).arrows := FamilyOfElements.sieveExtend x
⊢ ∃! t, FamilyOfElements.IsAmalgamation x t
Tactic:
have hx_ext := FamilyOfElements.Compatible.sieveExtend hx
Proof state after:
C : Type u
inst✝² : Category C
inst✝¹ : Precoherent C
X✝ W X : C
α : Type
inst✝ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : IsColimit (cocone (Sieve.generate (ofArrows Y π)).arrows)
x : FamilyOfElements (yoneda.obj W) (ofArrows Y π)
hx : FamilyOfElements.Compatible x
x_ext : FamilyOfElements (yoneda.obj W) (Sieve.generate (ofArrows Y π)).arrows := FamilyOfElements.sieveExtend x
hx_ext : FamilyOfElements.Compatible (FamilyOfElements.sieveExtend x)
⊢ ∃! t, FamilyOfElements.IsAmalgamation x t
Theorem: coherentTopology.isSheaf_Yoneda
Proof state before:
C : Type u
inst✝² : Category C
inst✝¹ : Precoherent C
X✝ W X : C
α : Type
inst✝ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : IsColimit (cocone (Sieve.generate (ofArrows Y π)).arrows)
x : FamilyOfElements (yoneda.obj W) (ofArrows Y π)
hx : FamilyOfElements.Compatible x
x_ext : FamilyOfElements (yoneda.obj W) (Sieve.generate (ofArrows Y π)).arrows := FamilyOfElements.sieveExtend x
hx_ext : FamilyOfElements.Compatible (FamilyOfElements.sieveExtend x)
⊢ ∃! t, FamilyOfElements.IsAmalgamation x t
Tactic:
let S := Sieve.generate (ofArrows Y π)
Proof state after:
C : Type u
inst✝² : Category C
inst✝¹ : Precoherent C
X✝ W X : C
α : Type
inst✝ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : IsColimit (cocone (Sieve.generate (ofArrows Y π)).arrows)
x : FamilyOfElements (yoneda.obj W) (ofArrows Y π)
hx : FamilyOfElements.Compatible x
x_ext : FamilyOfElements (yoneda.obj W) (Sieve.generate (ofArrows Y π)).arrows := FamilyOfElements.sieveExtend x
hx_ext : FamilyOfElements.Compatible (FamilyOfElements.sieveExtend x)
S : Sieve X := Sieve.generate (ofArrows Y π)
⊢ ∃! t, FamilyOfElements.IsAmalgamation x t
Theorem: coherentTopology.isSheaf_Yoneda
Proof state before:
C : Type u
inst✝² : Category C
inst✝¹ : Precoherent C
X✝ W X : C
α : Type
inst✝ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : IsColimit (cocone (Sieve.generate (ofArrows Y π)).arrows)
x : FamilyOfElements (yoneda.obj W) (ofArrows Y π)
hx : FamilyOfElements.Compatible x
x_ext : FamilyOfElements (yoneda.obj W) (Sieve.generate (ofArrows Y π)).arrows := FamilyOfElements.sieveExtend x
hx_ext : FamilyOfElements.Compatible (FamilyOfElements.sieveExtend x)
S : Sieve X := Sieve.generate (ofArrows Y π)
⊢ ∃! t, FamilyOfElements.IsAmalgamation x t
Tactic:
have := (Sieve.Yoneda_sheaf_iff_colimit S).mpr ⟨h_colim⟩ W x_ext hx_ext
Proof state after:
C : Type u
inst✝² : Category C
inst✝¹ : Precoherent C
X✝ W X : C
α : Type
inst✝ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : IsColimit (cocone (Sieve.generate (ofArrows Y π)).arrows)
x : FamilyOfElements (yoneda.obj W) (ofArrows Y π)
hx : FamilyOfElements.Compatible x
x_ext : FamilyOfElements (yoneda.obj W) (Sieve.generate (ofArrows Y π)).arrows := FamilyOfElements.sieveExtend x
hx_ext : FamilyOfElements.Compatible (FamilyOfElements.sieveExtend x)
S : Sieve X := Sieve.generate (ofArrows Y π)
this : ∃! t, FamilyOfElements.IsAmalgamation x_ext t
⊢ ∃! t, FamilyOfElements.IsAmalgamation x t
Theorem: coherentTopology.isSheaf_Yoneda
Proof state before:
C : Type u
inst✝² : Category C
inst✝¹ : Precoherent C
X✝ W X : C
α : Type
inst✝ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : IsColimit (cocone (Sieve.generate (ofArrows Y π)).arrows)
x : FamilyOfElements (yoneda.obj W) (ofArrows Y π)
hx : FamilyOfElements.Compatible x
x_ext : FamilyOfElements (yoneda.obj W) (Sieve.generate (ofArrows Y π)).arrows := FamilyOfElements.sieveExtend x
hx_ext : FamilyOfElements.Compatible (FamilyOfElements.sieveExtend x)
S : Sieve X := Sieve.generate (ofArrows Y π)
this : ∃! t, FamilyOfElements.IsAmalgamation x_ext t
⊢ ∃! t, FamilyOfElements.IsAmalgamation x t
Tactic:
rcases this with ⟨t, t_amalg, t_uniq⟩
Proof state after:
case intro.intro
C : Type u
inst✝² : Category C
inst✝¹ : Precoherent C
X✝ W X : C
α : Type
inst✝ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : IsColimit (cocone (Sieve.generate (ofArrows Y π)).arrows)
x : FamilyOfElements (yoneda.obj W) (ofArrows Y π)
hx : FamilyOfElements.Compatible x
x_ext : FamilyOfElements (yoneda.obj W) (Sieve.generate (ofArrows Y π)).arrows := FamilyOfElements.sieveExtend x
hx_ext : FamilyOfElements.Compatible (FamilyOfElements.sieveExtend x)
S : Sieve X := Sieve.generate (ofArrows Y π)
t : (yoneda.obj W).obj X.op
t_amalg : FamilyOfElements.IsAmalgamation x_ext t
t_uniq : ∀ (y : (yoneda.obj W).obj X.op), (fun t => FamilyOfElements.IsAmalgamation x_ext t) y → y = t
⊢ ∃! t, FamilyOfElements.IsAmalgamation x t
Theorem: coherentTopology.isSheaf_Yoneda
Proof state before:
case intro.intro
C : Type u
inst✝² : Category C
inst✝¹ : Precoherent C
X✝ W X : C
α : Type
inst✝ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : IsColimit (cocone (Sieve.generate (ofArrows Y π)).arrows)
x : FamilyOfElements (yoneda.obj W) (ofArrows Y π)
hx : FamilyOfElements.Compatible x
x_ext : FamilyOfElements (yoneda.obj W) (Sieve.generate (ofArrows Y π)).arrows := FamilyOfElements.sieveExtend x
hx_ext : FamilyOfElements.Compatible (FamilyOfElements.sieveExtend x)
S : Sieve X := Sieve.generate (ofArrows Y π)
t : (yoneda.obj W).obj X.op
t_amalg : FamilyOfElements.IsAmalgamation x_ext t
t_uniq : ∀ (y : (yoneda.obj W).obj X.op), (fun t => FamilyOfElements.IsAmalgamation x_ext t) y → y = t
⊢ ∃! t, FamilyOfElements.IsAmalgamation x t
Tactic:
use t
Proof state after:
case intro.intro
C : Type u
inst✝² : Category C
inst✝¹ : Precoherent C
X✝ W X : C
α : Type
inst✝ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : IsColimit (cocone (Sieve.generate (ofArrows Y π)).arrows)
x : FamilyOfElements (yoneda.obj W) (ofArrows Y π)
hx : FamilyOfElements.Compatible x
x_ext : FamilyOfElements (yoneda.obj W) (Sieve.generate (ofArrows Y π)).arrows := FamilyOfElements.sieveExtend x
hx_ext : FamilyOfElements.Compatible (FamilyOfElements.sieveExtend x)
S : Sieve X := Sieve.generate (ofArrows Y π)
t : (yoneda.obj W).obj X.op
t_amalg : FamilyOfElements.IsAmalgamation x_ext t
t_uniq : ∀ (y : (yoneda.obj W).obj X.op), (fun t => FamilyOfElements.IsAmalgamation x_ext t) y → y = t
⊢ (fun t => FamilyOfElements.IsAmalgamation x t) t ∧
    ∀ (y : (yoneda.obj W).obj X.op), (fun t => FamilyOfElements.IsAmalgamation x t) y → y = t
Theorem: coherentTopology.isSheaf_Yoneda
Proof state before:
case intro.intro
C : Type u
inst✝² : Category C
inst✝¹ : Precoherent C
X✝ W X : C
α : Type
inst✝ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : IsColimit (cocone (Sieve.generate (ofArrows Y π)).arrows)
x : FamilyOfElements (yoneda.obj W) (ofArrows Y π)
hx : FamilyOfElements.Compatible x
x_ext : FamilyOfElements (yoneda.obj W) (Sieve.generate (ofArrows Y π)).arrows := FamilyOfElements.sieveExtend x
hx_ext : FamilyOfElements.Compatible (FamilyOfElements.sieveExtend x)
S : Sieve X := Sieve.generate (ofArrows Y π)
t : (yoneda.obj W).obj X.op
t_amalg : FamilyOfElements.IsAmalgamation x_ext t
t_uniq : ∀ (y : (yoneda.obj W).obj X.op), (fun t => FamilyOfElements.IsAmalgamation x_ext t) y → y = t
⊢ (fun t => FamilyOfElements.IsAmalgamation x t) t ∧
    ∀ (y : (yoneda.obj W).obj X.op), (fun t => FamilyOfElements.IsAmalgamation x t) y → y = t
Tactic:
constructor
Proof state after:
case intro.intro.left
C : Type u
inst✝² : Category C
inst✝¹ : Precoherent C
X✝ W X : C
α : Type
inst✝ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : IsColimit (cocone (Sieve.generate (ofArrows Y π)).arrows)
x : FamilyOfElements (yoneda.obj W) (ofArrows Y π)
hx : FamilyOfElements.Compatible x
x_ext : FamilyOfElements (yoneda.obj W) (Sieve.generate (ofArrows Y π)).arrows := FamilyOfElements.sieveExtend x
hx_ext : FamilyOfElements.Compatible (FamilyOfElements.sieveExtend x)
S : Sieve X := Sieve.generate (ofArrows Y π)
t : (yoneda.obj W).obj X.op
t_amalg : FamilyOfElements.IsAmalgamation x_ext t
t_uniq : ∀ (y : (yoneda.obj W).obj X.op), (fun t => FamilyOfElements.IsAmalgamation x_ext t) y → y = t
⊢ (fun t => FamilyOfElements.IsAmalgamation x t) t

case intro.intro.right
C : Type u
inst✝² : Category C
inst✝¹ : Precoherent C
X✝ W X : C
α : Type
inst✝ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : IsColimit (cocone (Sieve.generate (ofArrows Y π)).arrows)
x : FamilyOfElements (yoneda.obj W) (ofArrows Y π)
hx : FamilyOfElements.Compatible x
x_ext : FamilyOfElements (yoneda.obj W) (Sieve.generate (ofArrows Y π)).arrows := FamilyOfElements.sieveExtend x
hx_ext : FamilyOfElements.Compatible (FamilyOfElements.sieveExtend x)
S : Sieve X := Sieve.generate (ofArrows Y π)
t : (yoneda.obj W).obj X.op
t_amalg : FamilyOfElements.IsAmalgamation x_ext t
t_uniq : ∀ (y : (yoneda.obj W).obj X.op), (fun t => FamilyOfElements.IsAmalgamation x_ext t) y → y = t
⊢ ∀ (y : (yoneda.obj W).obj X.op), (fun t => FamilyOfElements.IsAmalgamation x t) y → y = t
Theorem: coherentTopology.isSheaf_Yoneda
Proof state before:
case intro.intro.left
C : Type u
inst✝² : Category C
inst✝¹ : Precoherent C
X✝ W X : C
α : Type
inst✝ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : IsColimit (cocone (Sieve.generate (ofArrows Y π)).arrows)
x : FamilyOfElements (yoneda.obj W) (ofArrows Y π)
hx : FamilyOfElements.Compatible x
x_ext : FamilyOfElements (yoneda.obj W) (Sieve.generate (ofArrows Y π)).arrows := FamilyOfElements.sieveExtend x
hx_ext : FamilyOfElements.Compatible (FamilyOfElements.sieveExtend x)
S : Sieve X := Sieve.generate (ofArrows Y π)
t : (yoneda.obj W).obj X.op
t_amalg : FamilyOfElements.IsAmalgamation x_ext t
t_uniq : ∀ (y : (yoneda.obj W).obj X.op), (fun t => FamilyOfElements.IsAmalgamation x_ext t) y → y = t
⊢ (fun t => FamilyOfElements.IsAmalgamation x t) t
Tactic:
convert Presieve.isAmalgamation_restrict (Sieve.le_generate (ofArrows Y π)) _ _ t_amalg
Proof state after:
case h.e.h.e'_6.h.h.h
C : Type u
inst✝² : Category C
inst✝¹ : Precoherent C
X✝ W X : C
α : Type
inst✝ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : IsColimit (cocone (Sieve.generate (ofArrows Y π)).arrows)
x : FamilyOfElements (yoneda.obj W) (ofArrows Y π)
hx : FamilyOfElements.Compatible x
x_ext : FamilyOfElements (yoneda.obj W) (Sieve.generate (ofArrows Y π)).arrows := FamilyOfElements.sieveExtend x
hx_ext : FamilyOfElements.Compatible (FamilyOfElements.sieveExtend x)
S : Sieve X := Sieve.generate (ofArrows Y π)
t : (yoneda.obj W).obj X.op
t_amalg : FamilyOfElements.IsAmalgamation x_ext t
t_uniq : ∀ (y : (yoneda.obj W).obj X.op), (fun t => FamilyOfElements.IsAmalgamation x_ext t) y → y = t
⊢ x = FamilyOfElements.restrict (_ : ofArrows Y π ≤ (Sieve.generate (ofArrows Y π)).arrows) x_ext
Theorem: coherentTopology.isSheaf_Yoneda
Proof state before:
case h.e.h.e'_6.h.h.h
C : Type u
inst✝² : Category C
inst✝¹ : Precoherent C
X✝ W X : C
α : Type
inst✝ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : IsColimit (cocone (Sieve.generate (ofArrows Y π)).arrows)
x : FamilyOfElements (yoneda.obj W) (ofArrows Y π)
hx : FamilyOfElements.Compatible x
x_ext : FamilyOfElements (yoneda.obj W) (Sieve.generate (ofArrows Y π)).arrows := FamilyOfElements.sieveExtend x
hx_ext : FamilyOfElements.Compatible (FamilyOfElements.sieveExtend x)
S : Sieve X := Sieve.generate (ofArrows Y π)
t : (yoneda.obj W).obj X.op
t_amalg : FamilyOfElements.IsAmalgamation x_ext t
t_uniq : ∀ (y : (yoneda.obj W).obj X.op), (fun t => FamilyOfElements.IsAmalgamation x_ext t) y → y = t
⊢ x = FamilyOfElements.restrict (_ : ofArrows Y π ≤ (Sieve.generate (ofArrows Y π)).arrows) x_ext
Tactic:
refine Eq.symm (restrict_extend hx)
Proof state after:
no goals