internlm/Lean-Github huggingface dataset:
Theorem: CategoryTheory.Equalizer.Presieve.sheaf_condition'
Proof state before:
case H.h.mp
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
x : Presieve.FamilyOfElements P S
h✝ : Presieve.FamilyOfElements.Compatible x
t : P.obj X.op
q : Presieve.FamilyOfElements.IsAmalgamation x t
⊢ ↑(firstObjEqFamily P S).toEquiv (forkMap P (fun {Y} {f} => S f) t) = x
Tactic:
funext Y f hf
Proof state after:
case H.h.mp.h.h.h
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
x : Presieve.FamilyOfElements P S
h✝ : Presieve.FamilyOfElements.Compatible x
t : P.obj X.op
q : Presieve.FamilyOfElements.IsAmalgamation x t
Y : C
f : Y ⟶ X
hf : S f
⊢ ↑(firstObjEqFamily P S).toEquiv (forkMap P (fun {Y} {f} => S f) t) f hf = x f hf
Theorem: CategoryTheory.Equalizer.Presieve.sheaf_condition'
Proof state before:
case H.h.mp.h.h.h
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
x : Presieve.FamilyOfElements P S
h✝ : Presieve.FamilyOfElements.Compatible x
t : P.obj X.op
q : Presieve.FamilyOfElements.IsAmalgamation x t
Y : C
f : Y ⟶ X
hf : S f
⊢ ↑(firstObjEqFamily P S).toEquiv (forkMap P (fun {Y} {f} => S f) t) f hf = x f hf
Tactic:
simpa [forkMap] using q _ _
Proof state after:
no goals
Theorem: CategoryTheory.Equalizer.Presieve.sheaf_condition'
Proof state before:
case H.h.mpr
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
x : Presieve.FamilyOfElements P S
h✝ : Presieve.FamilyOfElements.Compatible x
t : P.obj X.op
⊢ ↑(firstObjEqFamily P S).toEquiv (forkMap P (fun {Y} {f} => S f) t) = x → Presieve.FamilyOfElements.IsAmalgamation x t
Tactic:
intro q Y f hf
Proof state after:
case H.h.mpr
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
x : Presieve.FamilyOfElements P S
h✝ : Presieve.FamilyOfElements.Compatible x
t : P.obj X.op
q : ↑(firstObjEqFamily P S).toEquiv (forkMap P (fun {Y} {f} => S f) t) = x
Y : C
f : Y ⟶ X
hf : S f
⊢ P.map f.op t = x f hf
Theorem: CategoryTheory.Equalizer.Presieve.sheaf_condition'
Proof state before:
case H.h.mpr
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
x : Presieve.FamilyOfElements P S
h✝ : Presieve.FamilyOfElements.Compatible x
t : P.obj X.op
q : ↑(firstObjEqFamily P S).toEquiv (forkMap P (fun {Y} {f} => S f) t) = x
Y : C
f : Y ⟶ X
hf : S f
⊢ P.map f.op t = x f hf
Tactic:
rw [← q]
Proof state after:
case H.h.mpr
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
x : Presieve.FamilyOfElements P S
h✝ : Presieve.FamilyOfElements.Compatible x
t : P.obj X.op
q : ↑(firstObjEqFamily P S).toEquiv (forkMap P (fun {Y} {f} => S f) t) = x
Y : C
f : Y ⟶ X
hf : S f
⊢ P.map f.op t = ↑(firstObjEqFamily P S).toEquiv (forkMap P (fun {Y} {f} => S f) t) f hf
Theorem: CategoryTheory.Equalizer.Presieve.sheaf_condition'
Proof state before:
case H.h.mpr
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
x : Presieve.FamilyOfElements P S
h✝ : Presieve.FamilyOfElements.Compatible x
t : P.obj X.op
q : ↑(firstObjEqFamily P S).toEquiv (forkMap P (fun {Y} {f} => S f) t) = x
Y : C
f : Y ⟶ X
hf : S f
⊢ P.map f.op t = ↑(firstObjEqFamily P S).toEquiv (forkMap P (fun {Y} {f} => S f) t) f hf
Tactic:
simp [forkMap]
Proof state after:
no goals
Theorem: Condensed.isSheaf_iff_conditions
Proof state before:
C : Type w
inst✝ : Category C
P : CompHausᵒᵖ ⥤ C
⊢ Presheaf.IsSheaf (coherentTopology CompHaus) P ↔ ProductCondition P ∧ EqualizerCondition P
Tactic:
constructor
Proof state after:
case mp
C : Type w
inst✝ : Category C
P : CompHausᵒᵖ ⥤ C
⊢ Presheaf.IsSheaf (coherentTopology CompHaus) P → ProductCondition P ∧ EqualizerCondition P

