internlm/Lean-Github huggingface dataset:
Theorem: coherentTopology.Sieve_of_has_EffectiveEpiFamily
Proof 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 _ _ _
Proof 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
Theorem: coherentTopology.Sieve_of_has_EffectiveEpiFamily
Proof 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 _ π)
Proof 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
Theorem: coherentTopology.Sieve_of_has_EffectiveEpiFamily
Proof 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 (_)
Proof 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
Theorem: coherentTopology.Sieve_of_has_EffectiveEpiFamily
Proof 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 _ ?_
Proof 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
Theorem: coherentTopology.Sieve_of_has_EffectiveEpiFamily
Proof 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]
Proof 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
Theorem: coherentTopology.Sieve_of_has_EffectiveEpiFamily
Proof 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
Proof 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
Theorem: coherentTopology.Sieve_of_has_EffectiveEpiFamily
Proof 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
Proof 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
Theorem: coherentTopology.Sieve_of_has_EffectiveEpiFamily
Proof 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
Proof 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
Theorem: coherentTopology.Sieve_of_has_EffectiveEpiFamily
Proof 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⟩
Proof 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
Theorem: coherentTopology.Sieve_of_has_EffectiveEpiFamily
Proof 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)
Proof 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
Theorem: coherentTopology.Sieve_of_has_EffectiveEpiFamily
Proof 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
Proof 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
Theorem: coherentTopology.Sieve_of_has_EffectiveEpiFamily
Proof 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
Proof state after:
no goals
Theorem: coherentTopology.Sieve_of_has_EffectiveEpiFamily
Proof 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)
Proof state after:
no goals
Theorem: coherentTopology.Sieve_of_has_EffectiveEpiFamily
Proof 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
Proof 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
Theorem: coherentTopology.Sieve_of_has_EffectiveEpiFamily
Proof 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
Proof 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
Theorem: coherentTopology.Sieve_of_has_EffectiveEpiFamily
Proof 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, π
Proof 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 π
Theorem: coherentTopology.Sieve_of_has_EffectiveEpiFamily
Proof 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
Proof 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 π
Theorem: coherentTopology.Sieve_of_has_EffectiveEpiFamily
Proof 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
Proof state after:
no goals
Theorem: coherentTopology.Sieve_of_has_EffectiveEpiFamily
Proof 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
Proof state after:
no goals
Theorem: Sieve.yonedaFamily_fromCocone_compatible
Proof state before:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
s : Cocone (diagram S.arrows)
⊢ FamilyOfElements.Compatible (yonedaFamilyOfElements_fromCocone S s)
Tactic:
intro Y₁ Y₂ Z g₁ g₂ f₁ f₂ hf₁ hf₂ hgf
Proof state after:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
s : Cocone (diagram S.arrows)
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S.arrows f₁
hf₂ : S.arrows f₂
hgf : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ (yoneda.obj s.pt).map g₁.op (yonedaFamilyOfElements_fromCocone S s f₁ hf₁) =
    (yoneda.obj s.pt).map g₂.op (yonedaFamilyOfElements_fromCocone S s f₂ hf₂)
Theorem: Sieve.yonedaFamily_fromCocone_compatible
Proof state before:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
s : Cocone (diagram S.arrows)
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S.arrows f₁
hf₂ : S.arrows f₂
hgf : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ (yoneda.obj s.pt).map g₁.op (yonedaFamilyOfElements_fromCocone S s f₁ hf₁) =
    (yoneda.obj s.pt).map g₂.op (yonedaFamilyOfElements_fromCocone S s f₂ hf₂)
Tactic:
have := s.ι.naturality
Proof state after:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
s : Cocone (diagram S.arrows)
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S.arrows f₁
hf₂ : S.arrows f₂
hgf : g₁ ≫ f₁ = g₂ ≫ f₂
this :
  ∀ ⦃X_1 Y : FullSubcategory fun f => S.arrows f.hom⦄ (f : X_1 ⟶ Y),
    (diagram S.arrows).map f ≫ s.ι.app Y =
      s.ι.app X_1 ≫ ((Functor.const (FullSubcategory fun f => S.arrows f.hom)).obj s.pt).map f
