internlm/Lean-Github huggingface dataset:
Theorem: coherentTopology.isSheaf_Yoneda
Proof state before:
case intro.intro.right
C : Type u
inst✝² : Category C
inst✝¹ : Precoherent C
X✝ W X : C
α : Type
inst✝ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : IsColimit (cocone (Sieve.generate (ofArrows Y π)).arrows)
x : FamilyOfElements (yoneda.obj W) (ofArrows Y π)
hx : FamilyOfElements.Compatible x
x_ext : FamilyOfElements (yoneda.obj W) (Sieve.generate (ofArrows Y π)).arrows := FamilyOfElements.sieveExtend x
hx_ext : FamilyOfElements.Compatible (FamilyOfElements.sieveExtend x)
S : Sieve X := Sieve.generate (ofArrows Y π)
t : (yoneda.obj W).obj X.op
t_amalg : FamilyOfElements.IsAmalgamation x_ext t
t_uniq : ∀ (y : (yoneda.obj W).obj X.op), (fun t => FamilyOfElements.IsAmalgamation x_ext t) y → y = t
⊢ ∀ (y : (yoneda.obj W).obj X.op), (fun t => FamilyOfElements.IsAmalgamation x t) y → y = t
Tactic:
exact fun y hy => t_uniq y <| isAmalgamation_sieveExtend x y hy
Proof state after:
no goals
Theorem: EffectiveEpiFamily_transitive
Proof state before:
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
⊢ EffectiveEpiFamily (fun c => Y_n c.fst c.snd) fun c => π_n c.fst c.snd ≫ π c.fst
Tactic:
rw [← Sieve.effectiveEpimorphic_family]
Proof state after:
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
⊢ EffectiveEpimorphic (ofArrows (fun c => Y_n c.fst c.snd) fun c => π_n c.fst c.snd ≫ π c.fst)
Theorem: EffectiveEpiFamily_transitive
Proof state before:
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
⊢ EffectiveEpimorphic (ofArrows (fun c => Y_n c.fst c.snd) fun c => π_n c.fst c.snd ≫ π c.fst)
Tactic:
suffices h₂ : (Sieve.generate (Presieve.ofArrows (fun (⟨a, b⟩ : Σ _, β _) => Y_n a b)
      (fun ⟨a,b⟩ => π_n a b ≫ π a))) ∈ GrothendieckTopology.sieves (coherentTopology C) X by
  change Nonempty _
  rw [← Sieve.Yoneda_sheaf_iff_colimit]
  intro W
  apply coherentTopology.isSheaf_Yoneda
  exact h₂
Proof state after:
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
⊢ Sieve.generate
      (ofArrows
        (fun x =>
          match x with
          | { fst := a, snd := b } => Y_n a b)
        fun x =>
        match x with
        | { fst := a, snd := b } => π_n a b ≫ π a) ∈
    GrothendieckTopology.sieves (coherentTopology C) X
Theorem: EffectiveEpiFamily_transitive
Proof state before:
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
⊢ Sieve.generate
      (ofArrows
        (fun x =>
          match x with
          | { fst := a, snd := b } => Y_n a b)
        fun x =>
        match x with
        | { fst := a, snd := b } => π_n a b ≫ π a) ∈
    GrothendieckTopology.sieves (coherentTopology C) X
Tactic:
let h' := h
Proof state after:
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpiFamily Y π := h
⊢ Sieve.generate
      (ofArrows
        (fun x =>
          match x with
          | { fst := a, snd := b } => Y_n a b)
        fun x =>
        match x with
        | { fst := a, snd := b } => π_n a b ≫ π a) ∈
    GrothendieckTopology.sieves (coherentTopology C) X
Theorem: EffectiveEpiFamily_transitive
Proof state before:
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpiFamily Y π := h
⊢ Sieve.generate
      (ofArrows
        (fun x =>
          match x with
          | { fst := a, snd := b } => Y_n a b)
        fun x =>
        match x with
        | { fst := a, snd := b } => π_n a b ≫ π a) ∈
    GrothendieckTopology.sieves (coherentTopology C) X
Tactic:
rw [← Sieve.effectiveEpimorphic_family] at h'
Proof state after:
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpimorphic (ofArrows Y π)
⊢ Sieve.generate
      (ofArrows
        (fun x =>
          match x with
          | { fst := a, snd := b } => Y_n a b)
        fun x =>
        match x with
        | { fst := a, snd := b } => π_n a b ≫ π a) ∈
    GrothendieckTopology.sieves (coherentTopology C) X
Theorem: EffectiveEpiFamily_transitive
Proof state before:
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpimorphic (ofArrows Y π)
⊢ Sieve.generate
      (ofArrows
        (fun x =>
          match x with
          | { fst := a, snd := b } => Y_n a b)
        fun x =>
        match x with
        | { fst := a, snd := b } => π_n a b ≫ π a) ∈
    GrothendieckTopology.sieves (coherentTopology C) X
Tactic:
let H' := H
Proof state after:
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpimorphic (ofArrows Y π)
H' : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a) := H
⊢ Sieve.generate
      (ofArrows
        (fun x =>
          match x with
          | { fst := a, snd := b } => Y_n a b)
        fun x =>
        match x with
        | { fst := a, snd := b } => π_n a b ≫ π a) ∈
    GrothendieckTopology.sieves (coherentTopology C) X
Theorem: EffectiveEpiFamily_transitive
Proof state before:
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpimorphic (ofArrows Y π)
H' : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a) := H
⊢ Sieve.generate
      (ofArrows
        (fun x =>
          match x with
          | { fst := a, snd := b } => Y_n a b)
        fun x =>
        match x with
        | { fst := a, snd := b } => π_n a b ≫ π a) ∈
    GrothendieckTopology.sieves (coherentTopology C) X
Tactic:
conv at H' =>
  intro a
  rw [← Sieve.effectiveEpimorphic_family]
Proof state after:
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpimorphic (ofArrows Y π)
H' : ∀ (a : α), EffectiveEpimorphic (ofArrows (Y_n a) (π_n a))
⊢ Sieve.generate
      (ofArrows
        (fun x =>
          match x with
          | { fst := a, snd := b } => Y_n a b)
        fun x =>
        match x with
        | { fst := a, snd := b } => π_n a b ≫ π a) ∈
    GrothendieckTopology.sieves (coherentTopology C) X
Theorem: EffectiveEpiFamily_transitive
Proof state before:
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpimorphic (ofArrows Y π)
H' : ∀ (a : α), EffectiveEpimorphic (ofArrows (Y_n a) (π_n a))
⊢ Sieve.generate
      (ofArrows
        (fun x =>
          match x with
          | { fst := a, snd := b } => Y_n a b)
        fun x =>
        match x with
        | { fst := a, snd := b } => π_n a b ≫ π a) ∈
    GrothendieckTopology.sieves (coherentTopology C) X
Tactic:
apply Coverage.saturate.transitive X (Sieve.generate (Presieve.ofArrows Y π))
Proof state after:
case a
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpimorphic (ofArrows Y π)
H' : ∀ (a : α), EffectiveEpimorphic (ofArrows (Y_n a) (π_n a))
⊢ Coverage.saturate (coherentCoverage C) X (Sieve.generate (ofArrows Y π))

case a
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpimorphic (ofArrows Y π)
H' : ∀ (a : α), EffectiveEpimorphic (ofArrows (Y_n a) (π_n a))
⊢ ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ X⦄,
    (Sieve.generate (ofArrows Y π)).arrows f →
      Coverage.saturate (coherentCoverage C) Y_1
        (Sieve.pullback f
          (Sieve.generate
            (ofArrows
              (fun x =>
                match x with
                | { fst := a, snd := b } => Y_n a b)
              fun x =>
              match x with
              | { fst := a, snd := b } => π_n a b ≫ π a)))
Theorem: EffectiveEpiFamily_transitive
Proof state before:
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h₂ :
  Sieve.generate
      (ofArrows
        (fun x =>
          match x with
          | { fst := a, snd := b } => Y_n a b)
        fun x =>
        match x with
        | { fst := a, snd := b } => π_n a b ≫ π a) ∈
    GrothendieckTopology.sieves (coherentTopology C) X
⊢ EffectiveEpimorphic (ofArrows (fun c => Y_n c.fst c.snd) fun c => π_n c.fst c.snd ≫ π c.fst)
Tactic:
change Nonempty _
Proof state after:
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h₂ :
  Sieve.generate
      (ofArrows
        (fun x =>
          match x with
          | { fst := a, snd := b } => Y_n a b)
        fun x =>
        match x with
        | { fst := a, snd := b } => π_n a b ≫ π a) ∈
    GrothendieckTopology.sieves (coherentTopology C) X