case mpr
C : Type w
inst✝ : Category C
P : CompHausᵒᵖ ⥤ C
⊢ ProductCondition P ∧ EqualizerCondition P → Presheaf.IsSheaf (coherentTopology CompHaus) P
Theorem: Condensed.isSheaf_iff_conditions
Proof state before:
case mp
C : Type w
inst✝ : Category C
P : CompHausᵒᵖ ⥤ C
⊢ Presheaf.IsSheaf (coherentTopology CompHaus) P → ProductCondition P ∧ EqualizerCondition P
Tactic:
intro H
Proof state after:
case mp
C : Type w
inst✝ : Category C
P : CompHausᵒᵖ ⥤ C
H : Presheaf.IsSheaf (coherentTopology CompHaus) P
⊢ ProductCondition P ∧ EqualizerCondition P
Theorem: Condensed.isSheaf_iff_conditions
Proof state before:
case mp
C : Type w
inst✝ : Category C
P : CompHausᵒᵖ ⥤ C
H : Presheaf.IsSheaf (coherentTopology CompHaus) P
⊢ ProductCondition P ∧ EqualizerCondition P
Tactic:
constructor
Proof state after:
case mp.left
C : Type w
inst✝ : Category C
P : CompHausᵒᵖ ⥤ C
H : Presheaf.IsSheaf (coherentTopology CompHaus) P
⊢ ProductCondition P

case mp.right
C : Type w
inst✝ : Category C
P : CompHausᵒᵖ ⥤ C
H : Presheaf.IsSheaf (coherentTopology CompHaus) P
⊢ EqualizerCondition P
Theorem: Condensed.isSheaf_iff_conditions
Proof state before:
case mp.left
C : Type w
inst✝ : Category C
P : CompHausᵒᵖ ⥤ C
H : Presheaf.IsSheaf (coherentTopology CompHaus) P
⊢ ProductCondition P
Tactic:
intro α _ X
Proof state after:
case mp.left
C : Type w
inst✝¹ : Category C
P : CompHausᵒᵖ ⥤ C
H : Presheaf.IsSheaf (coherentTopology CompHaus) P
α : Type
inst✝ : Fintype α
X : α → CompHaus
⊢ Nonempty (IsLimit (productFan P X))
Theorem: Condensed.isSheaf_iff_conditions
Proof state before:
case mp.left
C : Type w
inst✝¹ : Category C
P : CompHausᵒᵖ ⥤ C
H : Presheaf.IsSheaf (coherentTopology CompHaus) P
α : Type
inst✝ : Fintype α
X : α → CompHaus
⊢ Nonempty (IsLimit (productFan P X))
Tactic:
let B := ∐ X
Proof state after:
case mp.left
C : Type w
inst✝¹ : Category C
P : CompHausᵒᵖ ⥤ C
H : Presheaf.IsSheaf (coherentTopology CompHaus) P
α : Type
inst✝ : Fintype α
X : α → CompHaus
B : CompHaus := ∐ X
⊢ Nonempty (IsLimit (productFan P X))
Theorem: Condensed.isSheaf_iff_conditions
Proof state before:
case mp.left
C : Type w
inst✝¹ : Category C
P : CompHausᵒᵖ ⥤ C
H : Presheaf.IsSheaf (coherentTopology CompHaus) P
α : Type
inst✝ : Fintype α
X : α → CompHaus
B : CompHaus := ∐ X
⊢ Nonempty (IsLimit (productFan P X))
Tactic:
let π : (a : α) → (X a ⟶ B) := 
  Sigma.ι X
