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

State before:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
⊢ (∃ α x Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)) →
    S ∈ GrothendieckTopology.sieves (coherentTopology C) X
Tactic:
rintro ⟨α, ⟨h, ⟨Y, ⟨π, hπ⟩⟩⟩⟩
State after:
case intro.intro.intro.intro
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
h : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
⊢ S ∈ GrothendieckTopology.sieves (coherentTopology C) X

State before:
case intro.intro.intro.intro
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
h : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
⊢ S ∈ GrothendieckTopology.sieves (coherentTopology C) X
Tactic:
change Coverage.saturate _ _ _
State after:
case intro.intro.intro.intro
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
h : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
⊢ Coverage.saturate (coherentCoverage C) X S

State before:
case intro.intro.intro.intro
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
h : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
⊢ Coverage.saturate (coherentCoverage C) X S
Tactic:
let T := Sieve.generate (Presieve.ofArrows _ π)
State after:
case intro.intro.intro.intro
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
h : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
T : Sieve X := Sieve.generate (ofArrows (fun i => Y i) π)
⊢ Coverage.saturate (coherentCoverage C) X S

State before:
case intro.intro.intro.intro
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
h : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
T : Sieve X := Sieve.generate (ofArrows (fun i => Y i) π)
h_le : T ≤ S
⊢ Coverage.saturate (coherentCoverage C) X S
Tactic:
apply Coverage.saturate_of_superset (coherentCoverage C) h_le (_)
State after:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
h : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
T : Sieve X := Sieve.generate (ofArrows (fun i => Y i) π)
h_le : T ≤ S
⊢ Coverage.saturate (coherentCoverage C) X T

State before:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
h : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
T : Sieve X := Sieve.generate (ofArrows (fun i => Y i) π)
h_le : T ≤ S
⊢ Coverage.saturate (coherentCoverage C) X T
Tactic:
refine Coverage.saturate.of X _ ?_
State after:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
h : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
T : Sieve X := Sieve.generate (ofArrows (fun i => Y i) π)
h_le : T ≤ S
⊢ ofArrows (fun i => Y i) π ∈ Coverage.covering (coherentCoverage C) X

State before:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
h : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
T : Sieve X := Sieve.generate (ofArrows (fun i => Y i) π)
⊢ T ≤ S
Tactic:
rw [Sieve.sets_iff_generate (Presieve.ofArrows _ π) S]
State after:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
h : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
T : Sieve X := Sieve.generate (ofArrows (fun i => Y i) π)
⊢ ofArrows (fun i => Y i) π ≤ S.arrows

State before:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
h : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
T : Sieve X := Sieve.generate (ofArrows (fun i => Y i) π)
⊢ ofArrows (fun i => Y i) π ≤ S.arrows
Tactic:
refine Presieve.le_of_factorsThru_sieve (Presieve.ofArrows (fun i => Y i) π) S ?h
State after:
case h
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
h : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
T : Sieve X := Sieve.generate (ofArrows (fun i => Y i) π)
⊢ FactorsThru (ofArrows (fun i => Y i) π) S.arrows

State before:
case h
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
h : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
T : Sieve X := Sieve.generate (ofArrows (fun i => Y i) π)
⊢ FactorsThru (ofArrows (fun i => Y i) π) S.arrows
Tactic:
intro Y g f
State after:
case h
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
h : Fintype α
Y✝ : α → C
π : (a : α) → Y✝ a ⟶ X
hπ : EffectiveEpiFamily Y✝ π ∧ ∀ (a : α), S.arrows (π a)
T : Sieve X := Sieve.generate (ofArrows (fun i => Y✝ i) π)
Y : C
g : Y ⟶ X
f : ofArrows (fun i => Y✝ i) π g
⊢ ∃ W i e, S.arrows e ∧ i ≫ e = g

State before:
case h
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
h : Fintype α
Y✝ : α → C
π : (a : α) → Y✝ a ⟶ X
hπ : EffectiveEpiFamily Y✝ π ∧ ∀ (a : α), S.arrows (π a)
T : Sieve X := Sieve.generate (ofArrows (fun i => Y✝ i) π)
Y : C
g : Y ⟶ X
f : ofArrows (fun i => Y✝ i) π g
⊢ ∃ W i e, S.arrows e ∧ i ≫ e = g
Tactic:
use Y, 𝟙 Y
State after:
case h
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
h : Fintype α
Y✝ : α → C
π : (a : α) → Y✝ a ⟶ X
hπ : EffectiveEpiFamily Y✝ π ∧ ∀ (a : α), S.arrows (π a)
T : Sieve X := Sieve.generate (ofArrows (fun i => Y✝ i) π)
Y : C
g : Y ⟶ X
f : ofArrows (fun i => Y✝ i) π g
⊢ ∃ e, S.arrows e ∧ 𝟙 Y ≫ e = g

