ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u_2<VAR>CategoryTheory.Category.{u_6, u_2} A<VAR>t : C<VAR>ht : CategoryTheory.Limits.IsTerminal t<VAR>B : Type u_3<VAR>CategoryTheory.Category.{u_4, u_3} B<VAR>U : A ⥤ B<VAR>CategoryTheory.HasWeakSheafify J A<VAR>CategoryTheory.HasWeakSheafify J B<VAR>J.PreservesSheafification U<VAR>J.HasSheafCompose U<VAR>F : CategoryTheory.Sheaf J A<GOAL>((CategoryTheory.sheafifyComposeIso J U ((CategoryTheory.Functor.const Cᵒᵖ).obj (F.val.obj (Opposite.op t)))).symm ≪≫ (CategoryTheory.presheafToSheaf J B ⋙ CategoryTheory.sheafToPresheaf J B).mapIso (CategoryTheory.Functor.constComp Cᵒᵖ (F.val.obj (Opposite.op t)) U)).hom ≫ ((CategoryTheory.constantSheafAdj J B ht).counit.app ((CategoryTheory.sheafCompose J U).obj F)).val = ((CategoryTheory.sheafCompose J U).map ((CategoryTheory.constantSheafAdj J A ht).counit.app F)).val
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u_2<VAR>CategoryTheory.Category.{u_4, u_2} A<VAR>t : C<VAR>ht : CategoryTheory.Limits.IsTerminal t<VAR>B : Type u_3<VAR>CategoryTheory.Category.{u_5, u_3} B<VAR>U : A ⥤ B<VAR>CategoryTheory.HasWeakSheafify J A<VAR>CategoryTheory.HasWeakSheafify J B<VAR>J.PreservesSheafification U<VAR>J.HasSheafCompose U<VAR>F : CategoryTheory.Sheaf J A<VAR>(CategoryTheory.sheafCompose J U).ReflectsIsomorphisms<VAR>CategoryTheory.Sheaf.IsDiscrete J ht ((CategoryTheory.sheafCompose J U).obj F)<GOAL>CategoryTheory.Sheaf.IsDiscrete J ht F
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u_2<VAR>CategoryTheory.Category.{u_4, u_2} A<VAR>t : C<VAR>ht : CategoryTheory.Limits.IsTerminal t<VAR>B : Type u_3<VAR>CategoryTheory.Category.{u_5, u_3} B<VAR>U : A ⥤ B<VAR>CategoryTheory.HasWeakSheafify J A<VAR>CategoryTheory.HasWeakSheafify J B<VAR>(CategoryTheory.constantSheaf J A).Faithful<VAR>(CategoryTheory.constantSheaf J A).Full<VAR>(CategoryTheory.constantSheaf J B).Faithful<VAR>(CategoryTheory.constantSheaf J B).Full<VAR>J.PreservesSheafification U<VAR>J.HasSheafCompose U<VAR>F : CategoryTheory.Sheaf J A<VAR>(CategoryTheory.sheafCompose J U).ReflectsIsomorphisms<GOAL>CategoryTheory.Sheaf.IsDiscrete J ht F ↔ CategoryTheory.Sheaf.IsDiscrete J ht ((CategoryTheory.sheafCompose J U).obj F)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : C<VAR>self : CategoryTheory.Projective P<VAR>E X : C<VAR>f : P ⟶ X<VAR>e : E ⟶ X<VAR>CategoryTheory.Epi e<GOAL>∃ f', f' ≫ e = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>h : CategoryTheory.Limits.IsZero X<GOAL>CategoryTheory.Projective X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>self : CategoryTheory.ProjectivePresentation X<GOAL>CategoryTheory.Epi self.f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>self : CategoryTheory.ProjectivePresentation X<GOAL>CategoryTheory.Projective self.p
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.EnoughProjectives C<VAR>X : C<GOAL>Nonempty (CategoryTheory.ProjectivePresentation X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P X E : C<VAR>CategoryTheory.Projective P<VAR>f : P ⟶ X<VAR>e : E ⟶ X<VAR>CategoryTheory.Epi e<GOAL>CategoryTheory.Projective.factorThru f e ≫ e = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P Q : C<VAR>i : P ≅ Q<VAR>hP : CategoryTheory.Projective P<GOAL>CategoryTheory.Projective Q
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P Q : C<VAR>i : P ≅ Q<GOAL>CategoryTheory.Projective P ↔ CategoryTheory.Projective Q
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : C<GOAL>CategoryTheory.Projective P ↔ (CategoryTheory.coyoneda.obj (Opposite.op P)).PreservesEpimorphisms
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : F ⊣ G<VAR>G.PreservesEpimorphisms<VAR>P : C<VAR>hP : CategoryTheory.Projective P<GOAL>CategoryTheory.Projective (F.obj P)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : F ⊣ G<VAR>F.Full<VAR>F.Faithful<VAR>P : C<VAR>hP : CategoryTheory.Projective (F.obj P)<GOAL>CategoryTheory.Projective P
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>F : C ≌ D<VAR>P : C<GOAL>CategoryTheory.Projective (F.functor.obj P) ↔ CategoryTheory.Projective P
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>F : C ≌ D<GOAL>CategoryTheory.EnoughProjectives C ↔ CategoryTheory.EnoughProjectives D
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : Cᵒᵖ<VAR>f g : X ⟶ Y<GOAL>(f + g).unop = f.unop + g.unop
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : Cᵒᵖ<VAR>k : ℤ<VAR>f : X ⟶ Y<GOAL>(k • f).unop = k • f.unop
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : Cᵒᵖ<VAR>f : X ⟶ Y<GOAL>(-f).unop = -f.unop
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>f g : X ⟶ Y<GOAL>(f + g).op = f.op + g.op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>k : ℤ<VAR>f : X ⟶ Y<GOAL>(k • f).op = k • f.op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(-f).op = -f.op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : Cᵒᵖ<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.unopHom X Y) f = f.unop
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : Cᵒᵖ<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>f : ι → (X ⟶ Y)<GOAL>(s.sum f).unop = ∑ i ∈ s, (f i).unop
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.opHom X Y) f = f.op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>f : ι → (X ⟶ Y)<GOAL>(s.sum f).op = ∑ i ∈ s, (f i).op
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>self : CategoryTheory.Subgroupoid C<VAR>c d e : C<VAR>p : c ⟶ d<GOAL>p ∈ self.arrows c d → ∀ {q : d ⟶ e}, q ∈ self.arrows d e → CategoryTheory.CategoryStruct.comp p q ∈ self.arrows c e
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>self : CategoryTheory.Subgroupoid C<VAR>c d : C<VAR>p : c ⟶ d<GOAL>p ∈ self.arrows c d → CategoryTheory.Groupoid.inv p ∈ self.arrows d c
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>S : CategoryTheory.Subgroupoid C<VAR>c d : C<VAR>f : c ⟶ d<GOAL>CategoryTheory.Groupoid.inv f ∈ S.arrows d c ↔ f ∈ S.arrows c d
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>S : CategoryTheory.Subgroupoid C<VAR>c d e : C<VAR>f : c ⟶ d<VAR>g : d ⟶ e<VAR>hf : f ∈ S.arrows c d<GOAL>CategoryTheory.CategoryStruct.comp f g ∈ S.arrows c e ↔ g ∈ S.arrows d e
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>S : CategoryTheory.Subgroupoid C<VAR>c d e : C<VAR>f : c ⟶ d<VAR>g : d ⟶ e<VAR>hg : g ∈ S.arrows d e<GOAL>CategoryTheory.CategoryStruct.comp f g ∈ S.arrows c e ↔ f ∈ S.arrows c d
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>S : CategoryTheory.Subgroupoid C<VAR>c d : C<VAR>f : c ⟶ d<VAR>h : f ∈ S.arrows c d<GOAL>c ∈ S.objs
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>S : CategoryTheory.Subgroupoid C<VAR>c d : C<VAR>f : c ⟶ d<VAR>h : f ∈ S.arrows c d<GOAL>d ∈ S.objs
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>S : CategoryTheory.Subgroupoid C<VAR>c : C<GOAL>c ∈ S.objs → CategoryTheory.CategoryStruct.id c ∈ S.arrows c c
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>S : CategoryTheory.Subgroupoid C<VAR>c d : C<VAR>f : c ⟶ d<VAR>h : f ∈ S.arrows c d<GOAL>CategoryTheory.CategoryStruct.id c ∈ S.arrows c c
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>S : CategoryTheory.Subgroupoid C<VAR>c d : C<VAR>f : c ⟶ d<VAR>h : f ∈ S.arrows c d<GOAL>CategoryTheory.CategoryStruct.id d ∈ S.arrows d d
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>S : CategoryTheory.Subgroupoid C<GOAL>∀ {X Y Z : ↑S.objs} (p : X ⟶ Y) (q : Y ⟶ Z), ↑(CategoryTheory.CategoryStruct.comp p q) = CategoryTheory.CategoryStruct.comp ↑p ↑q
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>S : CategoryTheory.Subgroupoid C<GOAL>∀ {X Y : ↑S.objs} (p : X ⟶ Y), ↑(CategoryTheory.Groupoid.inv p) = CategoryTheory.Groupoid.inv ↑p
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>S : CategoryTheory.Subgroupoid C<VAR>c d : ↑S.objs<VAR>p : c ⟶ d<GOAL>↑(CategoryTheory.inv p) = CategoryTheory.inv ↑p
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>S : CategoryTheory.Subgroupoid C<GOAL>Function.Injective S.hom.obj
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>S : CategoryTheory.Subgroupoid C<VAR>c d : ↑S.objs<GOAL>Function.Injective fun f => S.hom.map f
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>S : CategoryTheory.Subgroupoid C<VAR>F : (c : C) × (d : C) × (c ⟶ d)<GOAL>F ∈ S ↔ F.snd.snd ∈ S.arrows F.fst F.snd.fst
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>S T : CategoryTheory.Subgroupoid C<GOAL>S ≤ T ↔ ∀ {c d : C}, S.arrows c d ⊆ T.arrows c d
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>c d : C<VAR>f : c ⟶ d<GOAL>f ∈ ⊤.arrows c d
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>c : C<GOAL>c ∈ ⊤.objs
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>s : Set (CategoryTheory.Subgroupoid C)<VAR>c d : C<VAR>p : c ⟶ d<GOAL>p ∈ (sInf s).arrows c d ↔ ∀ S ∈ s, p ∈ S.arrows c d
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>s : Set (CategoryTheory.Subgroupoid C)<VAR>p : (c : C) × (d : C) × (c ⟶ d)<GOAL>p ∈ sInf s ↔ ∀ S ∈ s, p ∈ S
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>S T : CategoryTheory.Subgroupoid C<VAR>h : S ≤ T<GOAL>S.objs ⊆ T.objs
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>S T : CategoryTheory.Subgroupoid C<VAR>h : S ≤ T<GOAL>Function.Injective (CategoryTheory.Subgroupoid.inclusion h).obj
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>S T : CategoryTheory.Subgroupoid C<VAR>h : S ≤ T<VAR>s t : ↑S.objs<GOAL>Function.Injective fun f => (CategoryTheory.Subgroupoid.inclusion h).map f
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>S : CategoryTheory.Subgroupoid C<GOAL>CategoryTheory.Subgroupoid.inclusion ⋯ = CategoryTheory.Functor.id ↑S.objs
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>R S T : CategoryTheory.Subgroupoid C<VAR>k : R ≤ S<VAR>h : S ≤ T<GOAL>CategoryTheory.Subgroupoid.inclusion ⋯ = (CategoryTheory.Subgroupoid.inclusion k).comp (CategoryTheory.Subgroupoid.inclusion h)
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>S T : CategoryTheory.Subgroupoid C<VAR>h : S ≤ T<GOAL>(CategoryTheory.Subgroupoid.inclusion h).comp T.hom = S.hom
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>c d : C<VAR>f : c ⟶ d<GOAL>f ∈ CategoryTheory.Subgroupoid.discrete.arrows c d ↔ ∃ (h : c = d), f = CategoryTheory.eqToHom h
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>S : CategoryTheory.Subgroupoid C<VAR>self : S.IsWide<VAR>c : C<GOAL>CategoryTheory.CategoryStruct.id c ∈ S.arrows c c
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>S : CategoryTheory.Subgroupoid C<GOAL>S.IsWide ↔ S.objs = Set.univ
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>S : CategoryTheory.Subgroupoid C<VAR>Sw : S.IsWide<VAR>c : C<GOAL>CategoryTheory.CategoryStruct.id c ∈ S.arrows c c
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>S : CategoryTheory.Subgroupoid C<VAR>Sw : S.IsWide<VAR>c d : C<VAR>h : c = d<GOAL>CategoryTheory.eqToHom h ∈ S.arrows c d
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>S : CategoryTheory.Subgroupoid C<VAR>self : S.IsNormal<VAR>c d : C<VAR>p : c ⟶ d<VAR>γ : c ⟶ c<GOAL>γ ∈ S.arrows c c → CategoryTheory.CategoryStruct.comp (CategoryTheory.Groupoid.inv p) (CategoryTheory.CategoryStruct.comp γ p) ∈ S.arrows d d
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>S : CategoryTheory.Subgroupoid C<VAR>Sn : S.IsNormal<VAR>c d : C<VAR>p : d ⟶ c<VAR>γ : c ⟶ c<GOAL>γ ∈ S.arrows c c → CategoryTheory.CategoryStruct.comp p (CategoryTheory.CategoryStruct.comp γ (CategoryTheory.Groupoid.inv p)) ∈ S.arrows d d
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>S : CategoryTheory.Subgroupoid C<VAR>Sn : S.IsNormal<VAR>c d : C<VAR>p : c ⟶ d<GOAL>Set.BijOn (fun γ => CategoryTheory.CategoryStruct.comp (CategoryTheory.Groupoid.inv p) (CategoryTheory.CategoryStruct.comp γ p)) (S.arrows c c) (S.arrows d d)
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<GOAL>⊤.IsNormal
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>s : Set (CategoryTheory.Subgroupoid C)<VAR>sn : ∀ S ∈ s, S.IsNormal<GOAL>(sInf s).IsNormal
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<GOAL>CategoryTheory.Subgroupoid.discrete.IsNormal
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>S : CategoryTheory.Subgroupoid C<VAR>Sn : S.IsNormal<VAR>c : C<VAR>cS : c ∈ S.objs<GOAL>(S.vertexSubgroup cS).Normal
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>X : (c d : C) → Set (c ⟶ d)<VAR>c d : C<GOAL>X c d ⊆ (CategoryTheory.Subgroupoid.generated X).arrows c d
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>X : (c d : C) → Set (c ⟶ d)<GOAL>CategoryTheory.Subgroupoid.generated X ≤ CategoryTheory.Subgroupoid.generatedNormal X
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>X : (c d : C) → Set (c ⟶ d)<GOAL>(CategoryTheory.Subgroupoid.generatedNormal X).IsNormal
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>X : (c d : C) → Set (c ⟶ d)<VAR>S : CategoryTheory.Subgroupoid C<VAR>Sn : S.IsNormal<GOAL>CategoryTheory.Subgroupoid.generatedNormal X ≤ S ↔ ∀ (c d : C), X c d ⊆ S.arrows c d
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>D : Type u_1<VAR>CategoryTheory.Groupoid D<VAR>φ : CategoryTheory.Functor C D<VAR>S T : CategoryTheory.Subgroupoid D<GOAL>S ≤ T → CategoryTheory.Subgroupoid.comap φ S ≤ CategoryTheory.Subgroupoid.comap φ T
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>D : Type u_1<VAR>CategoryTheory.Groupoid D<VAR>φ : CategoryTheory.Functor C D<VAR>S : CategoryTheory.Subgroupoid D<VAR>Sn : S.IsNormal<GOAL>(CategoryTheory.Subgroupoid.comap φ S).IsNormal
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>D : Type u_1<VAR>CategoryTheory.Groupoid D<VAR>φ : CategoryTheory.Functor C D<VAR>E : Type u_2<VAR>CategoryTheory.Groupoid E<VAR>ψ : CategoryTheory.Functor D E<GOAL>CategoryTheory.Subgroupoid.comap (φ.comp ψ) = CategoryTheory.Subgroupoid.comap φ ∘ CategoryTheory.Subgroupoid.comap ψ
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>D : Type u_1<VAR>CategoryTheory.Groupoid D<VAR>φ : CategoryTheory.Functor C D<VAR>c d : C<VAR>f : c ⟶ d<GOAL>f ∈ (CategoryTheory.Subgroupoid.ker φ).arrows c d ↔ ∃ (h : φ.obj c = φ.obj d), φ.map f = CategoryTheory.eqToHom h
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>D : Type u_1<VAR>CategoryTheory.Groupoid D<VAR>φ : CategoryTheory.Functor C D<GOAL>(CategoryTheory.Subgroupoid.ker φ).IsNormal
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>D : Type u_1<VAR>CategoryTheory.Groupoid D<VAR>φ : CategoryTheory.Functor C D<VAR>E : Type u_2<VAR>CategoryTheory.Groupoid E<VAR>ψ : CategoryTheory.Functor D E<GOAL>CategoryTheory.Subgroupoid.ker (φ.comp ψ) = CategoryTheory.Subgroupoid.comap φ (CategoryTheory.Subgroupoid.ker ψ)
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>D : Type u_1<VAR>CategoryTheory.Groupoid D<VAR>φ : CategoryTheory.Functor C D<VAR>hφ : Function.Injective φ.obj<VAR>S : CategoryTheory.Subgroupoid C<VAR>c d : D<VAR>f : c ⟶ d<GOAL>CategoryTheory.Subgroupoid.Map.Arrows φ hφ S c d f ↔ ∃ a b g, ∃ (ha : φ.obj a = c) (hb : φ.obj b = d) (_ : g ∈ S.arrows a b), f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (φ.map g) (CategoryTheory.eqToHom hb))
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>D : Type u_1<VAR>CategoryTheory.Groupoid D<VAR>φ : CategoryTheory.Functor C D<VAR>hφ : Function.Injective φ.obj<VAR>S : CategoryTheory.Subgroupoid C<VAR>c d : D<VAR>f : c ⟶ d<GOAL>f ∈ (CategoryTheory.Subgroupoid.map φ hφ S).arrows c d ↔ ∃ a b g, ∃ (ha : φ.obj a = c) (hb : φ.obj b = d) (_ : g ∈ S.arrows a b), f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (φ.map g) (CategoryTheory.eqToHom hb))
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>D : Type u_1<VAR>CategoryTheory.Groupoid D<VAR>φ : CategoryTheory.Functor C D<VAR>hφ : Function.Injective φ.obj<GOAL>GaloisConnection (CategoryTheory.Subgroupoid.map φ hφ) (CategoryTheory.Subgroupoid.comap φ)
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>D : Type u_1<VAR>CategoryTheory.Groupoid D<VAR>φ : CategoryTheory.Functor C D<VAR>hφ : Function.Injective φ.obj<VAR>S T : CategoryTheory.Subgroupoid C<GOAL>S ≤ T → CategoryTheory.Subgroupoid.map φ hφ S ≤ CategoryTheory.Subgroupoid.map φ hφ T
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>D : Type u_1<VAR>CategoryTheory.Groupoid D<VAR>φ : CategoryTheory.Functor C D<VAR>hφ : Function.Injective φ.obj<VAR>S : CategoryTheory.Subgroupoid C<GOAL>S ≤ CategoryTheory.Subgroupoid.comap φ (CategoryTheory.Subgroupoid.map φ hφ S)
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>D : Type u_1<VAR>CategoryTheory.Groupoid D<VAR>φ : CategoryTheory.Functor C D<VAR>hφ : Function.Injective φ.obj<VAR>T : CategoryTheory.Subgroupoid D<GOAL>CategoryTheory.Subgroupoid.map φ hφ (CategoryTheory.Subgroupoid.comap φ T) ≤ T
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>D : Type u_1<VAR>CategoryTheory.Groupoid D<VAR>φ : CategoryTheory.Functor C D<VAR>hφ : Function.Injective φ.obj<VAR>S : CategoryTheory.Subgroupoid C<VAR>T : CategoryTheory.Subgroupoid D<GOAL>CategoryTheory.Subgroupoid.map φ hφ S ≤ T ↔ S ≤ CategoryTheory.Subgroupoid.comap φ T
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>S : CategoryTheory.Subgroupoid C<VAR>D : Type u_1<VAR>CategoryTheory.Groupoid D<VAR>φ : CategoryTheory.Functor C D<VAR>hφ : Function.Injective φ.obj<VAR>d : D<GOAL>d ∈ (CategoryTheory.Subgroupoid.map φ hφ S).objs ↔ ∃ c ∈ S.objs, φ.obj c = d
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>S : CategoryTheory.Subgroupoid C<VAR>D : Type u_1<VAR>CategoryTheory.Groupoid D<VAR>φ : CategoryTheory.Functor C D<VAR>hφ : Function.Injective φ.obj<GOAL>(CategoryTheory.Subgroupoid.map φ hφ S).objs = φ.obj '' S.objs
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>D : Type u_1<VAR>CategoryTheory.Groupoid D<VAR>φ : CategoryTheory.Functor C D<VAR>hφ : Function.Injective φ.obj<VAR>c d : D<VAR>f : c ⟶ d<GOAL>f ∈ (CategoryTheory.Subgroupoid.im φ hφ).arrows c d ↔ ∃ a b g, ∃ (ha : φ.obj a = c) (hb : φ.obj b = d), f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (φ.map g) (CategoryTheory.eqToHom hb))
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>D : Type u_1<VAR>CategoryTheory.Groupoid D<VAR>φ : CategoryTheory.Functor C D<VAR>hφ : Function.Injective φ.obj<VAR>d : D<GOAL>d ∈ (CategoryTheory.Subgroupoid.im φ hφ).objs ↔ ∃ c, φ.obj c = d
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>D : Type u_1<VAR>CategoryTheory.Groupoid D<VAR>φ : CategoryTheory.Functor C D<VAR>hφ : Function.Injective φ.obj<VAR>hφ' : CategoryTheory.Subgroupoid.im φ hφ = ⊤<GOAL>Function.Surjective φ.obj
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>S : CategoryTheory.Subgroupoid C<VAR>D : Type u_1<VAR>CategoryTheory.Groupoid D<VAR>φ : CategoryTheory.Functor C D<VAR>hφ : Function.Injective φ.obj<VAR>hφ' : CategoryTheory.Subgroupoid.im φ hφ = ⊤<VAR>Sn : S.IsNormal<GOAL>(CategoryTheory.Subgroupoid.map φ hφ S).IsNormal
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>S : CategoryTheory.Subgroupoid C<GOAL>S.IsThin ↔ ∀ (c : ↑S.objs), Subsingleton ↑(S.arrows ↑c ↑c)
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>S : CategoryTheory.Subgroupoid C<GOAL>S.IsTotallyDisconnected ↔ ∀ (c d : C), (S.arrows c d).Nonempty → c = d
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>S : CategoryTheory.Subgroupoid C<GOAL>S.disconnect ≤ S
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>S : CategoryTheory.Subgroupoid C<VAR>Sn : S.IsNormal<GOAL>S.disconnect.IsNormal
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>S : CategoryTheory.Subgroupoid C<VAR>c : C<GOAL>c ∈ S.disconnect.objs ↔ c ∈ S.objs
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>S : CategoryTheory.Subgroupoid C<GOAL>S.disconnect.objs = S.objs
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>S : CategoryTheory.Subgroupoid C<GOAL>S.disconnect.IsTotallyDisconnected
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>D : Set C<GOAL>(CategoryTheory.Subgroupoid.full D).objs = D
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>D : Set C<VAR>c d : C<VAR>f : c ⟶ d<GOAL>f ∈ (CategoryTheory.Subgroupoid.full D).arrows c d ↔ c ∈ D ∧ d ∈ D
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>D : Set C<VAR>c : C<GOAL>c ∈ (CategoryTheory.Subgroupoid.full D).objs ↔ c ∈ D
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<GOAL>CategoryTheory.Subgroupoid.full ∅ = ⊥
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<GOAL>CategoryTheory.Subgroupoid.full Set.univ = ⊤
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>D E : Set C<VAR>h : D ≤ E<GOAL>CategoryTheory.Subgroupoid.full D ≤ CategoryTheory.Subgroupoid.full E
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>D : Set C<VAR>c d : ↑(CategoryTheory.Subgroupoid.full D).objs<VAR>f g : c ⟶ d<GOAL>f = g ↔ ↑f = ↑g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>Z : C<VAR>self : CategoryTheory.ProjectiveResolution Z<GOAL>QuasiIso self.π
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>Z : C<VAR>self : CategoryTheory.ProjectiveResolution Z<VAR>i : ℕ<GOAL>HomologicalComplex.HasHomology self.complex i
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>Z : C<VAR>self : CategoryTheory.ProjectiveResolution Z<VAR>n : ℕ<GOAL>CategoryTheory.Projective (self.complex.X n)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>Z : C<VAR>self : CategoryTheory.HasProjectiveResolution Z<GOAL>Nonempty (CategoryTheory.ProjectiveResolution Z)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>self : CategoryTheory.HasProjectiveResolutions C<VAR>Z : C<GOAL>CategoryTheory.HasProjectiveResolution Z
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>Z : C<VAR>P : CategoryTheory.ProjectiveResolution Z<VAR>n : ℕ<GOAL>HomologicalComplex.ExactAt P.complex (n + 1)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>Z : C<VAR>P : CategoryTheory.ProjectiveResolution Z<VAR>n : ℕ<GOAL>(CategoryTheory.ShortComplex.mk (P.complex.d (n + 2) (n + 1)) (P.complex.d (n + 1) n) ⋯).Exact
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>Z : C<VAR>P : CategoryTheory.ProjectiveResolution Z<VAR>n : ℕ<GOAL>P.π.f (n + 1) = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>Z : C<VAR>P : CategoryTheory.ProjectiveResolution Z<GOAL>CategoryTheory.CategoryStruct.comp (P.complex.d 1 0) (P.π.f 0) = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>Z : C<VAR>P : CategoryTheory.ProjectiveResolution Z<VAR>n : ℕ<GOAL>CategoryTheory.CategoryStruct.comp (P.complex.d n (n + 1)) (P.complex.d (n + 1) (n + 2)) = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>Z : C<VAR>CategoryTheory.Projective Z<GOAL>(CategoryTheory.ProjectiveResolution.self Z).π = CategoryTheory.CategoryStruct.id ((ChainComplex.single₀ C).obj Z)