Proof state after:
case mp.left
C : Type w
inst✝¹ : Category C
P : CompHausᵒᵖ ⥤ C
H : Presheaf.IsSheaf (coherentTopology CompHaus) P
α : Type
inst✝ : Fintype α
X : α → CompHaus
B : CompHaus := ∐ X
π : (a : α) → X a ⟶ B := Sigma.ι X
⊢ Nonempty (IsLimit (productFan P X))
Theorem: Condensed.isSheaf_iff_conditions
Proof state before:
case mp.left
C : Type w
inst✝¹ : Category C
P : CompHausᵒᵖ ⥤ C
H : Presheaf.IsSheaf (coherentTopology CompHaus) P
α : Type
inst✝ : Fintype α
X : α → CompHaus
B : CompHaus := ∐ X
π : (a : α) → X a ⟶ B := Sigma.ι X
⊢ Nonempty (IsLimit (productFan P X))
Tactic:
have : EffectiveEpiFamily X π := sorry
Proof state after:
case mp.left
C : Type w
inst✝¹ : Category C
P : CompHausᵒᵖ ⥤ C
H : Presheaf.IsSheaf (coherentTopology CompHaus) P
α : Type
inst✝ : Fintype α
X : α → CompHaus
B : CompHaus := ∐ X
π : (a : α) → X a ⟶ B := Sigma.ι X
this : EffectiveEpiFamily X π
⊢ Nonempty (IsLimit (productFan P X))
Theorem: Condensed.isSheaf_iff_conditions
Proof state before:
case mp.left
C : Type w
inst✝¹ : Category C
P : CompHausᵒᵖ ⥤ C
H : Presheaf.IsSheaf (coherentTopology CompHaus) P
α : Type
inst✝ : Fintype α
X : α → CompHaus
B : CompHaus := ∐ X
π : (a : α) → X a ⟶ B := Sigma.ι X
this : EffectiveEpiFamily X π
⊢ Nonempty (IsLimit (productFan P X))
Tactic:
specialize H (P.obj <| op B)
Proof state after:
case mp.left
C : Type w
inst✝¹ : Category C
P : CompHausᵒᵖ ⥤ C
α : Type
inst✝ : Fintype α
X : α → CompHaus
B : CompHaus := ∐ X
π : (a : α) → X a ⟶ B := Sigma.ι X
this : EffectiveEpiFamily X π
H : Presieve.IsSheaf (coherentTopology CompHaus) (P ⋙ coyoneda.obj (P.obj B.op).op)
⊢ Nonempty (IsLimit (productFan P X))
Theorem: Condensed.isSheaf_iff_conditions
Proof state before:
case mp.left
C : Type w
inst✝¹ : Category C
P : CompHausᵒᵖ ⥤ C
α : Type
inst✝ : Fintype α
X : α → CompHaus
B : CompHaus := ∐ X
π : (a : α) → X a ⟶ B := Sigma.ι X
this : EffectiveEpiFamily X π
H : Presieve.IsSheaf (coherentTopology CompHaus) (P ⋙ coyoneda.obj (P.obj B.op).op)
⊢ Nonempty (IsLimit (productFan P X))
Tactic:
erw [Presieve.isSheaf_coverage] at H
Proof state after:
case mp.left
C : Type w
inst✝¹ : Category C
P : CompHausᵒᵖ ⥤ C
α : Type
inst✝ : Fintype α
X : α → CompHaus
B : CompHaus := ∐ X
π : (a : α) → X a ⟶ B := Sigma.ι X
this : EffectiveEpiFamily X π
H :
  ∀ {X : CompHaus} (R : Presieve X),
    R ∈ Coverage.covering (coherentCoverage CompHaus) X → Presieve.IsSheafFor (P ⋙ coyoneda.obj (P.obj B.op).op) R
⊢ Nonempty (IsLimit (productFan P X))
Theorem: Condensed.isSheaf_iff_conditions
Proof state before:
case mp.left
C : Type w
inst✝¹ : Category C
P : CompHausᵒᵖ ⥤ C
α : Type
inst✝ : Fintype α
X : α → CompHaus
B : CompHaus := ∐ X
π : (a : α) → X a ⟶ B := Sigma.ι X
this : EffectiveEpiFamily X π
H :
  ∀ {X : CompHaus} (R : Presieve X),
    R ∈ Coverage.covering (coherentCoverage CompHaus) X → Presieve.IsSheafFor (P ⋙ coyoneda.obj (P.obj B.op).op) R
