Theorem: Condensed.isSheaf_iff_conditions (Condensed/SheafCondition.lean)

State before:
C : Type w
inst✝ : Category C
P : CompHausᵒᵖ ⥤ C
⊢ Presheaf.IsSheaf (coherentTopology CompHaus) P ↔ ProductCondition P ∧ EqualizerCondition P
Tactic:
constructor
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

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
State after:
case mp
C : Type w
inst✝ : Category C
P : CompHausᵒᵖ ⥤ C
H : Presheaf.IsSheaf (coherentTopology CompHaus) P
⊢ ProductCondition P ∧ EqualizerCondition P

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

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

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

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

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

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

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

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

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

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

State before:
case mp.right
C : Type w
inst✝ : Category C
P : CompHausᵒᵖ ⥤ C
H : Presheaf.IsSheaf (coherentTopology CompHaus) P
⊢ EqualizerCondition P
Tactic:
sorry
State after:
no goals

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⟩
State after:
case mpr
C : Type w
inst✝ : Category C
P : CompHausᵒᵖ ⥤ C
H1 : ProductCondition P
H2 : EqualizerCondition P
⊢ Presheaf.IsSheaf (coherentTopology CompHaus) P

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

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

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

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

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

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

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

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