internlm/Lean-Github huggingface dataset:
Theorem: CompHaus.extensiveRegular_generates_coherent
Proof state before:
case this.hS.h
X : CompHaus
S : Sieve X
Y : CompHaus
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → CompHaus
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : CompHaus := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : CompHaus
g : R ⟶ Y
W : CompHaus
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
this : Sieve.generate (ofArrows Xmap φ) ≤ Sieve.pullback F Z
⊢ IsIso (Sigma.desc φ)
Tactic:
suffices : Sigma.desc φ = 𝟙 _
Proof state after:
case this.hS.h
X : CompHaus
S : Sieve X
Y : CompHaus
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → CompHaus
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : CompHaus := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : CompHaus
g : R ⟶ Y
W : CompHaus
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
this✝ : Sieve.generate (ofArrows Xmap φ) ≤ Sieve.pullback F Z
this : Sigma.desc φ = 𝟙 (∐ fun b => Xmap b)
⊢ IsIso (Sigma.desc φ)

case this
X : CompHaus
S : Sieve X
Y : CompHaus
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → CompHaus
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : CompHaus := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : CompHaus
g : R ⟶ Y
W : CompHaus
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
this : Sieve.generate (ofArrows Xmap φ) ≤ Sieve.pullback F Z
⊢ Sigma.desc φ = 𝟙 (∐ fun b => Xmap b)
Theorem: CompHaus.extensiveRegular_generates_coherent
Proof state before:
case this
X : CompHaus
S : Sieve X
Y : CompHaus
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → CompHaus
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : CompHaus := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : CompHaus
g : R ⟶ Y
W : CompHaus
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
this : Sieve.generate (ofArrows Xmap φ) ≤ Sieve.pullback F Z
⊢ Sigma.desc φ = 𝟙 (∐ fun b => Xmap b)
Tactic:
ext
Proof state after:
case this.h.w
X : CompHaus
S : Sieve X
Y : CompHaus
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → CompHaus
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : CompHaus := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : CompHaus
g : R ⟶ Y
W : CompHaus
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
this : Sieve.generate (ofArrows Xmap φ) ≤ Sieve.pullback F Z
b✝ : I
x✝ : (forget CompHaus).obj (Xmap b✝)
⊢ ↑(Sigma.ι (fun b => Xmap b) b✝ ≫ Sigma.desc φ) x✝ = ↑(Sigma.ι (fun b => Xmap b) b✝ ≫ 𝟙 (∐ fun b => Xmap b)) x✝
Theorem: CompHaus.extensiveRegular_generates_coherent
Proof state before:
case this.h.w
X : CompHaus
S : Sieve X
Y : CompHaus
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → CompHaus
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : CompHaus := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : CompHaus
g : R ⟶ Y
W : CompHaus
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
this : Sieve.generate (ofArrows Xmap φ) ≤ Sieve.pullback F Z
b✝ : I
x✝ : (forget CompHaus).obj (Xmap b✝)
⊢ ↑(Sigma.ι (fun b => Xmap b) b✝ ≫ Sigma.desc φ) x✝ = ↑(Sigma.ι (fun b => Xmap b) b✝ ≫ 𝟙 (∐ fun b => Xmap b)) x✝
Tactic:
simp only [colimit.ι_desc, Cofan.mk_pt, Cofan.mk_ι_app, Category.comp_id]
Proof state after:
no goals
Theorem: CompHaus.extensiveRegular_generates_coherent
Proof state before:
case this.hS.h
X : CompHaus
S : Sieve X
Y : CompHaus
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → CompHaus
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : CompHaus := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : CompHaus
g : R ⟶ Y
W : CompHaus
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
this✝ : Sieve.generate (ofArrows Xmap φ) ≤ Sieve.pullback F Z
this : Sigma.desc φ = 𝟙 (∐ fun b => Xmap b)
⊢ IsIso (Sigma.desc φ)
Tactic:
rw [this]
Proof state after:
case this.hS.h
X : CompHaus
S : Sieve X
Y : CompHaus
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → CompHaus
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : CompHaus := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : CompHaus
g : R ⟶ Y
W : CompHaus
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
this✝ : Sieve.generate (ofArrows Xmap φ) ≤ Sieve.pullback F Z
this : Sigma.desc φ = 𝟙 (∐ fun b => Xmap b)
⊢ IsIso (𝟙 (∐ fun b => Xmap b))
Theorem: CompHaus.extensiveRegular_generates_coherent
Proof state before:
case this.hS.h
X : CompHaus
S : Sieve X
Y : CompHaus
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → CompHaus
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : CompHaus := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : CompHaus
g : R ⟶ Y
W : CompHaus
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
this✝ : Sieve.generate (ofArrows Xmap φ) ≤ Sieve.pullback F Z
this : Sigma.desc φ = 𝟙 (∐ fun b => Xmap b)
⊢ IsIso (𝟙 (∐ fun b => Xmap b))
Tactic:
exact inferInstance
Proof state after:
no goals
Theorem: CompHaus.extensiveRegular_generates_coherent
Proof state before:
case this.intro.intro.intro.refine'_1
X : CompHaus
S : Sieve X
Y : CompHaus
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → CompHaus
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : CompHaus := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : CompHaus
g : R ⟶ Y
W : CompHaus
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
Q : CompHaus
q : Q ⟶ ∐ Xmap
E : CompHaus
e : Q ⟶ E
r : E ⟶ ∐ Xmap
hq : ofArrows Xmap (fun i => Sigma.ι Xmap i) r ∧ e ≫ r = q
⊢ T (r ≫ F)
Tactic:
rw [h]
Proof state after:
case this.intro.intro.intro.refine'_1
X : CompHaus
S : Sieve X
Y : CompHaus
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → CompHaus
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : CompHaus := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : CompHaus
g : R ⟶ Y
W : CompHaus
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
Q : CompHaus
q : Q ⟶ ∐ Xmap
E : CompHaus
e : Q ⟶ E
r : E ⟶ ∐ Xmap
hq : ofArrows Xmap (fun i => Sigma.ι Xmap i) r ∧ e ≫ r = q
⊢ ofArrows Xmap f (r ≫ F)
Theorem: CompHaus.extensiveRegular_generates_coherent
Proof state before:
case this.intro.intro.intro.refine'_1
X : CompHaus
S : Sieve X
Y : CompHaus
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → CompHaus
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : CompHaus := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : CompHaus
g : R ⟶ Y
W : CompHaus
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
Q : CompHaus
q : Q ⟶ ∐ Xmap
E : CompHaus
e : Q ⟶ E
r : E ⟶ ∐ Xmap
hq : ofArrows Xmap (fun i => Sigma.ι Xmap i) r ∧ e ≫ r = q
⊢ ofArrows Xmap f (r ≫ F)
Tactic:
induction hq.1
Proof state after:
case this.intro.intro.intro.refine'_1.mk
X : CompHaus
S : Sieve X
Y : CompHaus
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → CompHaus
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : CompHaus := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : CompHaus
g : R ⟶ Y
W : CompHaus
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
Q : CompHaus
q : Q ⟶ ∐ Xmap
E : CompHaus
r : E ⟶ ∐ Xmap
i✝ : I
e : Q ⟶ Xmap i✝
hq : ofArrows Xmap (fun i => Sigma.ι Xmap i) (Sigma.ι Xmap i✝) ∧ e ≫ Sigma.ι Xmap i✝ = q
⊢ ofArrows Xmap f (Sigma.ι Xmap i✝ ≫ F)
Theorem: CompHaus.extensiveRegular_generates_coherent
Proof state before:
case this.intro.intro.intro.refine'_1.mk
X : CompHaus
S : Sieve X
Y : CompHaus
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → CompHaus
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : CompHaus := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : CompHaus
g : R ⟶ Y
W : CompHaus
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
Q : CompHaus
q : Q ⟶ ∐ Xmap
E : CompHaus
r : E ⟶ ∐ Xmap
i✝ : I
e : Q ⟶ Xmap i✝
hq : ofArrows Xmap (fun i => Sigma.ι Xmap i) (Sigma.ι Xmap i✝) ∧ e ≫ Sigma.ι Xmap i✝ = q
⊢ ofArrows Xmap f (Sigma.ι Xmap i✝ ≫ F)
Tactic:
dsimp
Proof state after:
case this.intro.intro.intro.refine'_1.mk
X : CompHaus
S : Sieve X
Y : CompHaus
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → CompHaus
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : CompHaus := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : CompHaus
g : R ⟶ Y
W : CompHaus
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
Q : CompHaus
q : Q ⟶ ∐ Xmap
E : CompHaus
r : E ⟶ ∐ Xmap
i✝ : I
e : Q ⟶ Xmap i✝
hq : ofArrows Xmap (fun i => Sigma.ι Xmap i) (Sigma.ι Xmap i✝) ∧ e ≫ Sigma.ι Xmap i✝ = q
⊢ ofArrows Xmap f (Sigma.ι Xmap i✝ ≫ Sigma.desc f)
Theorem: CompHaus.extensiveRegular_generates_coherent
Proof state before:
case this.intro.intro.intro.refine'_1.mk
X : CompHaus
S : Sieve X
Y : CompHaus
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → CompHaus
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : CompHaus := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : CompHaus
g : R ⟶ Y
W : CompHaus
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
Q : CompHaus
q : Q ⟶ ∐ Xmap
E : CompHaus
r : E ⟶ ∐ Xmap
i✝ : I
e : Q ⟶ Xmap i✝
hq : ofArrows Xmap (fun i => Sigma.ι Xmap i) (Sigma.ι Xmap i✝) ∧ e ≫ Sigma.ι Xmap i✝ = q
⊢ ofArrows Xmap f (Sigma.ι Xmap i✝ ≫ Sigma.desc f)
Tactic:
simp only [colimit.ι_desc, Cofan.mk_pt, Cofan.mk_ι_app]
Proof state after:
case this.intro.intro.intro.refine'_1.mk
X : CompHaus
S : Sieve X
Y : CompHaus
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → CompHaus
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : CompHaus := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : CompHaus
g : R ⟶ Y
W : CompHaus
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
Q : CompHaus
q : Q ⟶ ∐ Xmap
E : CompHaus
r : E ⟶ ∐ Xmap
i✝ : I
e : Q ⟶ Xmap i✝
hq : ofArrows Xmap (fun i => Sigma.ι Xmap i) (Sigma.ι Xmap i✝) ∧ e ≫ Sigma.ι Xmap i✝ = q
⊢ ofArrows Xmap f (f i✝)
Theorem: CompHaus.extensiveRegular_generates_coherent
Proof state before:
case this.intro.intro.intro.refine'_1.mk
X : CompHaus
S : Sieve X
Y : CompHaus
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → CompHaus
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : CompHaus := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : CompHaus
g : R ⟶ Y
W : CompHaus
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
Q : CompHaus
q : Q ⟶ ∐ Xmap
E : CompHaus
r : E ⟶ ∐ Xmap
i✝ : I
e : Q ⟶ Xmap i✝
hq : ofArrows Xmap (fun i => Sigma.ι Xmap i) (Sigma.ι Xmap i✝) ∧ e ≫ Sigma.ι Xmap i✝ = q
⊢ ofArrows Xmap f (f i✝)
Tactic:
exact Presieve.ofArrows.mk _
Proof state after:
no goals
Theorem: CompHaus.extensiveRegular_generates_coherent
Proof state before:
case this.intro.intro.intro.refine'_2
X : CompHaus
S : Sieve X
Y : CompHaus
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → CompHaus
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : CompHaus := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : CompHaus
g : R ⟶ Y
W : CompHaus
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
Q : CompHaus
q : Q ⟶ ∐ Xmap
E : CompHaus
e : Q ⟶ E
r : E ⟶ ∐ Xmap
hq : ofArrows Xmap (fun i => Sigma.ι Xmap i) r ∧ e ≫ r = q
⊢ e ≫ r ≫ F = q ≫ Sigma.desc f
Tactic:
rw [← hq.2]
Proof state after:
case this.intro.intro.intro.refine'_2
X : CompHaus
S : Sieve X
Y : CompHaus
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → CompHaus
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : CompHaus := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : CompHaus
g : R ⟶ Y
W : CompHaus
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
Q : CompHaus
q : Q ⟶ ∐ Xmap
E : CompHaus
e : Q ⟶ E
r : E ⟶ ∐ Xmap
hq : ofArrows Xmap (fun i => Sigma.ι Xmap i) r ∧ e ≫ r = q
⊢ e ≫ r ≫ F = (e ≫ r) ≫ Sigma.desc f
Theorem: CompHaus.extensiveRegular_generates_coherent
Proof state before:
case this.intro.intro.intro.refine'_2
X : CompHaus
S : Sieve X
Y : CompHaus
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → CompHaus
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : CompHaus := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : CompHaus
g : R ⟶ Y
W : CompHaus
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
Q : CompHaus
q : Q ⟶ ∐ Xmap
E : CompHaus
e : Q ⟶ E
r : E ⟶ ∐ Xmap
hq : ofArrows Xmap (fun i => Sigma.ι Xmap i) r ∧ e ≫ r = q
⊢ e ≫ r ≫ F = (e ≫ r) ≫ Sigma.desc f
Tactic:
rfl
Proof state after:
no goals
Theorem: CompHaus.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mpr.top
X : CompHaus
S : Sieve X
X✝ : CompHaus
⊢ ⊤ ∈
    GrothendieckTopology.sieves
      (Coverage.toGrothendieck CompHaus
        (ExtensiveRegularCoverage' CompHaus
          (_ : ∀ {X Y Z : CompHaus} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
          (_ :
            ∀ {α : Type} [inst : Fintype α] {X : CompHaus} {Z : α → CompHaus} (π : (a : α) → Z a ⟶ X) {Y : CompHaus}
              (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst))))
      X✝
Tactic:
apply Coverage.saturate.top
Proof state after:
no goals
Theorem: CompHaus.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mpr.transitive.a
X : CompHaus
S : Sieve X
Y : CompHaus
T S✝ : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage CompHaus) Y T
a✝ :
  ∀ ⦃Y_1 : CompHaus⦄ ⦃f : Y_1 ⟶ Y⦄, T.arrows f → Coverage.saturate (coherentCoverage CompHaus) Y_1 (Sieve.pullback f S✝)