State before:
case h
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
h : Fintype α
Y✝ : α → C
π : (a : α) → Y✝ a ⟶ X
hπ : EffectiveEpiFamily Y✝ π ∧ ∀ (a : α), S.arrows (π a)
T : Sieve X := Sieve.generate (ofArrows (fun i => Y✝ i) π)
Y : C
g : Y ⟶ X
f : ofArrows (fun i => Y✝ i) π g
⊢ ∃ e, S.arrows e ∧ 𝟙 Y ≫ e = g
Tactic:
rcases f with ⟨i⟩
State after:
case h.mk
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
h : Fintype α
Y✝ : α → C
π : (a : α) → Y✝ a ⟶ X
hπ : EffectiveEpiFamily Y✝ π ∧ ∀ (a : α), S.arrows (π a)
T : Sieve X := Sieve.generate (ofArrows (fun i => Y✝ i) π)
Y : C
i : α
⊢ ∃ e, S.arrows e ∧ 𝟙 (Y✝ i) ≫ e = π i

State before:
case h.mk
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
h : Fintype α
Y✝ : α → C
π : (a : α) → Y✝ a ⟶ X
hπ : EffectiveEpiFamily Y✝ π ∧ ∀ (a : α), S.arrows (π a)
T : Sieve X := Sieve.generate (ofArrows (fun i => Y✝ i) π)
Y : C
i : α
⊢ ∃ e, S.arrows e ∧ 𝟙 (Y✝ i) ≫ e = π i
Tactic:
use (π i)
State after:
case h.mk
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
h : Fintype α
Y✝ : α → C
π : (a : α) → Y✝ a ⟶ X
hπ : EffectiveEpiFamily Y✝ π ∧ ∀ (a : α), S.arrows (π a)
T : Sieve X := Sieve.generate (ofArrows (fun i => Y✝ i) π)
Y : C
i : α
⊢ S.arrows (π i) ∧ 𝟙 (Y✝ i) ≫ π i = π i

State before:
case h.mk
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
h : Fintype α
Y✝ : α → C
π : (a : α) → Y✝ a ⟶ X
hπ : EffectiveEpiFamily Y✝ π ∧ ∀ (a : α), S.arrows (π a)
T : Sieve X := Sieve.generate (ofArrows (fun i => Y✝ i) π)
Y : C
i : α
⊢ S.arrows (π i) ∧ 𝟙 (Y✝ i) ≫ π i = π i
Tactic:
constructor
State after:
case h.mk.left
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
h : Fintype α
Y✝ : α → C
π : (a : α) → Y✝ a ⟶ X
hπ : EffectiveEpiFamily Y✝ π ∧ ∀ (a : α), S.arrows (π a)
T : Sieve X := Sieve.generate (ofArrows (fun i => Y✝ i) π)
Y : C
i : α
⊢ S.arrows (π i)

case h.mk.right
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
h : Fintype α
Y✝ : α → C
π : (a : α) → Y✝ a ⟶ X
hπ : EffectiveEpiFamily Y✝ π ∧ ∀ (a : α), S.arrows (π a)
T : Sieve X := Sieve.generate (ofArrows (fun i => Y✝ i) π)
Y : C
i : α
⊢ 𝟙 (Y✝ i) ≫ π i = π i

State before:
case h.mk.left
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
h : Fintype α
Y✝ : α → C
π : (a : α) → Y✝ a ⟶ X
hπ : EffectiveEpiFamily Y✝ π ∧ ∀ (a : α), S.arrows (π a)
T : Sieve X := Sieve.generate (ofArrows (fun i => Y✝ i) π)
Y : C
i : α
⊢ S.arrows (π i)
Tactic:
exact hπ.2 i
State after:
no goals

