mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
S : Presieve X
⊢ map F S ≤ functorPushforward F S

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
ι : Type u_1
X : C
Z : ι → C
f : (i : ι) → Z i ⟶ X
R : (i : ι) → Presieve (Z i)
⊢ (Sieve.bind (Sieve.ofArrows Z f).arrows fun x x_1 hg ↦
      Sieve.pullback (Sieve.ofArrows.h hg) (Sieve.generate (R (Sieve.ofArrows.i hg)))) ≤
    Sieve.generate (bindOfArrows Z f R)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
P : Cᵒᵖ ⥤ Type v₁
⊢ IsSheafFor P S.arrows ↔ YonedaSheafCondition P S

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Plus

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{w', w} D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Cᵒᵖ ⥤ D
X Y : C
f✝ : X ⟶ Y
S T : (J.Cover Y)ᵒᵖ
f : S ⟶ T
I : (unop ((J.pullback f✝).op.obj T)).shape.L
⊢ ((J.diagram P Y).map f ≫
        Multiequalizer.lift ((unop ((J.pullback f✝).op.obj T)).index P) ((J.diagram P Y).obj T)
          (fun I ↦ Multiequalizer.ι ((unop T).index P) (Cover.Arrow.base I)) ⋯) ≫
      Multiequalizer.ι ((unop ((J.pullback f✝).op.obj T)).index P) I =
    (Multiequalizer.lift ((unop ((J.pullback f✝).op.obj S)).index P) ((J.diagram P Y).obj S)
          (fun I ↦ Multiequalizer.ι ((unop S).index P) (Cover.Arrow.base I)) ⋯ ≫
        ((J.pullback f✝).op ⋙ J.diagram P X).map f) ≫
      Multiequalizer.ι ((unop ((J.pullback f✝).op.obj T)).index P) I

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Plus

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{w', w} D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P✝ P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X : C
W : (J.Cover X)ᵒᵖ
i : (unop W).shape.R
⊢ (Multiequalizer.ι ((unop W).index P) ((unop W).shape.fst i) ≫ η.app (op ((unop W).shape.fst i).Y)) ≫
      ((unop W).index Q).fst i =
    (Multiequalizer.ι ((unop W).index P) ((unop W).shape.snd i) ≫ η.app (op ((unop W).shape.snd i).Y)) ≫
      ((unop W).index Q).snd i

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
⊢ (∀ (c : Cone (S.arrows.diagram.op ⋙ P)), Subsingleton (c ⟶ P.mapCone S.arrows.cocone.op)) ↔
    ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ coyoneda.obj E) S.arrows

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Plus

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{w', w} D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Cᵒᵖ ⥤ D
⊢ J.diagramNatTrans (𝟙 P) X = 𝟙 (J.diagram P X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : Type u₂
inst✝¹ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
inst✝ : HasPullbacks C
K : Pretopology C
⊢ IsSheaf K.toGrothendieck P ↔
    ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Nonempty (IsLimit (P.mapCone (generate R).arrows.cocone.op))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Plus

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : Preadditive D
X : C
P Q : Cᵒᵖ ⥤ D
⊢ J.diagramNatTrans 0 X = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
E : A
X : C
P : Cᵒᵖ ⥤ A
hP : IsSheaf J P
S : J.Cover X
x : (I : S.Arrow) → E ⟶ P.obj (op I.Y)
hx : ∀ ⦃I₁ I₂ : S.Arrow⦄ (r : I₁.Relation I₂), x I₁ ≫ P.map r.g₁.op = x I₂ ≫ P.map r.g₂.op
I : S.Arrow
⊢ hP.amalgamate S x hx ≫ P.map I.f.op = x I

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Plus

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{w', w} D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P Q R : Cᵒᵖ ⥤ D
η : P ⟶ Q
γ : Q ⟶ R
X : C
⊢ J.diagramNatTrans (η ≫ γ) X = J.diagramNatTrans η X ≫ J.diagramNatTrans γ X

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
⊢ (IsSeparatedFor P R ∧ ∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t) ↔ IsSheafFor P R

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
t : IsSeparatedFor P R
⊢ (∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t) → IsSheafFor P R

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
hP : IsSheaf J P
I : Type u_1
S : C
X : I → C
f : (i : I) → X i ⟶ S
hf : ofArrows X f ∈ J S
E : A
x y : E ⟶ P.obj (op S)
h : ∀ (i : I), x ≫ P.map (f i).op = y ≫ P.map (f i).op
⊢ x = y

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
F G : Sheaf J A
f g : F ⟶ G
⊢ f = g ↔ f.hom = g.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
F G : Sheaf J A
f g : F ⟶ G
h : f.hom = g.hom
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type t
inst✝¹ : Small.{w, t} I
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).HasPairwisePullbacks
⊢ IsSheafFor P (Presieve.ofArrows X π) ↔ Nonempty (IsLimit (Fork.ofι (forkMap P X π) ⋯))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
⊢ IsSheafFor P R ↔ IsSheafFor P (generate R).arrows

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X✝ : C
R : Presieve X✝
S : Sieve X✝
inst✝ : R.HasPairwisePullbacks
F : Cᵒᵖ ⥤ Type u_1
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
⊢ F.map f.op ≫ F.map c.fst.op = F.map f.op ≫ F.map c.snd.op

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Plus

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
⊢ ∀ (X : Cᵒᵖ),
    colimMap (J.diagramPullback P (𝟙 X).unop) ≫ colimit.pre (J.diagram P (unop X)) (J.pullback (𝟙 X).unop).op =
      𝟙 (colimit (J.diagram P (unop X)))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
⊢ IsSheafFor P (singleton (𝟙 X))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
⊢ IsSheafFor P ⊤

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P₁ : Cᵒᵖ ⥤ Type w
P₂ : Cᵒᵖ ⥤ Type w'
e : ⦃X : C⦄ → P₁.obj (op X) ≃ P₂.obj (op X)
he :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₁.obj (op Y)),
    e ((ConcreteCategory.hom (P₁.map f.op)) x) = (ConcreteCategory.hom (P₂.map f.op)) (e x)
X✝ : C
R : Presieve X✝
hP₁ : IsSheafFor P₁ R
x₂ : FamilyOfElements P₂ R
hx₂ : x₂.Compatible
X Y : C
f : X ⟶ Y
x : P₂.obj (op Y)
⊢ e (e.symm ((ConcreteCategory.hom (P₂.map f.op)) x)) = e ((ConcreteCategory.hom (P₁.map f.op)) (e.symm x))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type u_1
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
x : F.obj (op X)
⊢ (∀ {Z : C} (p₁ p₂ : Z ⟶ X),
      p₁ ≫ f = p₂ ≫ f → (ConcreteCategory.hom (F.map p₁.op)) x = (ConcreteCategory.hom (F.map p₂.op)) x) ↔
    (ConcreteCategory.hom (F.map c.fst.op)) x = (ConcreteCategory.hom (F.map c.snd.op)) x

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P₁ : Cᵒᵖ ⥤ Type w
P₂ : Cᵒᵖ ⥤ Type w'
e : ⦃X : C⦄ → P₁.obj (op X) ≃ P₂.obj (op X)
he :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₁.obj (op Y)),
    e ((ConcreteCategory.hom (P₁.map f.op)) x) = (ConcreteCategory.hom (P₂.map f.op)) (e x)
X : C
R : Presieve X
hP₁ : IsSheafFor P₁ R
x₂ : FamilyOfElements P₂ R
hx₂ : x₂.Compatible
he' :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₂.obj (op Y)),
    e.symm ((ConcreteCategory.hom (P₂.map f.op)) x) = (ConcreteCategory.hom (P₁.map f.op)) (e.symm x)
x₁ : FamilyOfElements P₁ R := fun Y f hf ↦ e.symm (x₂ f hf)
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : R f₁
h₂ : R f₂
fac : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ e ((ConcreteCategory.hom (P₁.map g₁.op)) (x₁ f₁ h₁)) = e ((ConcreteCategory.hom (P₁.map g₂.op)) (x₁ f₂ h₂))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P₁ : Cᵒᵖ ⥤ Type w
P₂ : Cᵒᵖ ⥤ Type w'
e : ⦃X : C⦄ → P₁.obj (op X) ≃ P₂.obj (op X)
he :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₁.obj (op Y)),
    e ((ConcreteCategory.hom (P₁.map f.op)) x) = (ConcreteCategory.hom (P₂.map f.op)) (e x)