⊢ Nonempty (IsLimit (productFan P X))
Tactic:
specialize H (Presieve.ofArrows X π) ?_
Proof state after:
case mp.left
C : Type w
inst✝¹ : Category C
P : CompHausᵒᵖ ⥤ C
α : Type
inst✝ : Fintype α
X : α → CompHaus
B : CompHaus := ∐ X
π : (a : α) → X a ⟶ B := Sigma.ι X
this : EffectiveEpiFamily X π
H :
  ∀ {X : CompHaus} (R : Presieve X),
    R ∈ Coverage.covering (coherentCoverage CompHaus) X → Presieve.IsSheafFor (P ⋙ coyoneda.obj (P.obj B.op).op) R
⊢ Presieve.ofArrows X π ∈ Coverage.covering (coherentCoverage CompHaus) B

case mp.left
C : Type w
inst✝¹ : Category C
P : CompHausᵒᵖ ⥤ C
α : Type
inst✝ : Fintype α
X : α → CompHaus
B : CompHaus := ∐ X
π : (a : α) → X a ⟶ B := Sigma.ι X
this : EffectiveEpiFamily X π
H : Presieve.IsSheafFor (P ⋙ coyoneda.obj (P.obj B.op).op) (Presieve.ofArrows X π)
⊢ Nonempty (IsLimit (productFan P X))
Theorem: Condensed.isSheaf_iff_conditions
Proof state before:
case mp.left
C : Type w
inst✝¹ : Category C
P : CompHausᵒᵖ ⥤ C
α : Type
inst✝ : Fintype α
X : α → CompHaus
B : CompHaus := ∐ X
π : (a : α) → X a ⟶ B := Sigma.ι X
this : EffectiveEpiFamily X π
H : Presieve.IsSheafFor (P ⋙ coyoneda.obj (P.obj B.op).op) (Presieve.ofArrows X π)
⊢ Nonempty (IsLimit (productFan P X))
Tactic:
sorry
Proof state after:
no goals
Theorem: Condensed.isSheaf_iff_conditions
Proof state before:
case mp.left
C : Type w
inst✝¹ : Category C
P : CompHausᵒᵖ ⥤ C
α : Type
inst✝ : Fintype α
X : α → CompHaus
B : CompHaus := ∐ X
π : (a : α) → X a ⟶ B := Sigma.ι X
this : EffectiveEpiFamily X π
H :
  ∀ {X : CompHaus} (R : Presieve X),
    R ∈ Coverage.covering (coherentCoverage CompHaus) X → Presieve.IsSheafFor (P ⋙ coyoneda.obj (P.obj B.op).op) R
⊢ Presieve.ofArrows X π ∈ Coverage.covering (coherentCoverage CompHaus) B
Tactic:
sorry
Proof state after:
no goals
Theorem: Condensed.isSheaf_iff_conditions
Proof state before:
case mp.right
C : Type w
inst✝ : Category C
P : CompHausᵒᵖ ⥤ C
H : Presheaf.IsSheaf (coherentTopology CompHaus) P
⊢ EqualizerCondition P
Tactic:
sorry
Proof state after:
no goals
Theorem: Condensed.isSheaf_iff_conditions
Proof state before:
case mpr
C : Type w
inst✝ : Category C
P : CompHausᵒᵖ ⥤ C
⊢ ProductCondition P ∧ EqualizerCondition P → Presheaf.IsSheaf (coherentTopology CompHaus) P
Tactic:
intro ⟨H1,H2⟩
Proof state after:
case mpr
C : Type w
inst✝ : Category C
P : CompHausᵒᵖ ⥤ C
H1 : ProductCondition P
H2 : EqualizerCondition P
⊢ Presheaf.IsSheaf (coherentTopology CompHaus) P
Theorem: Condensed.isSheaf_iff_conditions
Proof state before:
case mpr
C : Type w
inst✝ : Category C
P : CompHausᵒᵖ ⥤ C
H1 : ProductCondition P
H2 : EqualizerCondition P
⊢ Presheaf.IsSheaf (coherentTopology CompHaus) P
Tactic:
intro T
Proof state after:
case mpr
C : Type w
inst✝ : Category C
P : CompHausᵒᵖ ⥤ C
H1 : ProductCondition P
H2 : EqualizerCondition P
T : C
⊢ Presieve.IsSheaf (coherentTopology CompHaus) (P ⋙ coyoneda.obj T.op)
Theorem: Condensed.isSheaf_iff_conditions
Proof state before:
case mpr
C : Type w
inst✝ : Category C
P : CompHausᵒᵖ ⥤ C
H1 : ProductCondition P
H2 : EqualizerCondition P
T : C
⊢ Presieve.IsSheaf (coherentTopology CompHaus) (P ⋙ coyoneda.obj T.op)
Tactic:
erw [Presieve.isSheaf_coverage]
Proof state after:
case mpr
C : Type w
inst✝ : Category C
P : CompHausᵒᵖ ⥤ C
H1 : ProductCondition P
H2 : EqualizerCondition P
T : C
⊢ ∀ {X : CompHaus} (R : Presieve X),
    R ∈ Coverage.covering (coherentCoverage CompHaus) X → Presieve.IsSheafFor (P ⋙ coyoneda.obj T.op) R