State before:
case h.mk.right
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
h : Fintype α
Y✝ : α → C
π : (a : α) → Y✝ a ⟶ X
hπ : EffectiveEpiFamily Y✝ π ∧ ∀ (a : α), S.arrows (π a)
T : Sieve X := Sieve.generate (ofArrows (fun i => Y✝ i) π)
Y : C
i : α
⊢ 𝟙 (Y✝ i) ≫ π i = π i
Tactic:
exact Category.id_comp (π i)
State after:
no goals

State before:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
h : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
T : Sieve X := Sieve.generate (ofArrows (fun i => Y i) π)
h_le : T ≤ S
⊢ ofArrows (fun i => Y i) π ∈ Coverage.covering (coherentCoverage C) X
Tactic:
unfold coherentCoverage
State after:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
h : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
T : Sieve X := Sieve.generate (ofArrows (fun i => Y i) π)
h_le : T ≤ S
⊢ ofArrows (fun i => Y i) π ∈
    Coverage.covering
      { covering := fun B => {S | ∃ α x X π, S = ofArrows X π ∧ EffectiveEpiFamily X π},
        pullback :=
          (_ :
            ∀ ⦃B₁ B₂ : C⦄ (f : B₂ ⟶ B₁) (S : Presieve B₁),
              S ∈ (fun B => {S | ∃ α x X π, S = ofArrows X π ∧ EffectiveEpiFamily X π}) B₁ →
                ∃ T,
                  T ∈ (fun B => {S | ∃ α x X π, S = ofArrows X π ∧ EffectiveEpiFamily X π}) B₂ ∧
                    FactorsThruAlong T S f) }
      X

State before:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
h : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
T : Sieve X := Sieve.generate (ofArrows (fun i => Y i) π)
h_le : T ≤ S
⊢ ofArrows (fun i => Y i) π ∈
    Coverage.covering
      { covering := fun B => {S | ∃ α x X π, S = ofArrows X π ∧ EffectiveEpiFamily X π},
        pullback :=
          (_ :
            ∀ ⦃B₁ B₂ : C⦄ (f : B₂ ⟶ B₁) (S : Presieve B₁),
              S ∈ (fun B => {S | ∃ α x X π, S = ofArrows X π ∧ EffectiveEpiFamily X π}) B₁ →
                ∃ T,
                  T ∈ (fun B => {S | ∃ α x X π, S = ofArrows X π ∧ EffectiveEpiFamily X π}) B₂ ∧
                    FactorsThruAlong T S f) }
      X
Tactic:
simp
State after:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
h : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
T : Sieve X := Sieve.generate (ofArrows (fun i => Y i) π)
h_le : T ≤ S
⊢ ∃ α_1 x X_1 π_1, ofArrows (fun i => Y i) π = ofArrows X_1 π_1 ∧ EffectiveEpiFamily X_1 π_1

State before:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
h : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
T : Sieve X := Sieve.generate (ofArrows (fun i => Y i) π)
h_le : T ≤ S
⊢ ∃ α_1 x X_1 π_1, ofArrows (fun i => Y i) π = ofArrows X_1 π_1 ∧ EffectiveEpiFamily X_1 π_1
Tactic:
use α, inferInstance, Y, π
State after:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
h : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
T : Sieve X := Sieve.generate (ofArrows (fun i => Y i) π)
h_le : T ≤ S
⊢ ofArrows (fun i => Y i) π = ofArrows Y π ∧ EffectiveEpiFamily Y π

State before:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
h : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
T : Sieve X := Sieve.generate (ofArrows (fun i => Y i) π)
h_le : T ≤ S
⊢ ofArrows (fun i => Y i) π = ofArrows Y π ∧ EffectiveEpiFamily Y π
Tactic:
constructor
State after:
case left
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
h : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
T : Sieve X := Sieve.generate (ofArrows (fun i => Y i) π)
h_le : T ≤ S
⊢ ofArrows (fun i => Y i) π = ofArrows Y π

case right
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
h : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
T : Sieve X := Sieve.generate (ofArrows (fun i => Y i) π)
h_le : T ≤ S
⊢ EffectiveEpiFamily Y π

State before:
case left
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
h : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
T : Sieve X := Sieve.generate (ofArrows (fun i => Y i) π)
h_le : T ≤ S
⊢ ofArrows (fun i => Y i) π = ofArrows Y π
Tactic:
rfl
State after:
no goals

State before:
case right
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
h : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
T : Sieve X := Sieve.generate (ofArrows (fun i => Y i) π)
h_le : T ≤ S
⊢ EffectiveEpiFamily Y π
Tactic:
exact hπ.1
State after:
no goals