Theorem: coherentTopology.isSheaf_Yoneda (ExtrDisc/Topologies.lean)

State before:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X W : C
⊢ IsSheaf (coherentTopology C) (yoneda.obj W)
Tactic:
rw [isSheaf_coherent]
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 π)

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
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 π)

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
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 π)

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
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 π)

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
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

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
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

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
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

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 π)
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

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
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

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⟩
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

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
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

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
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

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
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

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)
State after:
no goals

State before:
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
Tactic:
exact fun y hy => t_uniq y <| isAmalgamation_sieveExtend x y hy
State after:
no goals