Theorem: Condensed.isSheaf_iff_conditions
Proof state before:
case mpr
C : Type w
inst✝ : Category C
P : CompHausᵒᵖ ⥤ C
H1 : ProductCondition P
H2 : EqualizerCondition P
T : C
⊢ ∀ {X : CompHaus} (R : Presieve X),
    R ∈ Coverage.covering (coherentCoverage CompHaus) X → Presieve.IsSheafFor (P ⋙ coyoneda.obj T.op) R
Tactic:
rintro B R ⟨α, _, X, π, rfl, H⟩
Proof state after:
case mpr.intro.intro.intro.intro.intro
C : Type w
inst✝ : Category C
P : CompHausᵒᵖ ⥤ C
H1 : ProductCondition P
H2 : EqualizerCondition P
T : C
B : CompHaus
α : Type
w✝ : Fintype α
X : α → CompHaus
π : (a : α) → X a ⟶ B
H : EffectiveEpiFamily X π
⊢ Presieve.IsSheafFor (P ⋙ coyoneda.obj T.op) (Presieve.ofArrows X π)
Theorem: Condensed.isSheaf_iff_conditions
Proof state before:
case mpr.intro.intro.intro.intro.intro
C : Type w
inst✝ : Category C
P : CompHausᵒᵖ ⥤ C
H1 : ProductCondition P
H2 : EqualizerCondition P
T : C
B : CompHaus
α : Type
w✝ : Fintype α
X : α → CompHaus
π : (a : α) → X a ⟶ B
H : EffectiveEpiFamily X π
⊢ Presieve.IsSheafFor (P ⋙ coyoneda.obj T.op) (Presieve.ofArrows X π)
Tactic:
specialize H2 (Sigma.desc π)
Proof state after:
case mpr.intro.intro.intro.intro.intro
C : Type w
inst✝ : Category C
P : CompHausᵒᵖ ⥤ C
H1 : ProductCondition P
T : C
B : CompHaus
α : Type
w✝ : Fintype α
X : α → CompHaus
π : (a : α) → X a ⟶ B
H : EffectiveEpiFamily X π
H2 : Nonempty (IsLimit (equalizerFork P (Sigma.desc π)))
⊢ Presieve.IsSheafFor (P ⋙ coyoneda.obj T.op) (Presieve.ofArrows X π)
Theorem: Condensed.isSheaf_iff_conditions
Proof state before:
case mpr.intro.intro.intro.intro.intro
C : Type w
inst✝ : Category C
P : CompHausᵒᵖ ⥤ C
H1 : ProductCondition P
T : C
B : CompHaus
α : Type
w✝ : Fintype α
X : α → CompHaus
π : (a : α) → X a ⟶ B
H : EffectiveEpiFamily X π
H2 : Nonempty (IsLimit (equalizerFork P (Sigma.desc π)))
⊢ Presieve.IsSheafFor (P ⋙ coyoneda.obj T.op) (Presieve.ofArrows X π)
Tactic:
rw [isSheafFor_ofArrows]
Proof state after:
case mpr.intro.intro.intro.intro.intro
C : Type w
inst✝ : Category C
P : CompHausᵒᵖ ⥤ C
H1 : ProductCondition P
T : C
B : CompHaus
α : Type
w✝ : Fintype α
X : α → CompHaus
π : (a : α) → X a ⟶ B
H : EffectiveEpiFamily X π
H2 : Nonempty (IsLimit (equalizerFork P (Sigma.desc π)))
⊢ ∀ (x : (a : α) → (P ⋙ coyoneda.obj T.op).obj (X a).op),
    (∀ (R : CompHaus) (i j : α) (ri : R ⟶ X i) (rj : R ⟶ X j),
        (P ⋙ coyoneda.obj T.op).map ri.op (x i) = (P ⋙ coyoneda.obj T.op).map rj.op (x j)) →
      ∃! b, ∀ (i : α), (P ⋙ coyoneda.obj T.op).map (π i).op b = x i