⊢ (yoneda.obj s.pt).map g₁.op (yonedaFamilyOfElements_fromCocone S s f₁ hf₁) =
    (yoneda.obj s.pt).map g₂.op (yonedaFamilyOfElements_fromCocone S s f₂ hf₂)
Theorem: Sieve.yonedaFamily_fromCocone_compatible
Proof state before:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
s : Cocone (diagram S.arrows)
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S.arrows f₁
hf₂ : S.arrows f₂
hgf : g₁ ≫ f₁ = g₂ ≫ f₂
this :
  ∀ ⦃X_1 Y : FullSubcategory fun f => S.arrows f.hom⦄ (f : X_1 ⟶ Y),
    (diagram S.arrows).map f ≫ s.ι.app Y =
      s.ι.app X_1 ≫ ((Functor.const (FullSubcategory fun f => S.arrows f.hom)).obj s.pt).map f
⊢ (yoneda.obj s.pt).map g₁.op (yonedaFamilyOfElements_fromCocone S s f₁ hf₁) =
    (yoneda.obj s.pt).map g₂.op (yonedaFamilyOfElements_fromCocone S s f₂ hf₂)
Tactic:
simp
Proof state after:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
s : Cocone (diagram S.arrows)
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S.arrows f₁
hf₂ : S.arrows f₂
hgf : g₁ ≫ f₁ = g₂ ≫ f₂
this :
  ∀ ⦃X_1 Y : FullSubcategory fun f => S.arrows f.hom⦄ (f : X_1 ⟶ Y),
    (diagram S.arrows).map f ≫ s.ι.app Y =
      s.ι.app X_1 ≫ ((Functor.const (FullSubcategory fun f => S.arrows f.hom)).obj s.pt).map f
⊢ g₁ ≫ yonedaFamilyOfElements_fromCocone S s f₁ hf₁ = g₂ ≫ yonedaFamilyOfElements_fromCocone S s f₂ hf₂
Theorem: Sieve.yonedaFamily_fromCocone_compatible
Proof state before:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
s : Cocone (diagram S.arrows)
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S.arrows f₁
hf₂ : S.arrows f₂
hgf : g₁ ≫ f₁ = g₂ ≫ f₂
this :
  ∀ ⦃X_1 Y : FullSubcategory fun f => S.arrows f.hom⦄ (f : X_1 ⟶ Y),
    (diagram S.arrows).map f ≫ s.ι.app Y =
      s.ι.app X_1 ≫ ((Functor.const (FullSubcategory fun f => S.arrows f.hom)).obj s.pt).map f
⊢ g₁ ≫ yonedaFamilyOfElements_fromCocone S s f₁ hf₁ = g₂ ≫ yonedaFamilyOfElements_fromCocone S s f₂ hf₂
Tactic:
dsimp [yonedaFamilyOfElements_fromCocone]
Proof state after:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
s : Cocone (diagram S.arrows)
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S.arrows f₁
hf₂ : S.arrows f₂
hgf : g₁ ≫ f₁ = g₂ ≫ f₂
this :
  ∀ ⦃X_1 Y : FullSubcategory fun f => S.arrows f.hom⦄ (f : X_1 ⟶ Y),
    (diagram S.arrows).map f ≫ s.ι.app Y =
      s.ι.app X_1 ≫ ((Functor.const (FullSubcategory fun f => S.arrows f.hom)).obj s.pt).map f
⊢ g₁ ≫ s.ι.app { obj := Over.mk f₁, property := hf₁ } = g₂ ≫ s.ι.app { obj := Over.mk f₂, property := hf₂ }
Theorem: Sieve.yonedaFamily_fromCocone_compatible
Proof state before:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
s : Cocone (diagram S.arrows)
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S.arrows f₁
hf₂ : S.arrows f₂
hgf : g₁ ≫ f₁ = g₂ ≫ f₂
this :
  ∀ ⦃X_1 Y : FullSubcategory fun f => S.arrows f.hom⦄ (f : X_1 ⟶ Y),
    (diagram S.arrows).map f ≫ s.ι.app Y =
      s.ι.app X_1 ≫ ((Functor.const (FullSubcategory fun f => S.arrows f.hom)).obj s.pt).map f