a_ih✝¹ :
  T ∈
    GrothendieckTopology.sieves
      (Coverage.toGrothendieck CompHaus
        (ExtensiveRegularCoverage' CompHaus
          (_ : ∀ {X Y Z : CompHaus} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
          (_ :
            ∀ {α : Type} [inst : Fintype α] {X : CompHaus} {Z : α → CompHaus} (π : (a : α) → Z a ⟶ X) {Y : CompHaus}
              (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst))))
      Y
a_ih✝ :
  ∀ ⦃Y_1 : CompHaus⦄ ⦃f : Y_1 ⟶ Y⦄,
    T.arrows f →
      Sieve.pullback f S✝ ∈
        GrothendieckTopology.sieves
          (Coverage.toGrothendieck CompHaus
            (ExtensiveRegularCoverage' CompHaus
              (_ : ∀ {X Y Z : CompHaus} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
              (_ :
                ∀ {α : Type} [inst : Fintype α] {X : CompHaus} {Z : α → CompHaus} (π : (a : α) → Z a ⟶ X) {Y : CompHaus}
                  (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst))))
          Y_1
⊢ Coverage.saturate
    (ExtensiveRegularCoverage' CompHaus
      (_ : ∀ {X Y Z : CompHaus} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
      (_ :
        ∀ {α : Type} [inst : Fintype α] {X : CompHaus} {Z : α → CompHaus} (π : (a : α) → Z a ⟶ X) {Y : CompHaus}
          (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
    Y T
Tactic:
assumption
Proof state after:
no goals
Theorem: CompHaus.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mpr.transitive.a
X : CompHaus
S : Sieve X
Y : CompHaus
T S✝ : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage CompHaus) Y T
a✝ :
  ∀ ⦃Y_1 : CompHaus⦄ ⦃f : Y_1 ⟶ Y⦄, T.arrows f → Coverage.saturate (coherentCoverage CompHaus) Y_1 (Sieve.pullback f S✝)
a_ih✝¹ :
  T ∈
    GrothendieckTopology.sieves
      (Coverage.toGrothendieck CompHaus
        (ExtensiveRegularCoverage' CompHaus
          (_ : ∀ {X Y Z : CompHaus} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
          (_ :
            ∀ {α : Type} [inst : Fintype α] {X : CompHaus} {Z : α → CompHaus} (π : (a : α) → Z a ⟶ X) {Y : CompHaus}
              (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst))))
      Y
a_ih✝ :
  ∀ ⦃Y_1 : CompHaus⦄ ⦃f : Y_1 ⟶ Y⦄,
    T.arrows f →
      Sieve.pullback f S✝ ∈
        GrothendieckTopology.sieves
          (Coverage.toGrothendieck CompHaus
            (ExtensiveRegularCoverage' CompHaus
              (_ : ∀ {X Y Z : CompHaus} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
              (_ :
                ∀ {α : Type} [inst : Fintype α] {X : CompHaus} {Z : α → CompHaus} (π : (a : α) → Z a ⟶ X) {Y : CompHaus}
                  (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst))))
          Y_1
⊢ ∀ ⦃Y_1 : CompHaus⦄ ⦃f : Y_1 ⟶ Y⦄,
    T.arrows f →
      Coverage.saturate
        (ExtensiveRegularCoverage' CompHaus
          (_ : ∀ {X Y Z : CompHaus} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
          (_ :
            ∀ {α : Type} [inst : Fintype α] {X : CompHaus} {Z : α → CompHaus} (π : (a : α) → Z a ⟶ X) {Y : CompHaus}
              (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
        Y_1 (Sieve.pullback f S✝)
Tactic:
assumption
Proof state after:
no goals
Theorem: CompHaus.isSheafFor_of_Dagur
Proof state before:
B : CompHaus
S : Presieve B
hS :
  S ∈
    Coverage.covering
      (ExtensiveRegularCoverage' CompHaus
        (_ : ∀ {X Y Z : CompHaus} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
        (_ :
          ∀ {α : Type} [inst : Fintype α] {X : CompHaus} {Z : α → CompHaus} (π : (a : α) → Z a ⟶ X) {Y : CompHaus}
            (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
      B
F : CompHausᵒᵖ ⥤ Type (u + 1)
hFpfp : PreservesFiniteProducts F
hFecs : EqualizerCondition F
⊢ IsSheafFor F S
Tactic:
cases' hS with hSIso hSSingle
Proof state after:
case inl
B : CompHaus
S : Presieve B
F : CompHausᵒᵖ ⥤ Type (u + 1)
hFpfp : PreservesFiniteProducts F
hFecs : EqualizerCondition F
hSIso : S ∈ ExtensiveSieve B
⊢ IsSheafFor F S

case inr
B : CompHaus
S : Presieve B
F : CompHausᵒᵖ ⥤ Type (u + 1)
hFpfp : PreservesFiniteProducts F
hFecs : EqualizerCondition F
hSSingle : S ∈ RegularSieve B
⊢ IsSheafFor F S
Theorem: CompHaus.isSheafFor_of_Dagur
Proof state before:
case inl
B : CompHaus
S : Presieve B
F : CompHausᵒᵖ ⥤ Type (u + 1)
hFpfp : PreservesFiniteProducts F
hFecs : EqualizerCondition F
hSIso : S ∈ ExtensiveSieve B
⊢ IsSheafFor F S
Tactic:
exact isSheafForExtensiveSieve hSIso hFpfp
Proof state after:
no goals
Theorem: CompHaus.isSheafFor_of_Dagur
Proof state before:
case inr
B : CompHaus
S : Presieve B
F : CompHausᵒᵖ ⥤ Type (u + 1)
hFpfp : PreservesFiniteProducts F
hFecs : EqualizerCondition F
hSSingle : S ∈ RegularSieve B
⊢ IsSheafFor F S
Tactic:
rw [Equalizer.Presieve.sheaf_condition, Limits.Types.type_equalizer_iff_unique]
Proof state after:
case inr
B : CompHaus
S : Presieve B
F : CompHausᵒᵖ ⥤ Type (u + 1)
hFpfp : PreservesFiniteProducts F
hFecs : EqualizerCondition F
hSSingle : S ∈ RegularSieve B
⊢ ∀ (y : Equalizer.FirstObj F S),
    Equalizer.Presieve.firstMap F S y = Equalizer.Presieve.secondMap F S y → ∃! x, Equalizer.forkMap F S x = y
Theorem: CompHaus.isSheafFor_of_Dagur
Proof state before:
case inr
B : CompHaus
S : Presieve B
F : CompHausᵒᵖ ⥤ Type (u + 1)
hFpfp : PreservesFiniteProducts F
hFecs : EqualizerCondition F
hSSingle : S ∈ RegularSieve B
⊢ ∀ (y : Equalizer.FirstObj F S),
    Equalizer.Presieve.firstMap F S y = Equalizer.Presieve.secondMap F S y → ∃! x, Equalizer.forkMap F S x = y
Tactic:
intro y h
Proof state after:
case inr
B : CompHaus
S : Presieve B
F : CompHausᵒᵖ ⥤ Type (u + 1)
hFpfp : PreservesFiniteProducts F
hFecs : EqualizerCondition F
hSSingle : S ∈ RegularSieve B
y : Equalizer.FirstObj F S
h : Equalizer.Presieve.firstMap F S y = Equalizer.Presieve.secondMap F S y
⊢ ∃! x, Equalizer.forkMap F S x = y