Theorem: Condensed.isSheaf_iff_conditions
Proof state before:
case mpr.intro.intro.intro.intro.intro
C : Type w
inst✝ : Category C
P : CompHausᵒᵖ ⥤ C
H1 : ProductCondition P
T : C
B : CompHaus
α : Type
w✝ : Fintype α
X : α → CompHaus
π : (a : α) → X a ⟶ B
H : EffectiveEpiFamily X π
H2 : Nonempty (IsLimit (equalizerFork P (Sigma.desc π)))
⊢ ∀ (x : (a : α) → (P ⋙ coyoneda.obj T.op).obj (X a).op),
    (∀ (R : CompHaus) (i j : α) (ri : R ⟶ X i) (rj : R ⟶ X j),
        (P ⋙ coyoneda.obj T.op).map ri.op (x i) = (P ⋙ coyoneda.obj T.op).map rj.op (x j)) →
      ∃! b, ∀ (i : α), (P ⋙ coyoneda.obj T.op).map (π i).op b = x i
Tactic:
intro x hx
Proof state after:
case mpr.intro.intro.intro.intro.intro
C : Type w
inst✝ : Category C
P : CompHausᵒᵖ ⥤ C
H1 : ProductCondition P
T : C
B : CompHaus
α : Type
w✝ : Fintype α
X : α → CompHaus
π : (a : α) → X a ⟶ B
H : EffectiveEpiFamily X π
H2 : Nonempty (IsLimit (equalizerFork P (Sigma.desc π)))
x : (a : α) → (P ⋙ coyoneda.obj T.op).obj (X a).op
hx :
  ∀ (R : CompHaus) (i j : α) (ri : R ⟶ X i) (rj : R ⟶ X j),
    (P ⋙ coyoneda.obj T.op).map ri.op (x i) = (P ⋙ coyoneda.obj T.op).map rj.op (x j)
⊢ ∃! b, ∀ (i : α), (P ⋙ coyoneda.obj T.op).map (π i).op b = x i
Theorem: Condensed.isSheaf_iff_conditions
Proof state before:
case mpr.intro.intro.intro.intro.intro
C : Type w
inst✝ : Category C
P : CompHausᵒᵖ ⥤ C
H1 : ProductCondition P
T : C
B : CompHaus
α : Type
w✝ : Fintype α
X : α → CompHaus
π : (a : α) → X a ⟶ B
H : EffectiveEpiFamily X π
H2 : Nonempty (IsLimit (equalizerFork P (Sigma.desc π)))
x : (a : α) → (P ⋙ coyoneda.obj T.op).obj (X a).op
hx :
  ∀ (R : CompHaus) (i j : α) (ri : R ⟶ X i) (rj : R ⟶ X j),
    (P ⋙ coyoneda.obj T.op).map ri.op (x i) = (P ⋙ coyoneda.obj T.op).map rj.op (x j)
⊢ ∃! b, ∀ (i : α), (P ⋙ coyoneda.obj T.op).map (π i).op b = x i
Tactic:
dsimp at x
Proof state after:
case mpr.intro.intro.intro.intro.intro
C : Type w
inst✝ : Category C
P : CompHausᵒᵖ ⥤ C
H1 : ProductCondition P
T : C
B : CompHaus
α : Type
w✝ : Fintype α
X : α → CompHaus
π : (a : α) → X a ⟶ B
H : EffectiveEpiFamily X π
H2 : Nonempty (IsLimit (equalizerFork P (Sigma.desc π)))
x : (a : α) → T ⟶ P.obj (X a).op
hx :
  ∀ (R : CompHaus) (i j : α) (ri : R ⟶ X i) (rj : R ⟶ X j),
    (P ⋙ coyoneda.obj T.op).map ri.op (x i) = (P ⋙ coyoneda.obj T.op).map rj.op (x j)