⊢ g₁ ≫ s.ι.app { obj := Over.mk f₁, property := hf₁ } = g₂ ≫ s.ι.app { obj := Over.mk f₂, property := hf₂ }
Tactic:
have hgf₁ : S.arrows (g₁ ≫ f₁) := by exact Sieve.downward_closed S hf₁ g₁
Proof state after:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
s : Cocone (diagram S.arrows)
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S.arrows f₁
hf₂ : S.arrows f₂
hgf : g₁ ≫ f₁ = g₂ ≫ f₂
this :
  ∀ ⦃X_1 Y : FullSubcategory fun f => S.arrows f.hom⦄ (f : X_1 ⟶ Y),
    (diagram S.arrows).map f ≫ s.ι.app Y =
      s.ι.app X_1 ≫ ((Functor.const (FullSubcategory fun f => S.arrows f.hom)).obj s.pt).map f
hgf₁ : S.arrows (g₁ ≫ f₁)
⊢ g₁ ≫ s.ι.app { obj := Over.mk f₁, property := hf₁ } = g₂ ≫ s.ι.app { obj := Over.mk f₂, property := hf₂ }
Theorem: Sieve.yonedaFamily_fromCocone_compatible
Proof state before:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
s : Cocone (diagram S.arrows)
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S.arrows f₁
hf₂ : S.arrows f₂
hgf : g₁ ≫ f₁ = g₂ ≫ f₂
this :
  ∀ ⦃X_1 Y : FullSubcategory fun f => S.arrows f.hom⦄ (f : X_1 ⟶ Y),
    (diagram S.arrows).map f ≫ s.ι.app Y =
      s.ι.app X_1 ≫ ((Functor.const (FullSubcategory fun f => S.arrows f.hom)).obj s.pt).map f
hgf₁ : S.arrows (g₁ ≫ f₁)
⊢ g₁ ≫ s.ι.app { obj := Over.mk f₁, property := hf₁ } = g₂ ≫ s.ι.app { obj := Over.mk f₂, property := hf₂ }
Tactic:
have hgf₂ : S.arrows (g₂ ≫ f₂) := by exact Sieve.downward_closed S hf₂ g₂
Proof state after:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
s : Cocone (diagram S.arrows)
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S.arrows f₁
hf₂ : S.arrows f₂
hgf : g₁ ≫ f₁ = g₂ ≫ f₂
this :
  ∀ ⦃X_1 Y : FullSubcategory fun f => S.arrows f.hom⦄ (f : X_1 ⟶ Y),
    (diagram S.arrows).map f ≫ s.ι.app Y =
      s.ι.app X_1 ≫ ((Functor.const (FullSubcategory fun f => S.arrows f.hom)).obj s.pt).map f
hgf₁ : S.arrows (g₁ ≫ f₁)
hgf₂ : S.arrows (g₂ ≫ f₂)
⊢ g₁ ≫ s.ι.app { obj := Over.mk f₁, property := hf₁ } = g₂ ≫ s.ι.app { obj := Over.mk f₂, property := hf₂ }
Theorem: Sieve.yonedaFamily_fromCocone_compatible
Proof state before:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
s : Cocone (diagram S.arrows)
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S.arrows f₁
hf₂ : S.arrows f₂
hgf : g₁ ≫ f₁ = g₂ ≫ f₂
this :
  ∀ ⦃X_1 Y : FullSubcategory fun f => S.arrows f.hom⦄ (f : X_1 ⟶ Y),
    (diagram S.arrows).map f ≫ s.ι.app Y =
      s.ι.app X_1 ≫ ((Functor.const (FullSubcategory fun f => S.arrows f.hom)).obj s.pt).map f