X : C
R : Presieve X
hP₁ : IsSheafFor P₁ R
x₂ : FamilyOfElements P₂ R
hx₂ : x₂.Compatible
he' :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₂.obj (op Y)),
    e.symm ((ConcreteCategory.hom (P₂.map f.op)) x) = (ConcreteCategory.hom (P₁.map f.op)) (e.symm x)
x₁ : FamilyOfElements P₁ R := fun Y f hf ↦ e.symm (x₂ f hf)
hx₁ : x₁.Compatible
t₂ : P₂.obj (op X)
⊢ x₂.IsAmalgamation t₂ ↔ x₁.IsAmalgamation (e.symm t₂)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type u_1
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
⊢ Presieve.IsSheafFor F (Presieve.singleton f) ↔ Nonempty (IsLimit (Fork.ofι (F.map f.op) ⋯))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X✝ : C
R : Presieve X✝
S : Sieve X✝
inst✝¹ : R.HasPairwisePullbacks
F : Cᵒᵖ ⥤ Type u_1
X Y : C
f : X ⟶ Y
inst✝ : HasPullback f f
⊢ F.map f.op ≫ F.map (pullback.fst f f).op = F.map f.op ≫ F.map (pullback.snd f f).op

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝¹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝ : ConcreteCategory D FD
X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : Meq P S
Y : C
f g : Y ⟶ X
h : f = g
hf : (↑S).arrows f
⊢ (↑S).arrows g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝¹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝ : ConcreteCategory D FD
X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : Meq P S
Y : C
f g : Y ⟶ X
h : f = g
hf : (↑S).arrows f
⊢ ↑x { Y := Y, f := f, hf := hf } = ↑x { Y := Y, f := g, hf := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝¹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝ : ConcreteCategory D FD
X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : ToType (P.obj (op X))
I : S.Relation
⊢ (ConcreteCategory.hom (P.map I.r.g₁.op)) ((fun I ↦ (ConcreteCategory.hom (P.map I.f.op)) x) I.fst) =
    (ConcreteCategory.hom (P.map I.r.g₂.op)) ((fun I ↦ (ConcreteCategory.hom (P.map I.f.op)) x) I.snd)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁴ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝² : ConcreteCategory D FD
inst✝¹ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
inst✝ : HasMultiequalizer (S.index P)
x : Meq P S
I : S.Arrow
⊢ (ConcreteCategory.hom (Multiequalizer.ι (S.index P) I)) ((equiv P S).symm x) = ↑x I

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P₁ : Cᵒᵖ ⥤ Type w
P₂ : Cᵒᵖ ⥤ Type w'
e : ⦃X : C⦄ → P₁.obj (op X) ≃ P₂.obj (op X)
he :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₁.obj (op Y)),
    e ((ConcreteCategory.hom (P₁.map f.op)) x) = (ConcreteCategory.hom (P₂.map f.op)) (e x)