⊢ ∃! b, ∀ (i : α), (P ⋙ coyoneda.obj T.op).map (π i).op b = x i
Theorem: Condensed.isSheaf_iff_conditions
Proof state before:
case mpr.intro.intro.intro.intro.intro
C : Type w
inst✝ : Category C
P : CompHausᵒᵖ ⥤ C
H1 : ProductCondition P
T : C
B : CompHaus
α : Type
w✝ : Fintype α
X : α → CompHaus
π : (a : α) → X a ⟶ B
H : EffectiveEpiFamily X π
H2 : Nonempty (IsLimit (equalizerFork P (Sigma.desc π)))
x : (a : α) → T ⟶ P.obj (X a).op
hx :
  ∀ (R : CompHaus) (i j : α) (ri : R ⟶ X i) (rj : R ⟶ X j),
    (P ⋙ coyoneda.obj T.op).map ri.op (x i) = (P ⋙ coyoneda.obj T.op).map rj.op (x j)
⊢ ∃! b, ∀ (i : α), (P ⋙ coyoneda.obj T.op).map (π i).op b = x i
Tactic:
sorry
Proof state after:
no goals
Theorem: ExtrDisc.Sheaf.isSheafColimitAux
Proof state before:
A : Type (u + 2)
inst✝⁴ : Category A
inst✝³ : HasZeroMorphisms A
inst✝² : HasFiniteBiproducts A
J : Type (u + 1)
inst✝¹ : SmallCategory J
F : J ⥤ ExtrDiscᵒᵖ ⥤ A
inst✝ : HasColimit F
h : ∀ (j : J), Presheaf.IsSheaf (coherentTopology ExtrDisc) (F.obj j)
⊢ Presheaf.IsSheaf (coherentTopology ExtrDisc) (colimit F)
Tactic:
rw [sheafCondition]
Proof state after:
A : Type (u + 2)
inst✝⁴ : Category A
inst✝³ : HasZeroMorphisms A
inst✝² : HasFiniteBiproducts A
J : Type (u + 1)
inst✝¹ : SmallCategory J
F : J ⥤ ExtrDiscᵒᵖ ⥤ A
inst✝ : HasColimit F
h : ∀ (j : J), Presheaf.IsSheaf (coherentTopology ExtrDisc) (F.obj j)
⊢ Nonempty (PreservesFiniteProducts (colimit F))
Theorem: ExtrDisc.Sheaf.isSheafColimitAux
Proof state before:
A : Type (u + 2)
inst✝⁴ : Category A
inst✝³ : HasZeroMorphisms A
inst✝² : HasFiniteBiproducts A
J : Type (u + 1)
inst✝¹ : SmallCategory J
F : J ⥤ ExtrDiscᵒᵖ ⥤ A
inst✝ : HasColimit F
h : ∀ (j : J), Presheaf.IsSheaf (coherentTopology ExtrDisc) (F.obj j)
⊢ Nonempty (PreservesFiniteProducts (colimit F))
Tactic:
exact ⟨preservesFiniteProducts _ h⟩
Proof state after:
no goals
Theorem: ExtrDisc.Sheaf.isSheafColimit
Proof state before:
A : Type (u + 2)
inst✝⁴ : Category A
inst✝³ : HasZeroMorphisms A
inst✝² : HasFiniteBiproducts A
J : Type (u + 1)
inst✝¹ : SmallCategory J
F✝ : J ⥤ ExtrDiscᵒᵖ ⥤ A
F : J ⥤ Sheaf (coherentTopology ExtrDisc) A
inst✝ : HasColimit (F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A)
⊢ Presheaf.IsSheaf (coherentTopology ExtrDisc) (colimit (F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A))
Tactic:
apply isSheafColimitAux
Proof state after:
case h
A : Type (u + 2)
inst✝⁴ : Category A
inst✝³ : HasZeroMorphisms A
inst✝² : HasFiniteBiproducts A
J : Type (u + 1)
inst✝¹ : SmallCategory J
F✝ : J ⥤ ExtrDiscᵒᵖ ⥤ A
F : J ⥤ Sheaf (coherentTopology ExtrDisc) A
inst✝ : HasColimit (F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A)
⊢ ∀ (j : J), Presheaf.IsSheaf (coherentTopology ExtrDisc) ((F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A).obj j)
Theorem: ExtrDisc.Sheaf.isSheafColimit
Proof state before:
case h
A : Type (u + 2)
inst✝⁴ : Category A
inst✝³ : HasZeroMorphisms A
inst✝² : HasFiniteBiproducts A
J : Type (u + 1)
inst✝¹ : SmallCategory J
F✝ : J ⥤ ExtrDiscᵒᵖ ⥤ A
F : J ⥤ Sheaf (coherentTopology ExtrDisc) A
inst✝ : HasColimit (F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A)
⊢ ∀ (j : J), Presheaf.IsSheaf (coherentTopology ExtrDisc) ((F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A).obj j)
Tactic:
intro j
Proof state after:
case h
A : Type (u + 2)
inst✝⁴ : Category A
inst✝³ : HasZeroMorphisms A
inst✝² : HasFiniteBiproducts A
J : Type (u + 1)
inst✝¹ : SmallCategory J
F✝ : J ⥤ ExtrDiscᵒᵖ ⥤ A
F : J ⥤ Sheaf (coherentTopology ExtrDisc) A
inst✝ : HasColimit (F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A)
j : J
⊢ Presheaf.IsSheaf (coherentTopology ExtrDisc) ((F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A).obj j)
Theorem: ExtrDisc.Sheaf.isSheafColimit
Proof state before:
case h
A : Type (u + 2)
inst✝⁴ : Category A
inst✝³ : HasZeroMorphisms A
inst✝² : HasFiniteBiproducts A
J : Type (u + 1)
inst✝¹ : SmallCategory J
F✝ : J ⥤ ExtrDiscᵒᵖ ⥤ A
F : J ⥤ Sheaf (coherentTopology ExtrDisc) A
inst✝ : HasColimit (F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A)
j : J
⊢ Presheaf.IsSheaf (coherentTopology ExtrDisc) ((F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A).obj j)
Tactic:
apply Sheaf.cond
Proof state after:
no goals
Theorem: ExtrDisc.Sheaf.isSheafOfIsColimit
Proof state before:
A : Type (u + 2)
inst✝³ : Category A
inst✝² : HasZeroMorphisms A
inst✝¹ : HasFiniteBiproducts A
J : Type (u + 1)
inst✝ : SmallCategory J
F✝ : J ⥤ ExtrDiscᵒᵖ ⥤ A
F : J ⥤ Sheaf (coherentTopology ExtrDisc) A
S : Cocone (F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A)
hS : IsColimit S
⊢ Presheaf.IsSheaf (coherentTopology ExtrDisc) S.pt
Tactic:
have : HasColimit (F ⋙ sheafToPresheaf _ _) := ⟨S,hS⟩
Proof state after:
A : Type (u + 2)
inst✝³ : Category A
inst✝² : HasZeroMorphisms A
inst✝¹ : HasFiniteBiproducts A
J : Type (u + 1)
inst✝ : SmallCategory J
F✝ : J ⥤ ExtrDiscᵒᵖ ⥤ A
F : J ⥤ Sheaf (coherentTopology ExtrDisc) A
S : Cocone (F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A)
hS : IsColimit S
this : HasColimit (F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A)
⊢ Presheaf.IsSheaf (coherentTopology ExtrDisc) S.pt
Theorem: ExtrDisc.Sheaf.isSheafOfIsColimit
Proof state before:
A : Type (u + 2)
inst✝³ : Category A
inst✝² : HasZeroMorphisms A
inst✝¹ : HasFiniteBiproducts A
J : Type (u + 1)
inst✝ : SmallCategory J
F✝ : J ⥤ ExtrDiscᵒᵖ ⥤ A
F : J ⥤ Sheaf (coherentTopology ExtrDisc) A
S : Cocone (F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A)
hS : IsColimit S
this : HasColimit (F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A)
⊢ Presheaf.IsSheaf (coherentTopology ExtrDisc) S.pt
Tactic:
let e : S.pt ≅ colimit (F ⋙ sheafToPresheaf _ _) := 
  hS.coconePointUniqueUpToIso (colimit.isColimit _)
Proof state after:
A : Type (u + 2)
inst✝³ : Category A
inst✝² : HasZeroMorphisms A
inst✝¹ : HasFiniteBiproducts A
J : Type (u + 1)
inst✝ : SmallCategory J
F✝ : J ⥤ ExtrDiscᵒᵖ ⥤ A
F : J ⥤ Sheaf (coherentTopology ExtrDisc) A
S : Cocone (F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A)
hS : IsColimit S
this : HasColimit (F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A)
e : S.pt ≅ colimit (F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A) :=
  IsColimit.coconePointUniqueUpToIso hS (colimit.isColimit (F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A))
⊢ Presheaf.IsSheaf (coherentTopology ExtrDisc) S.pt