hgf₁ : S.arrows (g₁ ≫ f₁)
hgf₂ : S.arrows (g₂ ≫ f₂)
⊢ g₁ ≫ s.ι.app { obj := Over.mk f₁, property := hf₁ } = g₂ ≫ s.ι.app { obj := Over.mk f₂, property := hf₂ }
Tactic:
let F : (Over.mk (g₁ ≫ f₁) : Over X) ⟶ (Over.mk (g₂ ≫ f₂) : Over X) := (Over.homMk (𝟙 Z) )
Proof state after:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
s : Cocone (diagram S.arrows)
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S.arrows f₁
hf₂ : S.arrows f₂
hgf : g₁ ≫ f₁ = g₂ ≫ f₂
this :
  ∀ ⦃X_1 Y : FullSubcategory fun f => S.arrows f.hom⦄ (f : X_1 ⟶ Y),
    (diagram S.arrows).map f ≫ s.ι.app Y =
      s.ι.app X_1 ≫ ((Functor.const (FullSubcategory fun f => S.arrows f.hom)).obj s.pt).map f
hgf₁ : S.arrows (g₁ ≫ f₁)
hgf₂ : S.arrows (g₂ ≫ f₂)
F : Over.mk (g₁ ≫ f₁) ⟶ Over.mk (g₂ ≫ f₂) := Over.homMk (𝟙 Z)
⊢ g₁ ≫ s.ι.app { obj := Over.mk f₁, property := hf₁ } = g₂ ≫ s.ι.app { obj := Over.mk f₂, property := hf₂ }
Theorem: Sieve.yonedaFamily_fromCocone_compatible
Proof state before:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
s : Cocone (diagram S.arrows)
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S.arrows f₁
hf₂ : S.arrows f₂
hgf : g₁ ≫ f₁ = g₂ ≫ f₂
this :
  ∀ ⦃X_1 Y : FullSubcategory fun f => S.arrows f.hom⦄ (f : X_1 ⟶ Y),
    (diagram S.arrows).map f ≫ s.ι.app Y =
      s.ι.app X_1 ≫ ((Functor.const (FullSubcategory fun f => S.arrows f.hom)).obj s.pt).map f
hgf₁ : S.arrows (g₁ ≫ f₁)
hgf₂ : S.arrows (g₂ ≫ f₂)
F : Over.mk (g₁ ≫ f₁) ⟶ Over.mk (g₂ ≫ f₂) := Over.homMk (𝟙 Z)
⊢ g₁ ≫ s.ι.app { obj := Over.mk f₁, property := hf₁ } = g₂ ≫ s.ι.app { obj := Over.mk f₂, property := hf₂ }
Tactic:
let F₁ : (Over.mk (g₁ ≫ f₁) : Over X) ⟶ (Over.mk f₁ : Over X) := (Over.homMk g₁)
Proof state after:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
s : Cocone (diagram S.arrows)
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S.arrows f₁
hf₂ : S.arrows f₂
hgf : g₁ ≫ f₁ = g₂ ≫ f₂
this :
  ∀ ⦃X_1 Y : FullSubcategory fun f => S.arrows f.hom⦄ (f : X_1 ⟶ Y),
    (diagram S.arrows).map f ≫ s.ι.app Y =
      s.ι.app X_1 ≫ ((Functor.const (FullSubcategory fun f => S.arrows f.hom)).obj s.pt).map f
hgf₁ : S.arrows (g₁ ≫ f₁)
hgf₂ : S.arrows (g₂ ≫ f₂)
F : Over.mk (g₁ ≫ f₁) ⟶ Over.mk (g₂ ≫ f₂) := Over.homMk (𝟙 Z)
F₁ : Over.mk (g₁ ≫ f₁) ⟶ Over.mk f₁ := Over.homMk g₁
⊢ g₁ ≫ s.ι.app { obj := Over.mk f₁, property := hf₁ } = g₂ ≫ s.ι.app { obj := Over.mk f₂, property := hf₂ }