⊢ Nonempty
    (IsColimit
      (cocone (Sieve.generate (ofArrows (fun c => Y_n c.fst c.snd) fun c => π_n c.fst c.snd ≫ π c.fst)).arrows))
Theorem: EffectiveEpiFamily_transitive
Proof state before:
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h₂ :
  Sieve.generate
      (ofArrows
        (fun x =>
          match x with
          | { fst := a, snd := b } => Y_n a b)
        fun x =>
        match x with
        | { fst := a, snd := b } => π_n a b ≫ π a) ∈
    GrothendieckTopology.sieves (coherentTopology C) X
⊢ Nonempty
    (IsColimit
      (cocone (Sieve.generate (ofArrows (fun c => Y_n c.fst c.snd) fun c => π_n c.fst c.snd ≫ π c.fst)).arrows))
Tactic:
rw [← Sieve.Yoneda_sheaf_iff_colimit]
Proof state after:
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h₂ :
  Sieve.generate
      (ofArrows
        (fun x =>
          match x with
          | { fst := a, snd := b } => Y_n a b)
        fun x =>
        match x with
        | { fst := a, snd := b } => π_n a b ≫ π a) ∈
    GrothendieckTopology.sieves (coherentTopology C) X
⊢ ∀ (W : C),
    IsSheafFor (yoneda.obj W)
      (Sieve.generate (ofArrows (fun c => Y_n c.fst c.snd) fun c => π_n c.fst c.snd ≫ π c.fst)).arrows
Theorem: EffectiveEpiFamily_transitive
Proof state before:
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h₂ :
  Sieve.generate
      (ofArrows
        (fun x =>
          match x with
          | { fst := a, snd := b } => Y_n a b)
        fun x =>
        match x with
        | { fst := a, snd := b } => π_n a b ≫ π a) ∈
    GrothendieckTopology.sieves (coherentTopology C) X
⊢ ∀ (W : C),
    IsSheafFor (yoneda.obj W)
      (Sieve.generate (ofArrows (fun c => Y_n c.fst c.snd) fun c => π_n c.fst c.snd ≫ π c.fst)).arrows
Tactic:
intro W
Proof state after:
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h₂ :
  Sieve.generate
      (ofArrows
        (fun x =>
          match x with
          | { fst := a, snd := b } => Y_n a b)
        fun x =>
        match x with
        | { fst := a, snd := b } => π_n a b ≫ π a) ∈
    GrothendieckTopology.sieves (coherentTopology C) X
W : C
⊢ IsSheafFor (yoneda.obj W)
    (Sieve.generate (ofArrows (fun c => Y_n c.fst c.snd) fun c => π_n c.fst c.snd ≫ π c.fst)).arrows
Theorem: EffectiveEpiFamily_transitive
Proof state before:
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h₂ :
  Sieve.generate
      (ofArrows
        (fun x =>
          match x with
          | { fst := a, snd := b } => Y_n a b)
        fun x =>
        match x with
        | { fst := a, snd := b } => π_n a b ≫ π a) ∈
    GrothendieckTopology.sieves (coherentTopology C) X
W : C
⊢ IsSheafFor (yoneda.obj W)
    (Sieve.generate (ofArrows (fun c => Y_n c.fst c.snd) fun c => π_n c.fst c.snd ≫ π c.fst)).arrows
Tactic:
apply coherentTopology.isSheaf_Yoneda
Proof state after:
case a
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h₂ :
  Sieve.generate
      (ofArrows
        (fun x =>
          match x with
          | { fst := a, snd := b } => Y_n a b)
        fun x =>
        match x with
        | { fst := a, snd := b } => π_n a b ≫ π a) ∈
    GrothendieckTopology.sieves (coherentTopology C) X
W : C
⊢ Sieve.generate (ofArrows (fun c => Y_n c.fst c.snd) fun c => π_n c.fst c.snd ≫ π c.fst) ∈
    GrothendieckTopology.sieves (coherentTopology C) X
Theorem: EffectiveEpiFamily_transitive
Proof state before:
case a
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h₂ :
  Sieve.generate
      (ofArrows
        (fun x =>
          match x with
          | { fst := a, snd := b } => Y_n a b)
        fun x =>
        match x with
        | { fst := a, snd := b } => π_n a b ≫ π a) ∈
    GrothendieckTopology.sieves (coherentTopology C) X
W : C
⊢ Sieve.generate (ofArrows (fun c => Y_n c.fst c.snd) fun c => π_n c.fst c.snd ≫ π c.fst) ∈
    GrothendieckTopology.sieves (coherentTopology C) X
Tactic:
exact h₂
Proof state after:
no goals
Theorem: EffectiveEpiFamily_transitive
Proof state before:
case a
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpimorphic (ofArrows Y π)
H' : ∀ (a : α), EffectiveEpimorphic (ofArrows (Y_n a) (π_n a))
⊢ Coverage.saturate (coherentCoverage C) X (Sieve.generate (ofArrows Y π))
Tactic:
apply Coverage.saturate.of
Proof state after:
case a.hS
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpimorphic (ofArrows Y π)
H' : ∀ (a : α), EffectiveEpimorphic (ofArrows (Y_n a) (π_n a))
⊢ ofArrows Y π ∈ Coverage.covering (coherentCoverage C) X
Theorem: EffectiveEpiFamily_transitive
Proof state before:
case a.hS
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpimorphic (ofArrows Y π)
H' : ∀ (a : α), EffectiveEpimorphic (ofArrows (Y_n a) (π_n a))
⊢ ofArrows Y π ∈ Coverage.covering (coherentCoverage C) X
Tactic:
use α, inferInstance, Y, π
Proof state after:
case a.hS
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpimorphic (ofArrows Y π)
H' : ∀ (a : α), EffectiveEpimorphic (ofArrows (Y_n a) (π_n a))
⊢ ofArrows Y π = ofArrows Y π ∧ EffectiveEpiFamily Y π
Theorem: EffectiveEpiFamily_transitive
Proof state before:
case a.hS
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpimorphic (ofArrows Y π)
H' : ∀ (a : α), EffectiveEpimorphic (ofArrows (Y_n a) (π_n a))
⊢ ofArrows Y π = ofArrows Y π ∧ EffectiveEpiFamily Y π
Tactic:
simp only [true_and]
Proof state after:
case a.hS
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpimorphic (ofArrows Y π)
H' : ∀ (a : α), EffectiveEpimorphic (ofArrows (Y_n a) (π_n a))
⊢ EffectiveEpiFamily Y π
Theorem: EffectiveEpiFamily_transitive
Proof state before:
case a.hS
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpimorphic (ofArrows Y π)
H' : ∀ (a : α), EffectiveEpimorphic (ofArrows (Y_n a) (π_n a))
⊢ EffectiveEpiFamily Y π
Tactic:
exact Iff.mp (Sieve.effectiveEpimorphic_family Y π) h'
Proof state after:
no goals
Theorem: EffectiveEpiFamily_transitive
Proof state before:
case a
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpimorphic (ofArrows Y π)
H' : ∀ (a : α), EffectiveEpimorphic (ofArrows (Y_n a) (π_n a))
⊢ ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ X⦄,
    (Sieve.generate (ofArrows Y π)).arrows f →
      Coverage.saturate (coherentCoverage C) Y_1
        (Sieve.pullback f
          (Sieve.generate
            (ofArrows
              (fun x =>
                match x with
                | { fst := a, snd := b } => Y_n a b)
              fun x =>
              match x with
              | { fst := a, snd := b } => π_n a b ≫ π a)))
Tactic:
intro V f ⟨Y₁, h, g, ⟨hY, hf⟩⟩
Proof state after:
case a
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h✝ : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpimorphic (ofArrows Y π)
H' : ∀ (a : α), EffectiveEpimorphic (ofArrows (Y_n a) (π_n a))
V : C
f : V ⟶ X
Y₁ : C
h : V ⟶ Y₁
g : Y₁ ⟶ X
hY : ofArrows Y π g
hf : h ≫ g = f
⊢ Coverage.saturate (coherentCoverage C) V
    (Sieve.pullback f
      (Sieve.generate
        (ofArrows
          (fun x =>
            match x with
            | { fst := a, snd := b } => Y_n a b)
          fun x =>
          match x with
          | { fst := a, snd := b } => π_n a b ≫ π a)))