X : C
R : Presieve X
hP₁ : IsSheafFor P₁ R
x₂ : FamilyOfElements P₂ R
hx₂ : x₂.Compatible
he' :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₂.obj (op Y)),
    e.symm ((ConcreteCategory.hom (P₂.map f.op)) x) = (ConcreteCategory.hom (P₁.map f.op)) (e.symm x)
x₁ : FamilyOfElements P₁ R := fun Y f hf ↦ e.symm (x₂ f hf)
hx₁ : x₁.Compatible
this : ∀ (t₂ : P₂.obj (op X)), x₂.IsAmalgamation t₂ ↔ x₁.IsAmalgamation (e.symm t₂)
t₂ : P₂.obj (op X)
ht₂ : x₂.IsAmalgamation t₂
⊢ x₁.IsAmalgamation (e.symm t₂)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P₁ : Cᵒᵖ ⥤ Type w
P₂ : Cᵒᵖ ⥤ Type w'
e : ⦃X : C⦄ → P₁.obj (op X) ≃ P₂.obj (op X)
he :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₁.obj (op Y)),
    e ((ConcreteCategory.hom (P₁.map f.op)) x) = (ConcreteCategory.hom (P₂.map f.op)) (e x)
X : C
R : Presieve X
hP₁ : IsSheafFor P₁ R
x₂ : FamilyOfElements P₂ R
hx₂ : x₂.Compatible
⊢ ∃! t, x₂.IsAmalgamation t

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
⊢ Presheaf.IsSheaf J P ↔ Presieve.IsSheaf J P

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J✝ : GrothendieckTopology C
A✝ : Type u₂
inst✝¹ : Category.{v₂, u₂} A✝
A : Type u₂
inst✝ : Category.{v₂, u₂} A
J : GrothendieckTopology C
ℱ : Sheaf J A
E : A
⊢ Presheaf.IsSheaf J (ℱ.obj ⋙ coyoneda.obj (op E))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
hP : IsSheaf J P
X : C
S : Sieve X
hS : S ∈ J X
⊢ Presieve.IsSheafFor P S.arrows

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
F : Sheaf J A
X : C
H : ⊥ ∈ J X
Y : A
⊢ Presieve.FamilyOfElements (F.obj ⋙ coyoneda.obj (op Y)) ⊥.arrows

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
F : Sheaf J A
X : C
H : ⊥ ∈ J X
Y : A
⊢ Presieve.FamilyOfElements.Compatible fun ⦃Y_1⦄ f a ↦ ⋯.elim

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
F : Sheaf J A
X : C
H : ⊥ ∈ J X
Y : A
t : (F.obj ⋙ coyoneda.obj (op Y)).obj (op X)
h :
  (fun t ↦ Presieve.FamilyOfElements.IsAmalgamation (fun ⦃Y_1⦄ f a ↦ ⋯.elim) t) t ∧
    ∀ (y : (F.obj ⋙ coyoneda.obj (op Y)).obj (op X)),
      (fun t ↦ Presieve.FamilyOfElements.IsAmalgamation (fun ⦃Y_1⦄ f a ↦ ⋯.elim) t) y → y = t
a : Y ⟶ F.obj.obj (op X)
⊢ (fun t ↦ Presieve.FamilyOfElements.IsAmalgamation (fun ⦃Y_1⦄ f a ↦ ⋯.elim) t) a

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P₁ : Cᵒᵖ ⥤ Type w
P₂ : Cᵒᵖ ⥤ Type w'
e : ⦃X : C⦄ → P₁.obj (op X) ≃ P₂.obj (op X)
he :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₁.obj (op Y)),
    e ((ConcreteCategory.hom (P₁.map f.op)) x) = (ConcreteCategory.hom (P₂.map f.op)) (e x)
X : C
R : Presieve X
⊢ IsSheafFor P₁ R ↔ IsSheafFor P₂ R

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁴ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝² : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
Y X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : Meq P S
f : Y ⟶ X
⊢ (ConcreteCategory.hom ((J.plusObj P).map f.op)) (mk x) = mk (x.pullback f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
F : Sheaf J A
X : C
H : ⊥ ∈ J X
⊢ IsTerminal (F.obj.obj (op X))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
X : A
hX : IsTerminal X
⊢ ∀ (X_1 : Sheaf J A) (m : X_1 ⟶ terminal J hX), m = { hom := (Functor.isTerminalConst Cᵒᵖ hX).from X_1.obj }

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
P' : Cᵒᵖ ⥤ Type w
i : P ≅ P'
hP : IsSeparatedFor P R
⊢ IsSeparatedFor P' R

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
H : J = ⊤
F : Sheaf J A
⊢ IsTerminal F

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
f : P ⟶ Q
inst✝ : Mono f
h : IsSeparatedFor Q R
⊢ IsSeparatedFor P R

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Plus

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
⊢ ∀ {X Y Z : Cᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z),
    colimMap (J.diagramPullback P (f ≫ g).unop) ≫ colimit.pre (J.diagram P (unop Z)) (J.pullback (f ≫ g).unop).op =
      (colimMap (J.diagramPullback P f.unop) ≫ colimit.pre (J.diagram P (unop Y)) (J.pullback f.unop).op) ≫
        colimMap (J.diagramPullback P g.unop) ≫ colimit.pre (J.diagram P (unop Z)) (J.pullback g.unop).op

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
A' : Type u₂
inst✝¹ : Category.{max v₁ u₁, u₂} A'
B : Type u₃
inst✝ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
P' : Cᵒᵖ ⥤ A'
X : C
S : J.Cover X
hP : IsSheaf J P
⊢ ∀ (s : Cone (S.index P).multicospan) (j : WalkingMulticospan S.shape),
    hP.amalgamate S (fun x ↦ Multifork.ι s x) ⋯ ≫ (S.multifork P).π.app j = s.π.app j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
A' : Type u₂
inst✝¹ : Category.{max v₁ u₁, u₂} A'
B : Type u₃
inst✝ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
P' : Cᵒᵖ ⥤ A'
X : C
S : J.Cover X
hP : IsSheaf J P
⊢ ∀ (s : Cone (S.index P).multicospan) (m : s.pt ⟶ (S.multifork P).pt),
    (∀ (j : WalkingMulticospan S.shape), m ≫ (S.multifork P).π.app j = s.π.app j) →
      m = hP.amalgamate S (fun x ↦ Multifork.ι s x) ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Plus

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X Y : Cᵒᵖ
f : X ⟶ Y
j✝ : (J.Cover (unop X))ᵒᵖ
I : (unop ((J.pullback f.unop).op.obj j✝)).shape.L
⊢ (Multiequalizer.lift ((unop ((J.pullback f.unop).op.obj j✝)).index P) ((J.diagram P (unop X)).obj j✝)
          (fun I ↦ Multiequalizer.ι ((unop j✝).index P) (Cover.Arrow.base I)) ⋯ ≫
        (J.diagramNatTrans η (unop Y)).app ((J.pullback f.unop).op.obj j✝)) ≫
      Multiequalizer.ι ((unop ((J.pullback f.unop).op.obj j✝)).index Q) I =
    ((J.diagramNatTrans η (unop X)).app j✝ ≫
        Multiequalizer.lift ((unop ((J.pullback f.unop).op.obj j✝)).index Q) ((J.diagram Q (unop X)).obj j✝)
          (fun I ↦ Multiequalizer.ι ((unop j✝).index Q) (Cover.Arrow.base I)) ⋯) ≫
      Multiequalizer.ι ((unop ((J.pullback f.unop).op.obj j✝)).index Q) I

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Plus

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
⊢ ∀ ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y),
    (J.plusObj P).map f ≫ colimMap (J.diagramNatTrans η (unop Y)) =
      colimMap (J.diagramNatTrans η (unop X)) ≫ (J.plusObj Q).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁴ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝² : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : ToType (P.obj (op X))
⊢ (ConcreteCategory.hom ((J.toPlus P).app (op X))) x = mk (Meq.mk S x)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
S : Sieve X
R : Presieve X
h : S.arrows ≤ R
hS : IsSheafFor P S.arrows
trans : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → IsSeparatedFor P (Sieve.pullback f S).arrows
⊢ IsSheafFor P R

Tactic:
by

Goal state after: