4.24 Adjoint functors to 4.43 Monoidal categories

Section4.24 Adjoint functors#

Section 4.24 of the Stacks Project, Tag 0036. 9 tags here are carried by 2 declarations of the repository (all in StacksCore) and 16 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0037, a definition

Tag 0037 in the Stacks Project.

Declarations registered for the tag:

Tag 0A8B, a lemma

Tag 0A8B in the Stacks Project.

Declarations registered for the tag:

Tag 0FWV, a lemma

Tag 0FWV in the Stacks Project.

CategoryTheory.Adjunction.fullyFaithfulLeftOfComp, a def in StacksCore (human-reviewed), declared in StacksCore/CategoryTheory/AdjointFunctors.lean, line 22. The attribute's comment: “Case 1”.

Given an adjunction L ⊣ R, if L ⋙ R is fully faithful L is too.

def Adjunction.fullyFaithfulLeftOfComp {C D : Type*} [Category C] [Category D]
    {L : C ⥤ D} {R : D ⥤ C} (adj : L ⊣ R) (h : (L ⋙ R).FullyFaithful) : L.FullyFaithful

CategoryTheory.Adjunction.fullyFaithfulRightOfComp, a def in StacksCore (human-reviewed), declared in StacksCore/CategoryTheory/AdjointFunctors.lean, line 32. The attribute's comment: “Case 2”.

Given an adjunction L ⊣ R, if R ⋙ L is fully faithful R is too.

def Adjunction.fullyFaithfulRightOfComp {C D : Type*} [Category C] [Category D]
    {L : C ⥤ D} {R : D ⥤ C} (adj : L ⊣ R) (h : (R ⋙ L).FullyFaithful) : R.FullyFaithful
Tag 07RB, a lemma

Tag 07RB in the Stacks Project.

Declarations registered for the tag:

Tag 0038, a lemma

Tag 0038 in the Stacks Project.

Declarations registered for the tag:

Tag 0039, a lemma

Tag 0039 in the Stacks Project.

Declarations registered for the tag:

Tag 0GLL, a lemma

Tag 0GLL in the Stacks Project.

Declarations registered for the tag:

Tag 0B65, a lemma

Tag 0B65 in the Stacks Project.

Declarations registered for the tag:

Tag 0DV0, a lemma

Tag 0DV0 in the Stacks Project.

Declarations registered for the tag:

Sources
LeanAdjunction.mkOfHomEquiv · isLeftAdjoint_of_rightAdjointObjIsDefined_eq_top · CategoryTheory.Adjunction.fullyFaithfulLeftOfComp · CategoryTheory.Adjunction.fullyFaithfulRightOfComp · Adjunction.fullyFaithfulLOfCompIsoId · Adjunction.unit_isIso_of_L_fully_faithful · Adjunction.fullyFaithfulLOfIsIsoUnit · Adjunction.fullyFaithfulROfCompIsoId

Section4.25 A criterion for representability#

Section 4.25 of the Stacks Project, Tag 0AHM. 3 tags here are carried by 4 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0AHN, a lemma

Tag 0AHN in the Stacks Project.

CategoryTheory.isCorepresentable_of_solutionSet, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Representable/SolutionSet.lean, line 273. References: SGA 4 I (8.12.8.1), “Sufficiency direction”.

Stacks 0AHN (Brown representability criterion).

Let C be a category with all (small) limits and F : C ⥤ Type v a functor that preserves limits. Suppose there is a family {xᵢ} of objects together with elements fᵢ ∈ F xᵢ such that for every y : C and every g ∈ F y there exists an i and a morphism φ : xᵢ ⟶ y with F.map φ fᵢ = g. Then F is corepresentable.

theorem isCorepresentable_of_solutionSet
    {C : Type u} [Category.{v} C] [HasLimitsOfSize.{v, v} C]
    (F : C ⥤ Type v) [PreservesLimitsOfSize.{v, v} F]
    {I : Type v} (x : I → C) (f : ∀ i, F.obj (x i))
    (hsurj : ∀ (y : C) (g : F.obj y), ∃ i, ∃ φ : x i ⟶ y, F.map φ (f i) = g) :
    F.IsCorepresentable
Tag 0AHP, a remark

Tag 0AHP in the Stacks Project.

CategoryTheory.bijective_comp_freeGroup_of, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Representable/Applications.lean, line 56. The attribute's comment: “the free group on a set”.

Stacks 0AHP, the free group on a set. The free group on E represents the functor G ↦ Map(E, G) on groups: composing a group homomorphism F_E → G with the canonical map FreeGroup.of : E → F_E is a bijection from Mor_{Groups}(F_E, G) to Map(E, G).

theorem bijective_comp_freeGroup_of (E : Type u) (G : Type v) [Group G] :
    Function.Bijective fun f : FreeGroup E →* G => (f : FreeGroup E → G) ∘ FreeGroup.of

CategoryTheory.closure_range_freeGroup_of, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Representable/Applications.lean, line 63. The attribute's comment: “the free group on a set”.

Stacks 0AHP, the free group on a set: the map E → F_E corresponding to the identity of F_E generates F_E, so no relations have been imposed.

theorem closure_range_freeGroup_of (E : Type u) :
    Subgroup.closure (Set.range (FreeGroup.of : E → FreeGroup E)) = ⊤

CategoryTheory.colimitHomEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Representable/Applications.lean, line 74. The attribute's comment: “colimits of topological spaces”.

Stacks 0AHP, colimits of topological spaces. For a diagram X : 𝓘 ⥤ Top of topological spaces, a morphism out of the colimit of X is the same thing as an element of lim_𝓘 Mor_{Top}(X_i, Y), i.e. a family of morphisms φ_i : X_i ⟶ Y compatible with the transition maps of the diagram. So the colimit — which exists because Top has limits and the criterion of Stacks 0AHN applies — is precisely a space representing the functor Y ↦ lim_𝓘 Mor_{Top}(X_i, Y) of the source.

noncomputable def colimitHomEquiv {𝓘 : Type u} [SmallCategory 𝓘] (X : 𝓘 ⥤ TopCat.{u})
    (Y : TopCat.{u}) :
    (colimit X ⟶ Y) ≃ (X ⟶ (Functor.const 𝓘).obj Y)
Tag 0AHQ, a theorem

Tag 0AHQ in the Stacks Project.

Declarations registered for the tag:

Sources
LeanCategoryTheory.isCorepresentable_of_solutionSet · CategoryTheory.bijective_comp_freeGroup_of · CategoryTheory.closure_range_freeGroup_of · CategoryTheory.colimitHomEquiv · isRightAdjoint_of_preservesLimits_of_solutionSetCondition

Section4.26 Categorically compact objects#

Section 4.26 of the Stacks Project, Tag 0FWW. 2 tags here are carried by 2 declarations of the repository (all in StacksFrontier) and 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0FWX, a definition

Tag 0FWX in the Stacks Project.

Declarations registered for the tag:

Tag 0FWY, a lemma

Tag 0FWY in the Stacks Project.

CategoryTheory.ObjectProperty.exists_extension_of_preservesFilteredColimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/KanExtension/Extend.lean, line 60. References: SGA 4 I (8.7.2), “existence of f̄”; SGA 4 I (8.7.3), “ess. surj. of (8.7.3.1)”.

Stacks 0FWY (existence). Let C and D have w-filtered colimits, let P be a property of objects of C cutting out an essentially w-small full subcategory of categorically compact objects (Stacks 0FWX), and assume every object of C is a w-filtered colimit of objects satisfying P. Then every functor F' out of that subcategory extends to a functor C ⥤ D commuting with filtered colimits.

theorem exists_extension_of_preservesFilteredColimits
    [HasFilteredColimitsOfSize.{w, w} C] [HasFilteredColimitsOfSize.{w, w} D]
    [EssentiallySmall.{w} P.FullSubcategory]
    (hP : P ≤ isFinitelyPresentable.{w} C) (hgen : ∀ X : C, P.ind.{w} X)
    (F' : P.FullSubcategory ⥤ D) :
    ∃ F : C ⥤ D, PreservesFilteredColimitsOfSize.{w, w} F ∧ Nonempty (P.ι ⋙ F ≅ F')

CategoryTheory.ObjectProperty.existsUnique_iso_of_preservesFilteredColimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/KanExtension/Extend.lean, line 80. References: SGA 4 I (8.7.2), “uniqueness of f̄”; SGA 4 I (8.7.3), “uniqueness of extension”.

Stacks 0FWY (uniqueness). Under the hypotheses of exists_extension_of_preservesFilteredColimits, an extension of F' commuting with filtered colimits is unique up to a unique natural isomorphism compatible with the identifications of the restrictions with F'.

theorem existsUnique_iso_of_preservesFilteredColimits
    [HasFilteredColimitsOfSize.{w, w} C] [EssentiallySmall.{w} P.FullSubcategory]
    (hP : P ≤ isFinitelyPresentable.{w} C) (hgen : ∀ X : C, P.ind.{w} X)
    {F' : P.FullSubcategory ⥤ D} (F₁ F₂ : C ⥤ D)
    [PreservesFilteredColimitsOfSize.{w, w} F₁] [PreservesFilteredColimitsOfSize.{w, w} F₂]
    (e₁ : P.ι ⋙ F₁ ≅ F') (e₂ : P.ι ⋙ F₂ ≅ F') :
    ∃! φ : F₁ ≅ F₂, Functor.whiskerLeft P.ι φ.hom = (e₁ ≪≫ e₂.symm).hom
Sources
LeanIsFinitelyPresentable · CategoryTheory.isFinitelyPresentable_iff_preservesFilteredColimits · CategoryTheory.ObjectProperty.exists_extension_of_preservesFilteredColimits · CategoryTheory.ObjectProperty.existsUnique_iso_of_preservesFilteredColimits

Section4.27 Localization in categories#

Section 4.27 of the Stacks Project, Tag 04VB. 20 tags here are carried by 25 declarations of the repository (all in StacksFrontier) and 19 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 04VC, a definition

Tag 04VC in the Stacks Project.

Declarations registered for the tag:

Tag 04VD, a lemma

Tag 04VD in the Stacks Project.

Declarations registered for the tag:

Tag 0BM2, a definition

Tag 0BM2 in the Stacks Project.

Declarations registered for the tag:

Tag 04VE, a lemma

Tag 04VE in the Stacks Project.

CategoryTheory.Localization.exists_common_leftFraction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Localization/LeftFraction/CommonDenominator.lean, line 141.

Stacks 04VE. Let W : MorphismProperty C have left calculus of fractions and let L be a localisation functor for W. For any finite family g : ∀ i, L.obj (X i) ⟶ L.obj Y, there exist a common target Y' : C, a morphism s : Y ⟶ Y' with W s, and a family f : ∀ i, X i ⟶ Y' such that each g i equals L.map (f i) ≫ (Localization.isoOfHom L W s _).inv.

theorem exists_common_leftFraction
    {C : Type u} [Category.{v} C] {W : MorphismProperty C}
    {D : Type*} [Category D] (L : C ⥤ D) [L.IsLocalization W]
    [W.HasLeftCalculusOfFractions]
    {ι : Type*} [Finite ι]
    {X : ι → C} {Y : C}
    (g : ∀ i, L.obj (X i) ⟶ L.obj Y) :
    ∃ (Y' : C) (s : Y ⟶ Y') (hs : W s) (f : ∀ i, X i ⟶ Y'),
      ∀ i, g i = L.map (f i) ≫ (Localization.isoOfHom L W s hs).inv
Tag 04VF, a lemma

Tag 04VF in the Stacks Project.

map_eq_iff_leftFractionRel, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Localization/LeftFraction/Equality.lean, line 55.

Stacks 04VF. For a left multiplicative system W on C and a localization functor L : C ⥤ D at W, two left fractions φ ψ : X ⟶ Y have the same image in D if and only if LeftFractionRel φ ψ, i.e. if and only if they agree after postcomposition with a suitable morphism of W.

theorem map_eq_iff_leftFractionRel {C D : Type*} [Category C] [Category D] (L : C ⥤ D)
    {W : MorphismProperty C} [W.HasLeftCalculusOfFractions] [L.IsLocalization W]
    {X Y : C} (φ ψ : W.LeftFraction X Y) :
    φ.map L (Localization.inverts _ _) = ψ.map L (Localization.inverts _ _) ↔
      LeftFractionRel φ ψ
Tag 05Q0, a remark

Tag 05Q0 in the Stacks Project.

CategoryTheory.MorphismProperty.isColimitUnderHomCocone, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Localization/LeftFraction/HomAsColimit.lean, line 128. The attribute's comment: “the displayed formula 05Q1: the morphisms X ⟶ Y of the localization are the filtered colimit of the sets Mor_C(X, Y') over the objects (s : Y ⟶ Y') of Y/S, at the tautological cocone whose leg at s sends f to the left fraction s⁻¹ f”. References: SGA 4 VI (6.5).

Morphisms of W⁻¹C as a colimit over Y/S: for a left multiplicative system W on C, a localization functor L : C ⥤ D of C at W and objects X, Y of C, the morphisms L.obj X ⟶ L.obj Y of W⁻¹C are the colimit colim_{(s : Y ⟶ Y') ∈ Y/S} Mor_C(X, Y'), in the sense that the tautological cocone underHomCocone, whose leg at s sends f to the left fraction s⁻¹ f, is a colimit cocone. The index category Y/S is filtered by MorphismProperty.isFiltered_under_of_hasLeftCalculusOfFractions, so this exhibits the morphisms of W⁻¹C as a filtered colimit of morphisms of C.

noncomputable def isColimitUnderHomCocone (X Y : C) : IsColimit (W.underHomCocone L X Y)
Tag 04VG, a lemma

Tag 04VG in the Stacks Project.

Declarations registered for the tag:

Tag 05Q2, a lemma

Tag 05Q2 in the Stacks Project.

CategoryTheory.MorphismProperty.Q_preservesFiniteColimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Localization/LeftFraction/Commutation.lean, line 53. References: SGA 5 V (2.3.4), “first assertion”.

Stacks 05Q2. For a left multiplicative system W on C, the localization functor Q : C ⥤ W⁻¹C commutes with finite colimits. This does not assert that W⁻¹C has finite colimits: only that Q carries a finite colimit cocone of C to a colimit cocone.

theorem Q_preservesFiniteColimits
    {C : Type*} [Category C] (W : MorphismProperty C) [W.HasLeftCalculusOfFractions] :
    Limits.PreservesFiniteColimits W.Q
Tag 05Q3, a lemma

Tag 05Q3 in the Stacks Project.

CategoryTheory.MorphismProperty.exists_leftFraction_lift_of_commSq, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Localization/LeftFraction/LiftSquare.lean, line 116.

Stacks 05Q3. A commutative square in the left localisation W⁻¹C between images of morphisms f : X ⟶ Y and f' : X' ⟶ Y' of C lifts to a commutative diagram in C involving two morphisms in W.

lemma exists_leftFraction_lift_of_commSq
    {X Y X' Y' : C} (f : X ⟶ Y) (f' : X' ⟶ Y')
    (a : (LeftFraction.Localization.Q W).obj X ⟶ (LeftFraction.Localization.Q W).obj X')
    (b : (LeftFraction.Localization.Q W).obj Y ⟶ (LeftFraction.Localization.Q W).obj Y')
    (sq : (LeftFraction.Localization.Q W).map f ≫ b =
      a ≫ (LeftFraction.Localization.Q W).map f') :
    ∃ (X'' Y'' : C) (g : X ⟶ X'') (s : X' ⟶ X'') (hs : W s)
      (h : Y ⟶ Y'') (t : Y' ⟶ Y'') (ht : W t) (f'' : X'' ⟶ Y''),
      f ≫ h = g ≫ f'' ∧ s ≫ f'' = f' ≫ t ∧
      a = (LeftFraction.mk g s hs).map (LeftFraction.Localization.Q W)
            (Localization.inverts _ _) ∧
      b = (LeftFraction.mk h t ht).map (LeftFraction.Localization.Q W)
            (Localization.inverts _ _)
Tag 04VH, a lemma

Tag 04VH in the Stacks Project.

CategoryTheory.MorphismProperty.RightFraction.comp_rel_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Localization/RightFraction/Defs.lean, line 174. The attribute's comment: “(2)”. References: SGA 4 VI (6.5), “6.5 c)”.

Stacks 04VH (2). The canonical composition of representatives respects the equivalence relation in both arguments. Combined with RightFraction.comp_rel_compOfOre, which identifies it with the composition along an arbitrary Ore square, this is well-definedness of composition on the quotient.

theorem RightFraction.comp_rel_comp [W.HasRightCalculusOfFractions] {X Y Z : C}
    {φ φ' : W.RightFraction X Y} {ψ ψ' : W.RightFraction Y Z} (hφ : RightFractionRel φ φ')
    (hψ : RightFractionRel ψ ψ') :
    RightFractionRel (RightFraction.comp W φ ψ) (RightFraction.comp W φ' ψ')

CategoryTheory.MorphismProperty.RightLocalization.category, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Localization/RightFraction/Defs.lean, line 272. The attribute's comment: “(3)”. References: SGA 4 VI (6.5).

Stacks 04VH (3). The objects of the right-fractions model W⁻¹C are the objects of C, the hom-sets are RightLocalization.Hom W X Y, identities are RightLocalization.Hom.id W X, and composition is RightLocalization.Hom.comp W. The category axioms are RightLocalization.Hom.id_comp, .comp_id and .assoc.

noncomputable instance RightLocalization.category [W.HasRightCalculusOfFractions] :
    Category (RightLocalization W)

Declarations registered for the tag:

Tag 0BM3, a definition

Tag 0BM3 in the Stacks Project.

RightLocalizationAsFraction.fInvS, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Localization/RightFraction/Morphism.lean, line 69.

Given a morphism f : X' ⟶ Y and a morphism s : X' ⟶ X with s ∈ W (where W is a right multiplicative system, i.e. has a right calculus of fractions), the morphism f s⁻¹ : X ⟶ Y in the localized category S⁻¹C = W.Localization.

Concretely, this is the image under W.Q of the pair (f, s), which represents the equivalence class of (f, s) under RightFractionRel.

noncomputable def fInvS [W.HasRightCalculusOfFractions]
    {X Y X' : C} (f : X' ⟶ Y) (s : X' ⟶ X) (hs : W s) :
    W.Q.obj X ⟶ W.Q.obj Y
Tag 04VI, a lemma

Tag 04VI in the Stacks Project.

CategoryTheory.Localization.exists_common_rightFraction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Localization/RightFraction/CommonDenominator.lean, line 169. References: SGA 4½ Etat 0 (2.3.2), “partial”.

Stacks 04VI (common right denominator).

Let W : MorphismProperty C admit a right calculus of fractions. Given a finite family of morphisms g i : W.Q.obj X ⟶ W.Q.obj (Y i) in the localization with common source W.Q.obj X, there exist an object X' of C, a morphism s : X' ⟶ X in W, and a family f i : X' ⟶ Y i in C such that each g i is represented by the right fraction (s, f i).

theorem exists_common_rightFraction
    (W : MorphismProperty C) [W.HasRightCalculusOfFractions]
    {ι : Type*} [Finite ι] {X : C} {Y : ι → C}
    (g : ∀ i, W.Q.obj X ⟶ W.Q.obj (Y i)) :
    ∃ (X' : C) (s : X' ⟶ X) (hs : W s) (f : ∀ i, X' ⟶ Y i),
      ∀ i, g i = (MorphismProperty.RightFraction.mk s hs (f i)).map
        W.Q (Localization.inverts _ W)
Tag 04VJ, a lemma

Tag 04VJ in the Stacks Project.

map_eq_iff_rightFractionRel, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Localization/RightFraction/Equality.lean, line 55.

Stacks 04VJ. For a right multiplicative system W on C and a localization functor L : C ⥤ D at W, two right fractions φ ψ : X ⟶ Y have the same image in D if and only if RightFractionRel φ ψ, i.e. if and only if they agree after precomposition with a suitable morphism of W.

theorem map_eq_iff_rightFractionRel {C D : Type*} [Category C] [Category D] (L : C ⥤ D)
    {W : MorphismProperty C} [W.HasRightCalculusOfFractions] [L.IsLocalization W]
    {X Y : C} (φ ψ : W.RightFraction X Y) :
    φ.map L (Localization.inverts _ _) = ψ.map L (Localization.inverts _ _) ↔
      RightFractionRel φ ψ
Tag 05Q4, a remark

Tag 05Q4 in the Stacks Project.

CategoryTheory.MorphismProperty.isCofiltered_over, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Localization/LeftFraction/AsColimit.lean, line 66.

Stacks 05Q4, first claim: for a right multiplicative system W on C and an object X of C, the category S/X = W.Over ⊤ X of W-morphisms to X is cofiltered in the sense of Stacks 04AZ, i.e. its identity diagram is a cofiltered diagram.

theorem isCofiltered_over (X : C) : (𝟭 (W.Over ⊤ X)).IsCofiltered

CategoryTheory.MorphismProperty.isColimitOverHomCocone, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Localization/LeftFraction/AsColimit.lean, line 147. References: SGA 4½ Etat 0 (2.3.2); SGA 5 V (2.3.3), “Hom-set clause”.

Stacks 05Q4, second claim: for a right multiplicative system W on C, a localization functor L : C ⥤ D of C at W and objects X, Y of C, the morphisms L.obj X ⟶ L.obj Y of W⁻¹C are the colimit colim_{(s : X' ⟶ X) ∈ (S/X)ᵒᵖ} Mor_C(X', Y), in the sense that the tautological cocone overHomCocone, whose leg at s sends f to the right fraction f s⁻¹, is a colimit cocone. The index category (S/X)ᵒᵖ is filtered by isCofiltered_over, so this exhibits the morphisms of W⁻¹C as a filtered colimit of morphisms of C.

noncomputable def isColimitOverHomCocone (X Y : C) : IsColimit (W.overHomCocone L X Y)
Tag 04VK, a lemma

Tag 04VK in the Stacks Project.

Q04VK, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Localization/UniversalProperty.lean, line 64. The attribute's comment: “(1)”. References: SGA 5 V (2.3), “functor p : E → E(S⁻¹)”; SGA 4½ Etat 0 (2.3.1).

The canonical localization functor Q04VK : 𝓒 ⥤ S⁻¹𝓒 (Stacks Tag 04VK (1)). This is the Mathlib functor LeftFraction.Localization.Q.

noncomputable def Q04VK : 𝓒 ⥤ LeftFraction.Localization S

Q_isIso_of_mem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Localization/UniversalProperty.lean, line 81. The attribute's comment: “(2)”.

Stacks 04VK (2): For any s ∈ S the morphism Q04VK(s) is an isomorphism in S⁻¹𝓒.

theorem Q_isIso_of_mem {X Y : 𝓒} (s : X ⟶ Y) (hs : S s) :
    IsIso ((Q04VK S).map s)

exists_unique_lift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Localization/UniversalProperty.lean, line 92. The attribute's comment: “(3)”. References: SGA 5 V (2.3), “left calc. of fractions”; SGA 4½ Etat 0 (2.3.1), “partial”; SGA 4½ Etat 0 (Problem2), “partial”.

Stacks 04VK (3) — combined statement: for any functor G : 𝓒 ⥤ 𝓓 inverting S, there exists a unique functor H : S⁻¹𝓒 ⥤ 𝓓 such that H ∘ Q04VK = G.

theorem exists_unique_lift (G : 𝓒 ⥤ 𝓓) (hG : S.IsInvertedBy G) :
    ∃! H : LeftFraction.Localization S ⥤ 𝓓, (Q04VK S) ⋙ H = G

Declarations registered for the tag:

Tag 05Q6, a lemma

Tag 05Q6 in the Stacks Project.

CategoryTheory.MorphismProperty.Q_preservesFiniteLimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Localization/RightFraction/Commutation.lean, line 354.

Stacks 05Q6. For a right multiplicative system W on C, the localization functor Q : C ⥤ W⁻¹C commutes with finite limits. This does not assert that W⁻¹C has finite limits: only that Q carries a finite limit cone of C to a limit cone.

theorem Q_preservesFiniteLimits
    {C : Type*} [Category C] (W : MorphismProperty C)
    [W.HasRightCalculusOfFractions] :
    PreservesFiniteLimits W.Q
Tag 05Q7, a lemma

Tag 05Q7 in the Stacks Project.

CategoryTheory.MorphismProperty.exists_rightFraction_lift_of_commSq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Localization/RightFraction/LiftSquare.lean, line 59.

Stacks 05Q7. Let W : MorphismProperty C admit a right calculus of fractions and let L : C ⥤ D be a localization of C at W. Given morphisms f : X ⟶ Y and f' : X' ⟶ Y' in C, and morphisms a : L.obj X ⟶ L.obj X', b : L.obj Y ⟶ L.obj Y' in D such that a ≫ L.map f' = L.map f ≫ b, there exist objects X'', Y'' in C, a morphism f'' : X'' ⟶ Y'', morphisms s : X'' ⟶ X, t : Y'' ⟶ Y with W s, W t, and morphisms g : X'' ⟶ X', h : Y'' ⟶ Y' such that s ≫ f = f'' ≫ t, g ≫ f' = f'' ≫ h, L.map s ≫ a = L.map g, and L.map t ≫ b = L.map h.

theorem exists_rightFraction_lift_of_commSq
    [L.IsLocalization W] [HasRightCalculusOfFractions W]
    {X Y X' Y' : C} (f : X ⟶ Y) (f' : X' ⟶ Y')
    (a : L.obj X ⟶ L.obj X') (b : L.obj Y ⟶ L.obj Y')
    (sq : a ≫ L.map f' = L.map f ≫ b) :
    ∃ (X'' Y'' : C) (f'' : X'' ⟶ Y'')
      (s : X'' ⟶ X) (_ : W s) (t : Y'' ⟶ Y) (_ : W t)
      (g : X'' ⟶ X') (h : Y'' ⟶ Y'),
        s ≫ f = f'' ≫ t ∧ g ≫ f' = f'' ≫ h ∧
        L.map s ≫ a = L.map g ∧
        L.map t ≫ b = L.map h
Tag 04VL, a lemma

Tag 04VL in the Stacks Project.

CategoryTheory.MorphismProperty.leftFractionEquivRightFraction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Localization/Comparison.lean, line 68. References: SGA 4½ Etat 0 (2.3.1), “partial”.

Stacks 04VL. The category of left fractions LeftFraction.Localization W and the category of right fractions (LeftFraction.Localization W.op)ᵒᵖ of C at the multiplicative system W are canonically equivalent. The equivalence is the one induced by the universal property of the localisation: both LeftFraction.Localization.Q W and rightFractionQ W invert exactly W, so Localization.uniq produces the canonical comparison, compatible with the two localisation functors (see compLeftFractionEquivRightFractionFunctor).

noncomputable def leftFractionEquivRightFraction :
    LeftFraction.Localization W ≌ (LeftFraction.Localization W.op)ᵒᵖ

CategoryTheory.MorphismProperty.compLeftFractionEquivRightFractionFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Localization/Comparison.lean, line 76.

Stacks 04VL. The canonical equivalence of 04VL is canonical: it is compatible with the two localisation functors out of C, i.e. it identifies a morphism written as a left fraction with the same morphism written as a right fraction.

noncomputable def compLeftFractionEquivRightFractionFunctor :
    LeftFraction.Localization.Q W ⋙ (leftFractionEquivRightFraction W).functor ≅
      rightFractionQ W
Tag 05Q8, a definition

Tag 05Q8 in the Stacks Project.

CategoryTheory.MorphismProperty.IsSaturated, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Localization/Saturated/Defs.lean, line 49.

W is a saturated multiplicative system when it is a multiplicative system — MS1 together with the two Ore conditions MS2 and the two cancellation conditions MS3, i.e. both a left and a right calculus of fractions — and satisfies MS4: for composable f : X ⟶ Y, g : Y ⟶ Z, h : Z ⟶ T, if W (f ≫ g) and W (g ≫ h) then W g.

structure IsSaturated (W : MorphismProperty C) : Prop
Tag 05Q9, a lemma

Tag 05Q9 in the Stacks Project.

CategoryTheory.MorphismProperty.invertedClosure_eq_satClosure, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Localization/Saturated/Closure.lean, line 172.

Ŝ = S': a morphism becomes invertible in the localization exactly when it has a W-partner on each side.

theorem invertedClosure_eq_satClosure : W.invertedClosure = W.satClosure

CategoryTheory.MorphismProperty.le_invertedClosure, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Localization/Saturated/Closure.lean, line 180.

W ≤ Ŝ: every morphism of W is inverted by Q.

theorem le_invertedClosure : W ≤ W.invertedClosure

CategoryTheory.MorphismProperty.isSaturated_invertedClosure, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Localization/Saturated/Closure.lean, line 255.

Ŝ is itself a saturated multiplicative system: it has a left and a right calculus of fractions and satisfies MS4.

theorem isSaturated_invertedClosure : IsSaturated W.invertedClosure

CategoryTheory.MorphismProperty.invertedClosure_le_of_isSaturated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Localization/Saturated/Closure.lean, line 272.

Ŝ is the smallest saturated multiplicative system containing W: it is contained in every saturated multiplicative system containing W.

theorem invertedClosure_le_of_isSaturated (W' : MorphismProperty C)
    (hW' : IsSaturated W') (hWW' : W ≤ W') : W.invertedClosure ≤ W'

CategoryTheory.MorphismProperty.IsSaturated.invertedClosure_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Localization/Saturated/Closure.lean, line 278.

If W is already saturated then Ŝ = W.

theorem IsSaturated.invertedClosure_eq (hW : IsSaturated W) :
    W.invertedClosure = W
Sources
LeanMorphismProperty.IsMultiplicative · MorphismProperty.HasLeftCalculusOfFractions · MorphismProperty.HasRightCalculusOfFractions · MorphismProperty.LeftFraction · CategoryTheory.MorphismProperty.LeftFractionRel · MorphismProperty.equivalenceLeftFractionRel · MorphismProperty.LeftFraction.comp₀_rel · MorphismProperty.LeftFraction.Localization.Hom.comp_eq

Section4.28 Formal properties#

Section 4.28 of the Stacks Project, Tag 003D. 2 tags here are carried by 1 declaration of the repository (in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 003E, a definition

Tag 003E in the Stacks Project.

Declarations registered for the tag:

Tag 003F, a lemma

Tag 003F in the Stacks Project.

CategoryTheory.NatTrans.horiz_vert_interchange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Bicategory/InterchangeLaw.lean, line 56.

Stacks 003F (interchange law). The horizontal (◫) and vertical (≫) compositions of natural transformations satisfy (t ≫ t') ◫ (s ≫ s') = (t ◫ s) ≫ (t' ◫ s').

theorem horiz_vert_interchange
    {A : Type u₁} {B : Type u₂} {C : Type u₃}
    [Category.{v₁} A] [Category.{v₂} B] [Category.{v₃} C]
    {F F' F'' : A ⥤ B} {G G' G'' : B ⥤ C}
    (t : F ⟶ F') (t' : F' ⟶ F'')
    (s : G ⟶ G') (s' : G' ⟶ G'') :
    (t ≫ t') ◫ (s ≫ s') = (t ◫ s) ≫ (t' ◫ s')
Sources
LeanNatTrans.hcomp · CategoryTheory.NatTrans.horiz_vert_interchange

Section4.29 2-categories#

Section 4.29 of the Stacks Project, Tag 003G. 3 tags here are carried by 7 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 003H, a definition

Tag 003H in the Stacks Project.

Declarations registered for the tag:

Tag 003L, a definition

Tag 003L in the Stacks Project.

Declarations registered for the tag:

Tag 003N, a definition

Tag 003N in the Stacks Project.

Declarations registered for the tag:

Sources
LeanBicategory.Strict · Bicategory.Equivalence · Bicategory.Equivalence.mkOfAdjointifyCounit · Pseudofunctor · StrictBicategory.category · LocallyDiscrete · LocallyDiscrete.mkPseudofunctor

Section4.30 (2, 1)-categories#

Section 4.30 of the Stacks Project, Tag 02X8. 3 tags here are carried by 5 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 003I, a definition

Tag 003I in the Stacks Project.

CategoryTheory.Bicategory.IsTwoOneCategory, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Bicategory/TwoOneCategory.lean, line 57.

A (strict) (2,1)-category is a 2-category — that is, a strict bicategory — in which every 2-morphism is an isomorphism, the latter spelled as Mathlib's Bicategory.IsLocallyGroupoid, i.e. each hom-category a ⟶ b is a groupoid.

def IsTwoOneCategory (B : Type u) [Bicategory.{w, v} B] : Prop
Tag 003K, an example

Tag 003K in the Stacks Project.

CategoryTheory.Bicategory.isTwoOneCategory_pith_cat, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Bicategory/Cat.lean, line 75.

Stacks 003K. The 2-category Cat of categories, functors and morphisms of functors (Stacks 003J) becomes a (2,1)-category once only the isomorphisms of functors are allowed as 2-morphisms. The resulting 2-category is Bicategory.Pith Cat; that its 2-morphisms are precisely the isomorphisms of functors is Pith.homEquivIso.

lemma isTwoOneCategory_pith_cat : IsTwoOneCategory (Pith Cat.{v, u})
Tag 003M, a remark

Tag 003M in the Stacks Project.

CategoryTheory.isTwoOneCategory_pith_catGroupoids, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Bicategory/CatVariants.lean, line 96. The attribute's comment: “the 2-category of groupoids”.

Stacks 003M, the variant for groupoids: the 2-category of groupoids becomes a (2,1)-category once only the isomorphisms of functors are allowed as 2-morphisms.

lemma isTwoOneCategory_pith_catGroupoids :
    IsTwoOneCategory (Pith CatGroupoids.{v₁, u₁})

CategoryTheory.isTwoOneCategory_pith_catFiberedInGroupoids, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Bicategory/CatVariants.lean, line 104. The attribute's comment: “the 2-category of categories fibred in groupoids over a fixed category”.

Stacks 003M, the variant for categories fibred in groupoids over a fixed category: the 2-category of categories fibred in groupoids over 𝒞 (Stacks 02XS) becomes a (2,1)-category once only the isomorphisms of 2-morphisms are kept.

lemma isTwoOneCategory_pith_catFiberedInGroupoids (𝒞 : Type u₁) [Category.{v₁} 𝒞] :
    IsTwoOneCategory (Pith (CatFiberedInGroupoids.{v₁, v₂, u₁, u₂} 𝒞))

CategoryTheory.isTwoOneCategory_pith_basedStack, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Bicategory/CatVariants.lean, line 111. The attribute's comment: “the 2-category of stacks”.

Stacks 003M, the variant for stacks: the 2-category of stacks over a site (Stacks 02ZG) becomes a (2,1)-category once only the isomorphisms of 2-morphisms are kept.

lemma isTwoOneCategory_pith_basedStack (𝒞 : Type u₁) [Category.{v₁} 𝒞]
    (J : GrothendieckTopology 𝒞) :
    IsTwoOneCategory (Pith (BasedStack.{v₁, v₂, u₁, u₂} 𝒞 J))
Sources
LeanCategoryTheory.Bicategory.IsTwoOneCategory · CategoryTheory.Bicategory.isTwoOneCategory_pith_cat · CategoryTheory.isTwoOneCategory_pith_catGroupoids · CategoryTheory.isTwoOneCategory_pith_catFiberedInGroupoids · CategoryTheory.isTwoOneCategory_pith_basedStack

Section4.31 2-fibre products#

Section 4.31 of the Stacks Project, Tag 003O. 15 tags here are carried by 28 declarations of the repository (all in StacksFrontier) and 3 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 003O, the section

Tag 003O in the Stacks Project.

CategoryTheory.Bicategory.TwoCommSq, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoFibreProduct/Defs.lean, line 96.

A 2-commutative cone over the cospan (f, g): an object pt together with 1-morphisms fst : pt ⟶ x, snd : pt ⟶ y and an invertible 2-morphism iso : fst ≫ f ≅ snd ≫ g filling the square.

Stacks 003O. These are the objects of the category of 2-commutative diagrams over the cospan (f, g).

structure TwoCommSq (f : x ⟶ z) (g : y ⟶ z)

CategoryTheory.Bicategory.TwoCommSq.PreHom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoFibreProduct/Defs.lean, line 117.

A pre-morphism of cones T ⟶ S: a 1-morphism hom : T.pt ⟶ S.pt together with invertible comparison 2-cells isoFst : T.fst ≅ hom ≫ S.fst, isoSnd : T.snd ≅ hom ≫ S.snd subject to the Stacks 003O compatibility square.

Stacks 003O. These are the morphisms of the category of 2-commutative diagrams, before passing to classes modulo the 2-cell equivalence TwoCommSq.PreHom.Rel.

structure TwoCommSq.PreHom (T S : TwoCommSq f g)

CategoryTheory.Bicategory.TwoCommSq.category, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoFibreProduct/Defs.lean, line 247.

Stacks 003O. The category of 2-commutative diagrams over the cospan (f, g): objects are the 2-commutative squares, and morphisms are pre-morphisms modulo the 2-cell equivalence, which is what makes composition strictly associative and unital.

instance TwoCommSq.category : Category (TwoCommSq f g)
Tag 003P, a definition

Tag 003P in the Stacks Project.

CategoryTheory.Bicategory.IsBiterminal, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Bicategory/TwoOneCategory.lean, line 67.

A final object of a (2,1)-category B, defined as an object T such that every hom-category X ⟶ T has a terminal object. In a locally groupoidal B this says that every object admits a 1-morphism to T, and any two such are isomorphic by a unique 2-morphism (CategoryTheory.Bicategory.isBiterminal_iff).

def IsBiterminal (T : B) : Prop
Tag 003Q, a definition

Tag 003Q in the Stacks Project.

CategoryTheory.Bicategory.IsTwoFibreProduct, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoFibreProduct/Defs.lean, line 270.

Stacks 003Q. A 2-commutative square P over (f, g) is a 2-fibre product of f and g when it is a terminal (final) object of the category TwoCommSq f g of 2-commutative diagrams. Its fst, snd and iso fields are the projections p, q and the invertible ψ : f ∘ p ⟶ g ∘ q of the source.

abbrev IsTwoFibreProduct (P : TwoCommSq f g) : Type _
Tag 003R, an example

Tag 003R in the Stacks Project.

Declarations registered for the tag:

Tag 02X9, a lemma

Tag 02X9 in the Stacks Project.

CategoryTheory.Cat.isTwoFibreProduct_categoricalPullbackSq, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoFibreProduct/CatCategoricalPullback.lean, line 214. The attribute's comment: “the explicit construction is a 2-fibre product in the sense of Stacks 003Q”.

The explicit 2-fibre product of two functors is a 2-fibre product of them in the bicategory of categories: it is a terminal object of the category of 2-commutative squares over the cospan.

def isTwoFibreProduct_categoricalPullbackSq (F : A ⟶ C) (G : B ⟶ C) :
    IsTwoFibreProduct (categoricalPullbackSq F G)
Tag 06RL, a remark

Tag 06RL in the Stacks Project.

CategoryTheory.Limits.CategoricalPullback.Quintuple, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoFibreProduct/SymmetricModel.lean, line 39.

Stacks 06RL. The symmetric model of the 2-fibre product 𝒜 ×_𝒞 ℬ: an object is a quintuple (A, B, C, a, b) with A : 𝒜, B : ℬ, C : 𝒞 and isomorphisms a : F A ≅ C, b : G B ≅ C.

structure Quintuple

CategoryTheory.Limits.CategoricalPullback.Quintuple.toCategoricalPullback, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoFibreProduct/SymmetricModel.lean, line 90.

Stacks 06RL. The comparison functor from the symmetric model to the standard 2-fibre product: on objects it sends (A, B, C, a, b) to (A, B, a ≪≫ b.symm), whose structural morphism is b⁻¹ ∘ a, and on morphisms it sends (f, g, h) to (f, g).

def toCategoricalPullback : Quintuple F G ⥤ CategoricalPullback F G

CategoryTheory.Limits.CategoricalPullback.Quintuple.isEquivalence_toCategoricalPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoFibreProduct/SymmetricModel.lean, line 165.

Stacks 06RL. The comparison functor from the symmetric quintuple model of the 2-fibre product to the standard model CategoricalPullback F G is an equivalence of categories.

theorem isEquivalence_toCategoricalPullback :
    (toCategoricalPullback (F := F) (G := G)).IsEquivalence
Tag 02XA, a lemma

Tag 02XA in the Stacks Project.

CategoryTheory.Limits.CategoricalPullback.map, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoFibreProduct/Functoriality.lean, line 43.

The functor 𝒳 ×_𝒵 𝒴 ⥤ 𝒜 ×_𝒞 ℬ induced by a 2-commutative diagram between the two cospans: on objects it sends (x, y, φ) to (L x, K y, α_y⁻¹ ∘ M(φ) ∘ β_x⁻¹), and on morphisms it applies L and K componentwise.

def CategoricalPullback.map (H : 𝒳 ⥤ 𝒵) (I : 𝒴 ⥤ 𝒵)
    (L : 𝒳 ⥤ 𝒜) (K : 𝒴 ⥤ ℬ) (M : 𝒵 ⥤ 𝒞) (F : 𝒜 ⥤ 𝒞) (G : ℬ ⥤ 𝒞)
    (α : K ⋙ G ≅ I ⋙ M) (β : H ⋙ M ≅ L ⋙ F) :
    CategoricalPullback H I ⥤ CategoricalPullback F G
Tag 02XB, a lemma

Tag 02XB in the Stacks Project.

CategoryTheory.induced_faithful_of_faithful, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoFibreProduct/InducedFunctor.lean, line 174. The attribute's comment: “(1)”.

Stacks 02XB (1) — If K and L are faithful, then the induced functor 𝒳 ×_𝒵 𝒴 ⥤ 𝒜 ×_𝒞 ℬ is faithful.

theorem induced_faithful_of_faithful [K.Faithful] [L.Faithful] :
    (CategoricalPullback.map H I L K M F G α β).Faithful

CategoryTheory.induced_fullyFaithful_of_fullyFaithful, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoFibreProduct/InducedFunctor.lean, line 183. The attribute's comment: “(2)”. References: SGA 1 VI (4.1).

Stacks 02XB (2) — If K and L are fully faithful and M is faithful, then the induced functor 𝒳 ×_𝒵 𝒴 ⥤ 𝒜 ×_𝒞 ℬ is fully faithful.

theorem induced_fullyFaithful_of_fullyFaithful
    [K.Faithful] [K.Full] [L.Faithful] [L.Full] [M.Faithful] :
    (CategoricalPullback.map H I L K M F G α β).Faithful ∧
      (CategoricalPullback.map H I L K M F G α β).Full

CategoryTheory.induced_isEquivalence_of_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoFibreProduct/InducedFunctor.lean, line 201. The attribute's comment: “(3)”.

Stacks 02XB (3) — If K and L are equivalences and M is fully faithful, then the induced functor 𝒳 ×_𝒵 𝒴 ⥤ 𝒜 ×_𝒞 ℬ is an equivalence of categories.

theorem induced_isEquivalence_of_isEquivalence
    [K.IsEquivalence] [L.IsEquivalence] [M.Faithful] [M.Full] :
    (CategoricalPullback.map H I L K M F G α β).IsEquivalence
Tag 02XC, a lemma

Tag 02XC in the Stacks Project.

CategoryTheory.Limits.CategoricalPullback.assocFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoFibreProduct/Associativity.lean, line 33.

Stacks 02XC. The canonical comparison functor (𝒜 ×_ℬ 𝒞) ×_𝒟 ℰ ⥤ 𝒜 ×_ℬ (𝒞 ×_𝒟 ℰ), rebracketing ((A, C, φ), E, ψ) ↦ (A, (C, E, ψ), φ).

def CategoricalPullback.assocFunctor
    (H : 𝒜 ⥤ ℬ) (K : 𝒞 ⥤ ℬ) (L : 𝒞 ⥤ 𝒟) (M : ℰ ⥤ 𝒟) :
    CategoricalPullback (CategoricalPullback.π₂ H K ⋙ L) M ⥤
      CategoricalPullback H (CategoricalPullback.π₁ L M ⋙ K)

CategoryTheory.Limits.CategoricalPullback.assoc, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoFibreProduct/Associativity.lean, line 58.

Stacks 02XC. Associativity of 2-fibre products of categories: for H : 𝒜 ⥤ ℬ, K : 𝒞 ⥤ ℬ, L : 𝒞 ⥤ 𝒟 and M : ℰ ⥤ 𝒟 the two iterated 2-fibre products are canonically equivalent, (𝒜 ×_ℬ 𝒞) ×_𝒟 ℰ ≌ 𝒜 ×_ℬ (𝒞 ×_𝒟 ℰ), via CategoricalPullback.assocFunctor.

def CategoricalPullback.assoc
    (H : 𝒜 ⥤ ℬ) (K : 𝒞 ⥤ ℬ) (L : 𝒞 ⥤ 𝒟) (M : ℰ ⥤ 𝒟) :
    CategoricalPullback (CategoricalPullback.π₂ H K ⋙ L) M ≌
      CategoricalPullback H (CategoricalPullback.π₁ L M ⋙ K)
Tag 04S7, a lemma

Tag 04S7 in the Stacks Project.

CategoryTheory.Limits.CategoricalPullback.pr₀₂, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoFibreProduct/TripleProjection.lean, line 91.

Stacks 04S7. For a commuting inner square G ⋙ P = H ⋙ Q under the diagram 𝒜 → ℬ ← 𝒞 → 𝒟 ← ℰ, the canonical functor (𝒜 ×_ℬ 𝒞) ×_𝒟 ℰ ⥤ 𝒜 ×_ℱ ℰ which forgets the middle factor and transports the two structural isomorphisms into ℱ.

def CategoricalPullback.pr₀₂ (h : G ⋙ P = H ⋙ Q) :
    CategoricalPullback (CategoricalPullback.π₂ F G ⋙ H) I ⥤
      CategoricalPullback (F ⋙ P) (I ⋙ Q)
Tag 02XD, a lemma

Tag 02XD in the Stacks Project.

CategoryTheory.Limits.CategoricalPullback.assocComp, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoFibreProduct/Cancellation.lean, line 107.

Stacks 02XD. The canonical equivalence of categories (A ×_B C) ×_C D ≌ A ×_B D for A --F--> B <--G-- C <--H-- D, i.e. CategoricalPullback (π₂ F G) H ≌ CategoricalPullback F (H ⋙ G), given by assocCompFunctor.

def assocComp :
    CategoricalPullback (π₂ F G) H ≌ CategoricalPullback F (H ⋙ G)
Tag 02XE, a lemma

Tag 02XE in the Stacks Project.

CategoryTheory.Limits.CategoricalPullback.prodDiagFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoFibreProduct/Diagonal.lean, line 58.

Stacks 02XE. The canonical comparison functor CategoricalPullback (G₁.prod G₂) (Functor.diag S) ⥤ CategoricalPullback G₁ G₂. On objects it sends ((X₁, X₂), Y, φ) to (X₁, X₂, φ₁ ≪≫ φ₂⁻¹), where φ = (φ₁, φ₂); on morphisms it acts as the identity on the underlying pair of component morphisms.

def prodDiagFunctor (G₁ : C₁ ⥤ S) (G₂ : C₂ ⥤ S) :
    CategoricalPullback (G₁.prod G₂) (Functor.diag S) ⥤ CategoricalPullback G₁ G₂

CategoryTheory.Limits.CategoricalPullback.isEquivalence_prodDiagFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoFibreProduct/Diagonal.lean, line 165.

Stacks 02XE. The canonical comparison functor prodDiagFunctor is an equivalence of categories: the 2-fibre product of G₁ × G₂ : C₁ × C₂ ⥤ S × S and the diagonal Δ : S ⥤ S × S is canonically equivalent to C₁ ×_S C₂.

theorem isEquivalence_prodDiagFunctor (G₁ : C₁ ⥤ S) (G₂ : C₂ ⥤ S) :
    (prodDiagFunctor G₁ G₂).IsEquivalence

CategoryTheory.Limits.CategoricalPullback.prodDiagEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoFibreProduct/Diagonal.lean, line 174.

Stacks 02XE. The canonical equivalence of categories CategoricalPullback (G₁.prod G₂) (Functor.diag S) ≌ CategoricalPullback G₁ G₂, induced by prodDiagFunctor.

noncomputable def prodDiagEquiv (G₁ : C₁ ⥤ S) (G₂ : C₂ ⥤ S) :
    CategoricalPullback (G₁.prod G₂) (Functor.diag S) ≌ CategoricalPullback G₁ G₂
Tag 02XF, a lemma

Tag 02XF in the Stacks Project.

CategoryTheory.Limits.CategoricalPullback.diagComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoFibreProduct/IteratedDiagonal.lean, line 98.

Stacks 02XF. The comparison functor (𝒞 ×_𝒮 𝒞) ×_{𝒞 × 𝒞} 𝒞 ⥤ 𝒞 ×_{𝒮 × 𝒮} 𝒮. On objects it sends ((c₁, c₂, φ), c₃, ψ) to (c₃, G₁ c₁, (G₁ ψ₁⁻¹, φ⁻¹ ∘ G₂ ψ₂⁻¹)), and on morphisms ((α₁, α₂), α₃) to (α₃, G₁ α₁).

def diagComparison : diagComparisonSource G₁ G₂ ⥤ diagComparisonTarget G₁ G₂

CategoryTheory.Limits.CategoricalPullback.isEquivalence_diagComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoFibreProduct/IteratedDiagonal.lean, line 234.

Stacks 02XF. The comparison functor (𝒞 ×_𝒮 𝒞) ×_{𝒞 × 𝒞} 𝒞 ⥤ 𝒞 ×_{𝒮 × 𝒮} 𝒮 is an equivalence of categories. (The source asserts an isomorphism of categories; that is corrected to an equivalence per the Stacks comments #5394 and #5627, since the functor is in general not bijective on objects.)

theorem isEquivalence_diagComparison : (diagComparison G₁ G₂).IsEquivalence
Tag 04Z1, a lemma

Tag 04Z1 in the Stacks Project.

CategoryTheory.Limits.CategoricalPullback.relativeDiagonalSquareIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoFibreProduct/AsPullback.lean, line 89.

Stacks 04Z1. The natural isomorphism σ : Θ ⋙ ρ ≅ π ⋙ Δ_{C/D} witnessing that the square 2-commutes; its component at (a, b, f) is (𝟙_{F a}, f⁻¹).

def relativeDiagonalSquareIso :
    (mapBase F G H ⋙ toRelativeDiagonalTarget F G H) ≅ (toBase F G ⋙ relativeDiagonal H)

CategoryTheory.Limits.CategoricalPullback.toRelativeDiagonalPullback, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoFibreProduct/AsPullback.lean, line 108.

Stacks 04Z1. The functor A ×_C B ⥤ (A ×_D B) ×_{C ×_D C} C induced by (Θ, π, σ) into the explicit 2-fibre product of the cospan A ×_D B --ρ--> C ×_D C <--Δ_{C/D}-- C. On objects it sends (a, b, f) to ((a, b, H f), F a, (𝟙_{F a}, f⁻¹)), and a morphism (x, y) to ((x, y), F x).

def toRelativeDiagonalPullback :
    CategoricalPullback F G ⥤
      CategoricalPullback (toRelativeDiagonalTarget F G H) (relativeDiagonal H)

CategoryTheory.Limits.CategoricalPullback.isEquivalence_toRelativeDiagonalPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoFibreProduct/AsPullback.lean, line 179.

Stacks 04Z1. The square above is a 2-fibre product diagram: the induced functor A ×_C B ⥤ (A ×_D B) ×_{C ×_D C} C is an equivalence of categories.

theorem isEquivalence_toRelativeDiagonalPullback :
    (toRelativeDiagonalPullback F G H).IsEquivalence
Tag 04YR, a lemma

Tag 04YR in the Stacks Project.

CategoryTheory.Limits.CategoricalPullback.baseChangeDiagonalSquareIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoFibreProduct/DiagonalBaseChange.lean, line 104.

Stacks 04YR. The structural 2-cell r ⋙ Δ_{X/Y} ≅ Δ_{U/V} ⋙ (r × r) of the base-change square for the diagonal. Both composites have both projections equal to r = π₁ h s, so the 2-cell is the canonical one with identity projections.

def baseChangeDiagonalSquareIso :
    (π₁ h s ⋙ relativeDiagonal h) ≅ (relativeDiagonal (π₂ h s) ⋙ mapDiag h s)

CategoryTheory.Limits.CategoricalPullback.baseChangeDiagonalSquare, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoFibreProduct/DiagonalBaseChange.lean, line 126.

Stacks 04YR. The base-change square for the diagonal, over U = h ⊡ s: its legs are r = π₁ h s : U ⥤ X and Δ_{U/V} = relativeDiagonal (π₂ h s) : U ⥤ U ×_V U, its cospan is Δ_{X/Y} = relativeDiagonal h : X ⥤ X ×_Y X and r × r = mapDiag h s, and its structural 2-cell is baseChangeDiagonalSquareIso.

def baseChangeDiagonalSquare :
    CatCommSqOver (relativeDiagonal h) (mapDiag h s) (h ⊡ s)

CategoryTheory.Limits.CategoricalPullback.isEquivalence_baseChangeDiagonalComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoFibreProduct/DiagonalBaseChange.lean, line 402.

Stacks 04YR. The diagonal is stable under base change: for h : X ⥤ Y and s : V ⥤ Y, with U = X ×_Y V, r = π₁ h s and g = π₂ h s, the square Δ_{U/V} : U ⥤ U ×_V U, r : U ⥤ X over Δ_{X/Y} : X ⥤ X ×_Y X, r × r : U ×_V U ⥤ X ×_Y X is 2-cartesian, i.e. its comparison functor U ⥤ Δ_{X/Y} ⊡ (r × r) is an equivalence of categories. The quasi-inverse is baseChangeDiagonalInverse, the unit is an identity by baseChangeDiagonalComparison_comp_inverse, and the counit is baseChangeDiagonalCounitIso.

theorem isEquivalence_baseChangeDiagonalComparison :
    Functor.IsEquivalence (comparison (relativeDiagonal h) (mapDiag h s)
      (baseChangeDiagonalSquare h s))
Sources
LeanCategoryTheory.Bicategory.TwoCommSq · CategoryTheory.Bicategory.TwoCommSq.PreHom · CategoryTheory.Bicategory.TwoCommSq.category · CategoryTheory.Bicategory.IsBiterminal · CategoryTheory.Bicategory.IsTwoFibreProduct · CategoryTheory.Limits.CategoricalPullback · CategoryTheory.Limits.CategoricalPullback.instCategory · CategoryTheory.Limits.CategoricalPullback.catCommSq

Section4.32 Categories over categories#

Section 4.32 of the Stacks Project, Tag 02XG. 4 tags here are carried by 21 declarations of the repository (all in StacksFrontier) and 8 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 003Y, a definition

Tag 003Y in the Stacks Project.

Declarations registered for the tag:

Tag 02XH, a definition

Tag 02XH in the Stacks Project.

Declarations registered for the tag:

Tag 0040, a lemma

Tag 0040 in the Stacks Project.

CategoryTheory.TwoFibreProductOver.fibreIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoFibreProduct/OverBase.lean, line 77.

Clause (1) of Stacks 0040: the comparison isomorphism φ of an object (U, x, y, φ) is an isomorphism F x ≅ G y in the fibre category 𝒮_U. Both F x and G y lie over U because F and G are 1-morphisms over 𝒞, and φ is vertical by construction.

def fibreIso (hF : F ⋙ p𝒮 = p𝒳) (hG : G ⋙ p𝒮 = p𝒴) (P : TwoFibreProductOver p𝒳 p𝒴 p𝒮 F G) :
    Functor.Fiber.mk (obj_over_base_x p𝒳 p𝒴 p𝒮 F G hF P) ≅
      Functor.Fiber.mk (obj_over_base_y p𝒳 p𝒴 p𝒮 F G hG P)

CategoryTheory.TwoFibreProductOver.lift, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoFibreProduct/OverBase.lean, line 96.

The mediating 1-morphism γ : W ⥤ 𝒳 ×_𝒮 𝒴 of Stacks 0040, sending w to the quadruple (pW w, H w, K w, t w). That H and K are 1-morphisms over 𝒞 is what makes the two components of γ h lie over the common base morphism pW h, and the comparison square is the naturality of t.

def lift : W ⥤ TwoFibreProductOver p𝒳 p𝒴 p𝒮 F G

CategoryTheory.TwoFibreProductOver.lift_comp_structureFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoFibreProduct/OverBase.lean, line 151.

The mediating 1-morphism is a 1-morphism of categories over 𝒞: it sends w to an object lying over pW w, and a morphism to one lying over pW h.

theorem lift_comp_structureFunctor :
    lift p𝒳 p𝒴 p𝒮 F G pW H K hH hK t ht ⋙ structureFunctor p𝒳 p𝒴 p𝒮 F G = pW

CategoryTheory.TwoFibreProductOver.liftCompFst_hom_app_isHomLift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoFibreProduct/OverBase.lean, line 168.

The first comparison isomorphism is a 2-morphism over 𝒞: its components are vertical.

theorem liftCompFst_hom_app_isHomLift (w : W) :
    p𝒳.IsHomLift (𝟙 (pW.obj w)) ((liftCompFst p𝒳 p𝒴 p𝒮 F G pW H K hH hK t ht).hom.app w)

CategoryTheory.TwoFibreProductOver.liftCompSnd_hom_app_isHomLift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoFibreProduct/OverBase.lean, line 174.

The second comparison isomorphism is a 2-morphism over 𝒞: its components are vertical.

theorem liftCompSnd_hom_app_isHomLift (w : W) :
    p𝒴.IsHomLift (𝟙 (pW.obj w)) ((liftCompSnd p𝒳 p𝒴 p𝒮 F G pW H K hH hK t ht).hom.app w)

CategoryTheory.TwoFibreProductOver.lift_whiskerRight_psi, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoFibreProduct/OverBase.lean, line 183.

The factorisation is compatible with the given isomorphism t: whiskering the 2-cell ψ into γ and correcting by the two comparison isomorphisms recovers t. This is the commuting square of 2-morphisms which makes γ a factorisation of the test cone (H, K, t), rather than merely a 1-morphism with the right two projections.

theorem lift_whiskerRight_psi :
    Functor.whiskerRight (liftCompFst p𝒳 p𝒴 p𝒮 F G pW H K hH hK t ht).hom F ≫ t.hom =
      Functor.whiskerLeft (lift p𝒳 p𝒴 p𝒮 F G pW H K hH hK t ht) (psiIso p𝒳 p𝒴 p𝒮 F G).hom ≫
        Functor.whiskerRight (liftCompSnd p𝒳 p𝒴 p𝒮 F G pW H K hH hK t ht).hom G

CategoryTheory.TwoFibreProductOver.natTrans_ext, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoFibreProduct/OverBase.lean, line 213.

Two 2-morphisms into the 2-fibre product that agree after projecting to 𝒳 and to 𝒴 are equal, so the mediating 2-morphism supplied by liftIso is the only one.

theorem natTrans_ext {γ δ : W ⥤ TwoFibreProductOver p𝒳 p𝒴 p𝒮 F G} {α β : γ ⟶ δ}
    (h₁ : Functor.whiskerRight α (fst p𝒳 p𝒴 p𝒮 F G) =
      Functor.whiskerRight β (fst p𝒳 p𝒴 p𝒮 F G))
    (h₂ : Functor.whiskerRight α (snd p𝒳 p𝒴 p𝒮 F G) =
      Functor.whiskerRight β (snd p𝒳 p𝒴 p𝒮 F G)) : α = β

CategoryTheory.TwoFibreProductOver.liftIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoFibreProduct/OverBase.lean, line 230.

Any other factorisation of the test cone (H, K, t) through the 2-fibre product is 2-isomorphic over 𝒞 to the mediating 1-morphism lift. Together with natTrans_ext this is the uniqueness half of the 2-universal property: the factorisation is unique up to a unique 2-isomorphism over 𝒞.

noncomputable def liftIso (γ : W ⥤ TwoFibreProductOver p𝒳 p𝒴 p𝒮 F G)
    (a : γ ⋙ fst p𝒳 p𝒴 p𝒮 F G ≅ H) (b : γ ⋙ snd p𝒳 p𝒴 p𝒮 F G ≅ K)
    (ha : ∀ w, p𝒳.IsHomLift (𝟙 (pW.obj w)) (a.hom.app w))
    (hb : ∀ w, p𝒴.IsHomLift (𝟙 (pW.obj w)) (b.hom.app w))
    (hab : Functor.whiskerRight a.hom F ≫ t.hom =
      Functor.whiskerLeft γ (psiIso p𝒳 p𝒴 p𝒮 F G).hom ≫ Functor.whiskerRight b.hom G)
    (hH : H ⋙ p𝒳 = pW) (hK : K ⋙ p𝒴 = pW)
    (ht : ∀ w, p𝒮.IsHomLift (𝟙 (pW.obj w)) (t.hom.app w)) :
    γ ≅ lift p𝒳 p𝒴 p𝒮 F G pW H K hH hK t ht

CategoryTheory.TwoFibreProductOver.fst_comp_eq, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoFibreProductOver.lean, line 207.

The first projection is strictly over 𝒞.

lemma fst_comp_eq : fst p𝒳 p𝒴 p𝒮 F G ⋙ p𝒳 = structureFunctor p𝒳 p𝒴 p𝒮 F G

CategoryTheory.TwoFibreProductOver.snd_comp_eq, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoFibreProductOver.lean, line 214.

The second projection is strictly over 𝒞.

lemma snd_comp_eq : snd p𝒳 p𝒴 p𝒮 F G ⋙ p𝒴 = structureFunctor p𝒳 p𝒴 p𝒮 F G

CategoryTheory.TwoFibreProductOver.psiIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoFibreProductOver.lean, line 222.

The 2-cell ψ : π₁ ⋙ F ≅ π₂ ⋙ G filling the square, with component at (U, x, y, φ) the comparison isomorphism φ itself.

def psiIso (p𝒳 : 𝒳 ⥤ 𝒞) (p𝒴 : 𝒴 ⥤ 𝒞) (p𝒮 : 𝒮 ⥤ 𝒞) (F : 𝒳 ⥤ 𝒮) (G : 𝒴 ⥤ 𝒮) :
    (fst p𝒳 p𝒴 p𝒮 F G ⋙ F) ≅ (snd p𝒳 p𝒴 p𝒮 F G ⋙ G)

CategoryTheory.TwoFibreProductOver.psiIso_hom_vertical, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoFibreProductOver.lean, line 237.

Every component of the 2-cell ψ is vertical over 𝒞: it lies over an identity.

lemma psiIso_hom_vertical (P : TwoFibreProductOver p𝒳 p𝒴 p𝒮 F G) :
    p𝒮.IsHomLift (𝟙 P.base) ((psiIso p𝒳 p𝒴 p𝒮 F G).hom.app P)
Tag 02XI, a lemma

Tag 02XI in the Stacks Project.

CategoryTheory.Limits.CategoricalPullbackOver.toFiberPullback, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoFibreProduct/Fibres.lean, line 295.

Stacks 02XI. The canonical functor (X ×_S Y)_U ⥤ X_U ×_{S_U} Y_U, sending (U, x, y, f) to (x, y, f) and (a, b) to (a, b).

def toFiberPullback (hf : F ⋙ pS = pX) (hg : G ⋙ pS = pY) (U : C) :
    (CategoricalPullbackOver.structureFunctor (pX := pX) (pY := pY) (pS := pS) (F := F)
      (G := G)).Fiber U ⥤
    CategoricalPullback (Functor.fiberMap pX pS F hf U) (Functor.fiberMap pY pS G hg U)

CategoryTheory.Limits.CategoricalPullbackOver.ofFiberPullback, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoFibreProduct/Fibres.lean, line 317.

Stacks 02XI. The canonical functor X_U ×_{S_U} Y_U ⥤ (X ×_S Y)_U inverse to toFiberPullback, sending (x, y, f) to (U, x, y, f) and (a, b) to (a, b).

def ofFiberPullback (hf : F ⋙ pS = pX) (hg : G ⋙ pS = pY) (U : C) :
    CategoricalPullback (Functor.fiberMap pX pS F hf U) (Functor.fiberMap pY pS G hg U) ⥤
    (CategoricalPullbackOver.structureFunctor (pX := pX) (pY := pY) (pS := pS) (F := F)
      (G := G)).Fiber U

CategoryTheory.Limits.CategoricalPullbackOver.toFiberPullback_comp_ofFiberPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoFibreProduct/Fibres.lean, line 425.

Stacks 02XI. Composing the comparison functor with its inverse gives the identity on the fibre (X ×_S Y)_U.

theorem toFiberPullback_comp_ofFiberPullback (hf : F ⋙ pS = pX) (hg : G ⋙ pS = pY) (U : C) :
    toFiberPullback pX pY pS F G hf hg U ⋙ ofFiberPullback pX pY pS F G hf hg U = 𝟭 _

CategoryTheory.Limits.CategoricalPullbackOver.ofFiberPullback_comp_toFiberPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoFibreProduct/Fibres.lean, line 439.

Stacks 02XI. Composing the inverse comparison functor with the comparison functor gives the identity on X_U ×_{S_U} Y_U. Together with toFiberPullback_comp_ofFiberPullback this says the fibre of the 2-fibre product over C at U is isomorphic, not merely equivalent, to the 2-fibre product of the fibres.

theorem ofFiberPullback_comp_toFiberPullback (hf : F ⋙ pS = pX) (hg : G ⋙ pS = pY) (U : C) :
    ofFiberPullback pX pY pS F G hf hg U ⋙ toFiberPullback pX pY pS F G hf hg U = 𝟭 _

CategoryTheory.TwoFibreProductOver.toFiberPullback, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoFibreProduct/OverFibres.lean, line 48.

Stacks 02XI. The canonical functor (𝒳 ×_𝒮 𝒴)_U ⥤ 𝒳_U ×_{𝒮_U} 𝒴_U, sending (U, x, y, φ) to (x, y, φ) and (a, b) to (a, b).

def toFiberPullback (hF : F ⋙ p𝒮 = p𝒳) (hG : G ⋙ p𝒮 = p𝒴) (U : 𝒞) :
    (structureFunctor p𝒳 p𝒴 p𝒮 F G).Fiber U ⥤
      CategoricalPullback (Functor.fiberMap p𝒳 p𝒮 F hF U) (Functor.fiberMap p𝒴 p𝒮 G hG U)

CategoryTheory.TwoFibreProductOver.ofFiberPullback, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoFibreProduct/OverFibres.lean, line 67.

Stacks 02XI. The canonical functor 𝒳_U ×_{𝒮_U} 𝒴_U ⥤ (𝒳 ×_𝒮 𝒴)_U inverse to toFiberPullback, sending (x, y, φ) to (U, x, y, φ) and (a, b) to (a, b) over 𝟙 U.

def ofFiberPullback (hF : F ⋙ p𝒮 = p𝒳) (hG : G ⋙ p𝒮 = p𝒴) (U : 𝒞) :
    CategoricalPullback (Functor.fiberMap p𝒳 p𝒮 F hF U) (Functor.fiberMap p𝒴 p𝒮 G hG U) ⥤
      (structureFunctor p𝒳 p𝒴 p𝒮 F G).Fiber U

CategoryTheory.TwoFibreProductOver.toFiberPullback_comp_ofFiberPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoFibreProduct/OverFibres.lean, line 166.

Stacks 02XI. Composing the comparison functor with its inverse gives the identity on the fibre (𝒳 ×_𝒮 𝒴)_U: the round trip forgets the base object and reinstates it as the literal U, which is the same object because it lies over U, and both functors are the identity on the underlying pair of components.

theorem toFiberPullback_comp_ofFiberPullback (hF : F ⋙ p𝒮 = p𝒳) (hG : G ⋙ p𝒮 = p𝒴) (U : 𝒞) :
    toFiberPullback p𝒳 p𝒴 p𝒮 F G hF hG U ⋙ ofFiberPullback p𝒳 p𝒴 p𝒮 F G hF hG U = 𝟭 _

CategoryTheory.TwoFibreProductOver.ofFiberPullback_comp_toFiberPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoFibreProduct/OverFibres.lean, line 181.

Stacks 02XI. Composing the inverse comparison functor with the comparison functor gives the identity on 𝒳_U ×_{𝒮_U} 𝒴_U: the base coordinate U is added and then forgotten, so the triple (x, y, φ) is rebuilt unchanged. Together with toFiberPullback_comp_ofFiberPullback this says the fibre of the 2-fibre product over 𝒞 at U is isomorphic, not merely equivalent, to the 2-fibre product of the fibres.

theorem ofFiberPullback_comp_toFiberPullback (hF : F ⋙ p𝒮 = p𝒳) (hG : G ⋙ p𝒮 = p𝒴) (U : 𝒞) :
    ofFiberPullback p𝒳 p𝒴 p𝒮 F G hF hG U ⋙ toFiberPullback p𝒳 p𝒴 p𝒮 F G hF hG U = 𝟭 _

CategoryTheory.TwoFibreProductOver.fiberEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoFibreProduct/OverFibres.lean, line 193.

Stacks 02XI, as an equivalence of categories: the fibre of the 2-fibre product over 𝒞 at U is the 2-fibre product of the fibre categories. Both unit and counit are identities, the two functors being strictly mutually inverse.

def fiberEquiv (hF : F ⋙ p𝒮 = p𝒳) (hG : G ⋙ p𝒮 = p𝒴) (U : 𝒞) :
    (structureFunctor p𝒳 p𝒴 p𝒮 F G).Fiber U ≌
      CategoricalPullback (Functor.fiberMap p𝒳 p𝒮 F hF U) (Functor.fiberMap p𝒴 p𝒮 G hG U)
Sources
LeanCategoryTheory.BasedCategory · CategoryTheory.BasedFunctor · CategoryTheory.BasedNatTrans · CategoryTheory.BasedNatTrans.homCategory · CategoryTheory.BasedCategory.bicategory · CategoryTheory.Functor.Fiber · CategoryTheory.Functor.Fiber.fiberCategory · CategoryTheory.Functor.IsHomLift

Section4.33 Fibred categories#

Section 4.33 of the Stacks Project, Tag 02XJ. 13 tags here are carried by 24 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 02XL, a lemma

Tag 02XL in the Stacks Project.

Stacks.StronglyCartesian.isStronglyCartesian_conditions_hold, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedCategory/StronglyCartesian.lean, line 37. References: SGA 1 VI (6.12), “iso ⇒ Cartesian”.

Stacks 02XL. All three claims of StronglyCartesianStability hold for every p : 𝒮 ⥤ 𝒞, each supplied by Mathlib: Functor.IsStronglyCartesian.comp, .of_isIso and .isIso_of_base_isIso.

theorem isStronglyCartesian_conditions_hold {𝒞 : Type*} [Category 𝒞] {𝒮 : Type*} [Category 𝒮]
    (p : 𝒮 ⥤ 𝒞) : StronglyCartesianStability p
Tag 09WU, a lemma

Tag 09WU in the Stacks Project.

CategoryTheory.Functor.IsStronglyCartesian.comp_functor, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedCategory/StronglyCartesianComp.lean, line 64.

If θ : a' ⟶ a is a strongly cartesian lift of φ : b ⟶ F.obj a along F : A ⥤ B, and φ is in turn a strongly cartesian lift of f : R ⟶ G.obj (F.obj a) along G : B ⥤ C, then θ is a strongly cartesian lift of f along F ⋙ G.

Taking φ := F.map θ and f := G.map (F.map θ): strong cartesianness of θ for F together with strong cartesianness of F.map θ for G implies strong cartesianness of θ for F ⋙ G.

lemma IsStronglyCartesian.comp_functor (F : A ⥤ B) (G : B ⥤ C)
    {a' a : A} {b : B} {R : C}
    (f : R ⟶ G.obj (F.obj a)) (φ : b ⟶ F.obj a) (θ : a' ⟶ a)
    [F.IsStronglyCartesian φ θ] [G.IsStronglyCartesian f φ] :
    (F ⋙ G).IsStronglyCartesian f θ
Tag 06N4, a lemma

Tag 06N4 in the Stacks Project.

CategoryTheory.hasPullback_of_isStronglyCartesian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedCategory/FibreProductsCartesian.lean, line 172.

Stacks 06N4. Given φ : x ⟶ y strongly cartesian over p, an existing fibre product p x ×_{p y} p z in 𝒞, and a strongly cartesian morphism a : w ⟶ z in 𝒮 lying over the second projection of that fibre product (as recorded by hw and ha), the fibre product x ×_y z exists in 𝒮.

theorem hasPullback_of_isStronglyCartesian
    (p : 𝒮 ⥤ 𝒞) {x y z : 𝒮} (φ : x ⟶ y) (g : z ⟶ y)
    [Functor.IsStronglyCartesian p (p.map φ) φ]
    [Limits.HasPullback (p.map φ) (p.map g)]
    (w : 𝒮) (a : w ⟶ z)
    (hw : p.obj w = Limits.pullback (p.map φ) (p.map g))
    (ha : p.map a = eqToHom hw ≫ Limits.pullback.snd (p.map φ) (p.map g))
    [Functor.IsStronglyCartesian p (p.map a) a] :
    Limits.HasPullback φ g

CategoryTheory.pullbackIsoOfIsStronglyCartesian, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedCategory/FibreProductsCartesian.lean, line 190.

Stacks 06N4. In the situation of hasPullback_of_isStronglyCartesian the fibre product x ×_y z is canonically isomorphic to w: both are limits of the same cospan, w by the limit square built from the strongly cartesian morphisms φ and a.

noncomputable def pullbackIsoOfIsStronglyCartesian
    (p : 𝒮 ⥤ 𝒞) {x y z : 𝒮} (φ : x ⟶ y) (g : z ⟶ y)
    [Functor.IsStronglyCartesian p (p.map φ) φ]
    [Limits.HasPullback (p.map φ) (p.map g)]
    (w : 𝒮) (a : w ⟶ z)
    (hw : p.obj w = Limits.pullback (p.map φ) (p.map g))
    (ha : p.map a = eqToHom hw ≫ Limits.pullback.snd (p.map φ) (p.map g))
    [Functor.IsStronglyCartesian p (p.map a) a] [Limits.HasPullback φ g] :
    Limits.pullback φ g ≅ w
Tag 02XM, a definition

Tag 02XM in the Stacks Project.

CategoryTheory.Functor.IsFibredCategory, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedCategory/ChoiceOfPullbacks.lean, line 303.

Stacks 02XM. A functor p : 𝒳 ⥤ 𝒮 is a fibred category over 𝒮 when for every object x of 𝒳 lying over an object U of 𝒮 and every morphism f : V ⟶ U of 𝒮 there exists a strongly cartesian morphism f^* x ⟶ x lying over f.

That φ lies over f is part of CategoryTheory.Functor.IsStronglyCartesian, which extends CategoryTheory.Functor.IsHomLift. See the implementation notes for why this is Mathlib's CategoryTheory.Functor.IsFibered and not its CategoryTheory.Functor.IsPreFibered.

def IsFibredCategory (p : 𝒳 ⥤ 𝒮) : Prop

CategoryTheory.Functor.isFibredCategory_iff_isFibered, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedCategory/ChoiceOfPullbacks.lean, line 315. The attribute's comment: “the identification with Mathlib's Functor.IsFibered”. References: SGA 1 VI (6.11), “Sufficiency”.

Stacks 02XM is Mathlib's CategoryTheory.Functor.IsFibered. Forward, a strongly cartesian lift of every base morphism makes p fibred by CategoryTheory.Functor.IsFibered.of_exists_isStronglyCartesian. Backward, a fibred category has a cartesian lift of every base morphism by CategoryTheory.Functor.IsPreFibered.exists_isCartesian and every cartesian morphism of a fibred category is strongly cartesian by CategoryTheory.Functor.IsFibered.isStronglyCartesian_of_isCartesian.

theorem isFibredCategory_iff_isFibered (p : 𝒳 ⥤ 𝒮) : p.IsFibredCategory ↔ p.IsFibered

Declarations registered for the tag:

Tag 02XN, a definition

Tag 02XN in the Stacks Project.

CategoryTheory.Functor.ChoiceOfPullbacks, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedCategory/ChoiceOfPullbacks.lean, line 91. The attribute's comment: “(1)”.

Stacks 02XN (1). A choice of pullbacks for p : 𝒳 ⥤ 𝒮 is a choice, for every morphism f : V ⟶ U of 𝒮 and every object x of the fibre of p over U, of an object f^* x of the fibre over V together with a strongly cartesian morphism f^* x ⟶ x lying over f.

structure ChoiceOfPullbacks (p : 𝒳 ⥤ 𝒮)

CategoryTheory.Functor.ChoiceOfPullbacks.pullbackFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedCategory/ChoiceOfPullbacks.lean, line 171. The attribute's comment: “(2)”.

Stacks 02XN (2). The pullback functor f^* : 𝒳_U ⥤ 𝒳_V between the fibres of p attached to a morphism f : V ⟶ U of 𝒮 by a choice of pullbacks.

noncomputable def pullbackFunctor {V U : 𝒮} (f : V ⟶ U) : p.Fiber U ⥤ p.Fiber V
Tag 02XO, a lemma

Tag 02XO in the Stacks Project.

CategoryTheory.Functor.IsFibered.pbMapId, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedCategory/PullbackPseudofunctor.lean, line 352.

Stacks 02XO, clause (2). The unitor (𝟙 U)* ≅ 𝟭 (p.Fiber U), the canonical isomorphism coming from the uniqueness of strongly cartesian factorisations.

noncomputable def pbMapId (p : 𝒳 ⥤ 𝒮) [p.IsFibered] (U : LocallyDiscrete 𝒮ᵒᵖ) :
    pbMap p (𝟙 U) ≅ 𝟙 (pbObj p U)

CategoryTheory.Functor.IsFibered.pbMapComp, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedCategory/PullbackPseudofunctor.lean, line 360. References: SGA 4 VI (6.1.2), “(6.1.2.1)”.

Stacks 02XO, clause (1). The compositor (g ≫ f)* ≅ f* ⋙ g*, the canonical isomorphism compatible with the chosen cartesian lifts; pbMapComp_uniq shows it is the only such isomorphism.

noncomputable def pbMapComp (p : 𝒳 ⥤ 𝒮) [p.IsFibered]
    {U V W : LocallyDiscrete 𝒮ᵒᵖ} (φ : U ⟶ V) (γ : V ⟶ W) :
    pbMap p (φ ≫ γ) ≅ pbMap p φ ≫ pbMap p γ

CategoryTheory.Functor.IsFibered.pullbackPseudofunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedCategory/PullbackPseudofunctor.lean, line 525. References: SGA 4 VI (7.1.4), “partial”; SGA 4 XVII (3.3.3), “Forward direction”.

Statement 1 (Stacks 02XO). The pullback pseudofunctor associated to a fibred category p. Its object part is U ↦ Cat.of (p.Fiber U), its 1-cell part is f ↦ f*, its unitor is (𝟙 U)* ≅ 𝟭 (p.Fiber U) and its compositor is (g ≫ f)* ≅ f* ⋙ g*.

noncomputable def pullbackPseudofunctor (p : 𝒳 ⥤ 𝒮) [p.IsFibered] :
    Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat

CategoryTheory.Functor.IsFibered.pullbackPseudofunctor_mapComp_compatible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedCategory/PullbackPseudofunctor.lean, line 563. References: SGA 1 VI (7.2), “partial”.

Stacks 02XO, clause (1). The compositor of the pullback pseudofunctor is compatible with the chosen strongly cartesian lifts: on each object X, its underlying comparison morphism, followed by the composite of the chosen cartesian projections over γ and over φ, is the chosen cartesian projection over φ ≫ γ.

theorem pullbackPseudofunctor_mapComp_compatible (p : 𝒳 ⥤ 𝒮) [p.IsFibered]
    {U V W : LocallyDiscrete 𝒮ᵒᵖ} (φ : U ⟶ V) (γ : V ⟶ W) (X : ↑(pbObj p U)) :
    Fiber.fiberInclusion.map (((pullbackPseudofunctor p).mapComp φ γ).hom.toNatTrans.app X)
        ≫ (cartComp φ.as.unop γ.as.unop).proj X =
      IsPreFibered.pullbackMap X.2 (φ ≫ γ).as.unop

CategoryTheory.Functor.IsFibered.pbMapComp_uniq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedCategory/PullbackPseudofunctor.lean, line 576. References: SGA 4 VI (6.1.2), “(6.1.2.1)”.

Stacks 02XO, clause (1), uniqueness. The compositor is the unique isomorphism (g ≫ f)* ≅ f* ⋙ g* compatible with the chosen cartesian lifts: any isomorphism whose components satisfy the compatibility triangle of pullbackPseudofunctor_mapComp_compatible equals pbMapComp.

theorem pbMapComp_uniq (p : 𝒳 ⥤ 𝒮) [p.IsFibered]
    {U V W : LocallyDiscrete 𝒮ᵒᵖ} (φ : U ⟶ V) (γ : V ⟶ W)
    (θ : pbMap p (φ ≫ γ) ≅ pbMap p φ ≫ pbMap p γ)
    (hθ : ∀ X : ↑(pbObj p U),
      Fiber.fiberInclusion.map (θ.hom.toNatTrans.app X) ≫
          (cartComp φ.as.unop γ.as.unop).proj X =
        IsPreFibered.pullbackMap X.2 (φ ≫ γ).as.unop) :
    θ = pbMapComp p φ γ
Tag 042G, a lemma

Tag 042G in the Stacks Project.

CategoryTheory.BasedCategory.isFibered_iff_of_equivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedCategory/EquivalenceInvariance.lean, line 170.

Stacks 042G (Lemma 4.33.8). Let 𝒮 be a category and let 𝒳 and 𝒴 be categories over 𝒮. If 𝒳 and 𝒴 are equivalent as categories over 𝒮, then 𝒳 is a fibred category over 𝒮 if and only if 𝒴 is.

theorem BasedCategory.isFibered_iff_of_equivalence
    {𝒳 : BasedCategory.{v₂, u₂} 𝒮} {𝒴 : BasedCategory.{v₃, u₃} 𝒮}
    (e : BasedCategory.Equivalence 𝒳 𝒴) :
    𝒳.p.IsFibered ↔ 𝒴.p.IsFibered
Tag 02XP, a definition

Tag 02XP in the Stacks Project.

CategoryTheory.CatFibered, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedCategory/TwoCategory.lean, line 85.

The 2-category of fibred categories over 𝒮: the sub-2-category of the 2-category BasedCategory 𝒮 of categories over 𝒮 (Stacks 003Y) whose

  1. objects are the categories p : 𝒳 ⥤ 𝒮 over 𝒮 that are fibred categories;
  2. 1-morphisms (𝒳, p) ⟶ (𝒴, p') are the functors G : 𝒳 ⥤ 𝒴 with p' ∘ G = p carrying strongly cartesian morphisms to strongly cartesian morphisms;
  3. 2-morphisms t : G ⟶ H are the morphisms of functors with p'(t_x) = 𝟙 (p x) for every object x of 𝒳.

The hom-category 𝒳 ⟶ 𝒴 is the source's Mor_{Fib/𝒮}(𝒳, 𝒴).

def CatFibered (𝒮 : Type u₁) [Category.{v₁} 𝒮]
Tag 02XQ, a lemma

Tag 02XQ in the Stacks Project.

CategoryTheory.TwoFibreProductOver.isFibered_structureFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedCategory/TwoFibreProduct.lean, line 223.

Stacks 02XQ, fibredness. If p𝒳, p𝒴, p𝒮 are fibred categories over 𝒞 and F, G are 1-morphisms of fibred categories over 𝒞, then the structure functor of the 2-fibre product 𝒳 ×_𝒮 𝒴 exhibits it as a fibred category over 𝒞.

theorem TwoFibreProductOver.isFibered_structureFunctor
    (p𝒳 : 𝒳 ⥤ 𝒞) (p𝒴 : 𝒴 ⥤ 𝒞) (p𝒮 : 𝒮 ⥤ 𝒞) (F : 𝒳 ⥤ 𝒮) (G : 𝒴 ⥤ 𝒮)
    [p𝒳.IsFibered] [p𝒴.IsFibered] [p𝒮.IsFibered]
    (hF : Functor.IsFibredOneMorphism p𝒳 p𝒮 F)
    (hG : Functor.IsFibredOneMorphism p𝒴 p𝒮 G) :
    (TwoFibreProductOver.structureFunctor p𝒳 p𝒴 p𝒮 F G).IsFibered

CategoryTheory.TwoFibreProductOver.fst_isFibredOneMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedCategory/TwoFibreProduct.lean, line 238.

Stacks 02XQ, first projection. Under the hypotheses of TwoFibreProductOver.isFibered_structureFunctor, the first projection π₁ is a 1-morphism of fibred categories over 𝒞: it is strictly over 𝒞 and preserves strongly cartesian morphisms.

theorem TwoFibreProductOver.fst_isFibredOneMorphism
    (p𝒳 : 𝒳 ⥤ 𝒞) (p𝒴 : 𝒴 ⥤ 𝒞) (p𝒮 : 𝒮 ⥤ 𝒞) (F : 𝒳 ⥤ 𝒮) (G : 𝒴 ⥤ 𝒮)
    [p𝒳.IsFibered] [p𝒴.IsFibered] [p𝒮.IsFibered]
    (hF : Functor.IsFibredOneMorphism p𝒳 p𝒮 F)
    (hG : Functor.IsFibredOneMorphism p𝒴 p𝒮 G) :
    Functor.IsFibredOneMorphism (TwoFibreProductOver.structureFunctor p𝒳 p𝒴 p𝒮 F G) p𝒳
      (TwoFibreProductOver.fst p𝒳 p𝒴 p𝒮 F G)

CategoryTheory.TwoFibreProductOver.snd_isFibredOneMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedCategory/TwoFibreProduct.lean, line 254.

Stacks 02XQ, second projection. Under the hypotheses of TwoFibreProductOver.isFibered_structureFunctor, the second projection π₂ is a 1-morphism of fibred categories over 𝒞.

theorem TwoFibreProductOver.snd_isFibredOneMorphism
    (p𝒳 : 𝒳 ⥤ 𝒞) (p𝒴 : 𝒴 ⥤ 𝒞) (p𝒮 : 𝒮 ⥤ 𝒞) (F : 𝒳 ⥤ 𝒮) (G : 𝒴 ⥤ 𝒮)
    [p𝒳.IsFibered] [p𝒴.IsFibered] [p𝒮.IsFibered]
    (hF : Functor.IsFibredOneMorphism p𝒳 p𝒮 F)
    (hG : Functor.IsFibredOneMorphism p𝒴 p𝒮 G) :
    Functor.IsFibredOneMorphism (TwoFibreProductOver.structureFunctor p𝒳 p𝒴 p𝒮 F G) p𝒴
      (TwoFibreProductOver.snd p𝒳 p𝒴 p𝒮 F G)
Tag 02XR, a lemma

Tag 02XR in the Stacks Project.

CategoryTheory.Functor.IsFibered.of_comp_over, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedCategory/Slice.lean, line 94.

If a fibred category p : S ⥤ C factors as p' ⋙ Over.forget U through the slice category Over U, then p' : S ⥤ Over U is a fibred category.

theorem IsFibered.of_comp_over (p : S ⥤ C)
    [p.IsFibered] (h : p' ⋙ Over.forget U = p) :
    p'.IsFibered
Tag 09WV, a lemma

Tag 09WV in the Stacks Project.

CategoryTheory.Functor.IsFibered.comp_functor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedCategory/CompFibered.lean, line 34.

A composite of fibred functors is fibred: if F : A ⥤ B and G : B ⥤ C are fibred, then so is F ⋙ G.

theorem IsFibered.comp_functor (F : A ⥤ B) (G : B ⥤ C)
    [F.IsFibered] [G.IsFibered] : (F ⋙ G).IsFibered
Tag 06N5, a lemma

Tag 06N5 in the Stacks Project.

CategoryTheory.Functor.IsFibered.hasPullback_of_isStronglyCartesian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedCategory/FibreProducts.lean, line 96.

Stacks 06N5, existence half. In a fibred category p : 𝒮 ⥤ 𝒞, if φ : x ⟶ y is strongly cartesian over p and the fibre product of p φ and p g exists in 𝒞, then the fibre product of φ and g exists in 𝒮.

theorem Functor.IsFibered.hasPullback_of_isStronglyCartesian
    (p : 𝒮 ⥤ 𝒞) [p.IsFibered]
    {x y z : 𝒮} (φ : x ⟶ y) (g : z ⟶ y)
    [Functor.IsStronglyCartesian p (p.map φ) φ]
    [Limits.HasPullback (p.map φ) (p.map g)] :
    Limits.HasPullback φ g

CategoryTheory.Functor.IsFibered.snd_isStronglyCartesian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedCategory/FibreProducts.lean, line 111.

Stacks 06N5, second projection strongly cartesian. Under the same hypotheses the second projection Limits.pullback.snd φ g : x ×_y z ⟶ z is strongly cartesian over p, since it is the canonical isomorphism x ×_y z ≅ w followed by the strongly cartesian morphism a.

theorem Functor.IsFibered.snd_isStronglyCartesian
    (p : 𝒮 ⥤ 𝒞) [p.IsFibered]
    {x y z : 𝒮} (φ : x ⟶ y) (g : z ⟶ y)
    [Functor.IsStronglyCartesian p (p.map φ) φ]
    [Limits.HasPullback (p.map φ) (p.map g)]
    [Limits.HasPullback φ g] :
    Functor.IsStronglyCartesian p
      (p.map (Limits.pullback.snd φ g)) (Limits.pullback.snd φ g)

CategoryTheory.Functor.IsFibered.map_isPullback_of_isStronglyCartesian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedCategory/FibreProducts.lean, line 131.

Stacks 06N5, image square is a fibre product square. Under the same hypotheses p sends the fibre product square of φ, g in 𝒮 to a fibre product square in 𝒞: the image p (x ×_y z), with the images of the two projections, is the fibre product of p φ and p g.

theorem Functor.IsFibered.map_isPullback_of_isStronglyCartesian
    (p : 𝒮 ⥤ 𝒞) [p.IsFibered]
    {x y z : 𝒮} (φ : x ⟶ y) (g : z ⟶ y)
    [Functor.IsStronglyCartesian p (p.map φ) φ]
    [Limits.HasPullback (p.map φ) (p.map g)]
    [Limits.HasPullback φ g] :
    IsPullback (p.map (Limits.pullback.fst φ g)) (p.map (Limits.pullback.snd φ g))
      (p.map φ) (p.map g)
Tag 08NF, a lemma

Tag 08NF in the Stacks Project.

CategoryTheory.Functor.IsFibered.exists_amelioration, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedCategory/Amelioration.lean, line 770.

Stacks 4.33.14 / 08NF. Let F : X ⥤ Y be a 1-morphism of fibred categories over C, with structure functors p : X ⥤ C and q : Y ⥤ C. Then there exist a fibred category (X', p'') over C and three 1-morphisms of fibred categories over C

u : X ⥤ X', v : X' ⥤ Y, w : X' ⥤ X,

with F = u ⋙ v such that 1. u is fully faithful; 2. w is left adjoint to u; and 3. v exhibits X' as a fibred category over Y (v.IsFibered), the structure functor of X' over C factoring as p'' = v ⋙ q.

The witness category X' is stated in the universe max u₁ u₂ u₃ v₁ v₂ v₃ so as to accommodate the explicit construction, in which an object carries a morphism of Y (living in the hom universe v₃). It is the amelioration Amelioration p q F hFq of F, moved into that universe by exists_amelioration_uliftHom.

theorem Functor.IsFibered.exists_amelioration
    {C : Type u₁} [Category.{v₁} C]
    {X : Type u₂} [Category.{v₂} X]
    {Y : Type u₃} [Category.{v₃} Y]
    (p : X ⥤ C) (q : Y ⥤ C) [p.IsFibered] [q.IsFibered]
    (F : X ⥤ Y) (hF : Functor.IsFibredOneMorphism p q F) :
    ∃ (X' : Type (max u₁ u₂ u₃ v₁ v₂ v₃)) (_ : Category.{max v₁ v₂ v₃} X')
      (p'' : X' ⥤ C) (_ : p''.IsFibered)
      (u : X ⥤ X') (v : X' ⥤ Y) (w : X' ⥤ X),
        -- the three functors are 1-morphisms of fibred categories over C
        Functor.IsFibredOneMorphism p p'' u ∧
        Functor.IsFibredOneMorphism p'' q v ∧
        Functor.IsFibredOneMorphism p'' p w ∧
        -- F factors as u ⋙ v
        F = u ⋙ v ∧
        -- the structure functor of X' over C factors through Y as p'' = v ⋙ q
        p'' = v ⋙ q ∧
        -- (1) u is fully faithful
        Nonempty u.FullyFaithful ∧
        -- (2) w is left adjoint to u
        Nonempty (w ⊣ u) ∧
        -- (3) v exhibits X' as a fibred category over Y
        v.IsFibered
Sources
LeanStacks.StronglyCartesian.isStronglyCartesian_conditions_hold · CategoryTheory.Functor.IsStronglyCartesian.comp_functor · CategoryTheory.hasPullback_of_isStronglyCartesian · CategoryTheory.pullbackIsoOfIsStronglyCartesian · CategoryTheory.Functor.IsFibredCategory · CategoryTheory.Functor.isFibredCategory_iff_isFibered · CategoryTheory.Functor.IsFibered · CategoryTheory.Functor.ChoiceOfPullbacks

Section4.34 Inertia#

Section 4.34 of the Stacks Project, Tag 04Z2. 3 tags here are carried by 5 declarations of the repository (1 in StacksCore and 4 in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 034H, a lemma

Tag 034H in the Stacks Project.

CategoryTheory.RelativeInertia.diagonalPullbackEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedCategory/InertiaDiagonal.lean, line 333. The attribute's comment: “(1)”.

The comparison functor Φ : I_{S/S'} ⥤ Δ ⊡ Δ is an equivalence of categories, with explicit quasi-inverse Ψ, unit coming from the equality Ψ ∘ Φ = 𝟭 and counit the isomorphism with component (id, κ).

def diagonalPullbackEquivalence (F : S ⥤ S') :
    RelativeInertia F ≌ CategoricalPullback (diagonal F) (diagonal F)

Declarations registered for the tag:

Tag 034I, a definition

Tag 034I in the Stacks Project.

CategoryTheory.RelativeInertia, a structure in StacksCore (human-reviewed), declared in StacksCore/CategoryTheory/Inertia.lean, line 72.

Stacks 034I. An object of the relative inertia category I_{S/S'} for a functor F : S ⥤ S': a pair (x, α) with α : Aut x such that F(α) = id_{F(x)}. The relative inertia I_{S/S'} (and the absolute inertia I_S = I_{S/C}) is the fibred category built from this structure.

structure RelativeInertia (F : S ⥤ S')
Tag 04Z6, a lemma

Tag 04Z6 in the Stacks Project.

CategoryTheory.RelativeInertia.isEquivalenceOver_toFibreProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedCategory/InertiaSquare.lean, line 450.

Stacks 04Z6. The 2-commutative square 

  I_{S/S'} --c--> I_S
     |             |
  F∘π |            | I_F
     v             v
     S' ---e---> I_{S'}
is a 2-fibre product in the (2,1)-category of fibred categories over C: the canonical comparison 1-morphism Θ to the explicit 2-fibre product S' ×_{e, I_{S'}, I_F} I_S is an equivalence of categories over C.

The witness produced has Θ itself as its underlying functor, so the statement is about the given comparison functor with its prescribed action on objects and morphisms, and not merely about the existence of some equivalence.

theorem isEquivalenceOver_toFibreProduct :
    Nonempty (IsEquivalenceOver (RelativeInertia.π F ⋙ p)
      (FibreProduct.structureFunctor p p' F hF) (toFibreProduct p p' F hF))

CategoryTheory.RelativeInertia.toFibreProduct_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedCategory/InertiaSquare.lean, line 466.

Consequence of Stacks 04Z6: the comparison functor Θ is an equivalence of the underlying categories.

theorem toFibreProduct_isEquivalence :
    (toFibreProduct p p' F hF).IsEquivalence

CategoryTheory.RelativeInertia.squareTwoCommutes, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedCategory/InertiaSquare.lean, line 476.

Stacks 04Z6, the square. The 2-commutativity of the square is witnessed by a natural isomorphism over C, I_F ∘ c ≅ e ∘ (F ∘ π). On an object (x, α) both composites are (F x, id), since F α = id, so the canonical 2-isomorphism is the identity.

def squareTwoCommutes :
    (comparison p p' F hF) ⋙ (functoriality p p' F hF)
      ≅ (RelativeInertia.π F ⋙ F) ⋙ (neutralSection p')
Sources
LeanCategoryTheory.RelativeInertia.diagonalPullbackEquivalence · CategoryTheory.RelativeInertia.isFibered · CategoryTheory.RelativeInertia · CategoryTheory.RelativeInertia.isEquivalenceOver_toFibreProduct · CategoryTheory.RelativeInertia.toFibreProduct_isEquivalence · CategoryTheory.RelativeInertia.squareTwoCommutes

Section4.35 Categories fibred in groupoids#

Section 4.35 of the Stacks Project, Tag 003S. 14 tags here are carried by 20 declarations of the repository (1 in StacksCore and 19 in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 03WP, an equation

Tag 03WP in the Stacks Project.

CategoryTheory.Functor.IsFiberedInGroupoids.existsUnique_vertical_factorisation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedInGroupoids/Lifts.lean, line 52.

Stacks 03WP. The two-step lift ψ ∘ φ : z ⟶ x of g ∘ f factors through the direct lift γ : z' ⟶ x by a unique morphism χ : z ⟶ z' of the fibre over W, i.e. a unique χ lying over id_W.

theorem existsUnique_vertical_factorisation :
    ∃! χ : z ⟶ z', p.IsHomLift (𝟙 W) χ ∧ χ ≫ γ = ψ ≫ φ

CategoryTheory.Functor.IsFiberedInGroupoids.twoStepLiftIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedInGroupoids/Lifts.lean, line 62.

Stacks 03WP. The comparison isomorphism z ≅ z' between the domain of the two-step lift of g ∘ f and the domain of a direct lift of g ∘ f. Both lifts are cartesian, so this is the canonical isomorphism between the domains of two cartesian lifts of one morphism of the base.

noncomputable def twoStepLiftIso : z ≅ z'

CategoryTheory.Functor.IsFiberedInGroupoids.isIso_of_vertical_comp_eq, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedInGroupoids/Lifts.lean, line 83.

Stacks 03WP. Every morphism χ : z ⟶ z' of the fibre over W filling the diagram is an isomorphism: by uniqueness it is the comparison isomorphism CategoryTheory.Functor.twoStepLiftIso.

lemma isIso_of_vertical_comp_eq (χ : z ⟶ z') [p.IsHomLift (𝟙 W) χ] (hχ : χ ≫ γ = ψ ≫ φ) :
    IsIso χ
Tag 003V, a lemma

Tag 003V in the Stacks Project.

CategoryTheory.Functor.IsFiberedInGroupoids.iff_isFibered_and_fiber_isGroupoid, a theorem in StacksCore (human-reviewed), declared in StacksCore/CategoryTheory/FiberedInGroupoidsEquiv.lean, line 165.

Stacks 003V (Lemma 4.35.2). A functor p : 𝒮 ⥤ 𝒞 is fibred in groupoids if and only if it is a fibred category all of whose fibres are groupoids.

theorem iff_isFibered_and_fiber_isGroupoid :
    p.IsFiberedInGroupoids ↔ p.IsFibered ∧ ∀ S, IsGroupoid (p.Fiber S)
Tag 03WQ, a lemma

Tag 03WQ in the Stacks Project.

stronglyCartesianOver_isMultiplicative, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedInGroupoids/MultiplicativeClass.lean, line 96. References: SGA 1 VI (6.13); SGA 1 VI (6.8), “Well-definedness of F̃”; SGA 4 VI (6.4), “Fr1”.

Stacks tag 03WQ (auxiliary multiplicativity). The morphism property stronglyCartesianOver p (strongly cartesian morphisms over their image) contains identities and is closed under composition — this is the content of the first sentence of the Stacks proof, namely that the subcategory 𝒮' of strongly cartesian morphisms is well-defined as a subcategory.

theorem stronglyCartesianOver_isMultiplicative
    {𝒞 : Type*} [Category 𝒞] {𝒮 : Type*} [Category 𝒮]
    (p : 𝒮 ⥤ 𝒞) [p.IsFibered] :
    (stronglyCartesianOver p).IsMultiplicative
Tag 02XS, a definition

Tag 02XS in the Stacks Project.

CategoryTheory.CatFiberedInGroupoids, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedInGroupoids/TwoCategory.lean, line 116.

The 2-category of categories fibred in groupoids over 𝒞: the full sub-2-category of the 2-category BasedCategory 𝒞 of categories over 𝒞 (Stacks 003Y) spanned by the categories fibred in groupoids. Explicitly:

  1. its objects are the categories p : 𝒮 ⥤ 𝒞 over 𝒞 that are fibred in groupoids;
  2. its 1-morphisms (𝒮, p) ⟶ (𝒮', p') are the functors G : 𝒮 ⥤ 𝒮' with p' ∘ G = p (no condition on strongly cartesian morphisms is needed: see CatFiberedInGroupoids.isStronglyCartesian_map);
  3. its 2-morphisms t : G ⟶ H are the morphisms of functors with p'(t_x) = 𝟙 (p x) for every object x of 𝒮.
abbrev CatFiberedInGroupoids (𝒞 : Type u₁) [Category.{v₁} 𝒞]
Tag 0041, a lemma

Tag 0041 in the Stacks Project.

CategoryTheory.TwoFibreProductOver.isFiberedInGroupoids, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedInGroupoids/TwoFibreProduct.lean, line 132.

Stacks 0041. The 2-category of categories fibred in groupoids over 𝒞 has 2-fibre products, given by the construction of Stacks 0040: if p𝒳, p𝒴, p𝒮 are fibred in groupoids and F, G are strictly over 𝒞, then the structure functor of 𝒳 ×_𝒮 𝒴 is fibred in groupoids.

theorem isFiberedInGroupoids (p𝒳 : 𝒳 ⥤ 𝒞) (p𝒴 : 𝒴 ⥤ 𝒞) (p𝒮 : 𝒮 ⥤ 𝒞) (F : 𝒳 ⥤ 𝒮) (G : 𝒴 ⥤ 𝒮)
    (h𝒳 : p𝒳.IsFiberedInGroupoids) (h𝒴 : p𝒴.IsFiberedInGroupoids)
    (h𝒮 : p𝒮.IsFiberedInGroupoids) (hF : F ⋙ p𝒮 = p𝒳) (hG : G ⋙ p𝒮 = p𝒴) :
    (structureFunctor p𝒳 p𝒴 p𝒮 F G).IsFiberedInGroupoids
Tag 003Z, a lemma

Tag 003Z in the Stacks Project.

CategoryTheory.Functor.IsFiberedInGroupoids.faithful_iff_forall_fiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedInGroupoids/Fibrewise.lean, line 207. The attribute's comment: “(1)”. References: SGA 1 VI (6.10), “fibred in groupoids”.

Stacks 003Z (1). G is faithful if and only if for every object U of C the induced functor G_U : S_U ⥤ S'_U on fibres is faithful.

theorem IsFiberedInGroupoids.faithful_iff_forall_fiber (p : S ⥤ C) (p' : S' ⥤ C)
    (hp : p.IsFiberedInGroupoids) (hp' : p'.IsFiberedInGroupoids) (G : S ⥤ S')
    (hG : G ⋙ p' = p) : G.Faithful ↔ ∀ U : C, (Fiber.mapOfComp p p' G hG U).Faithful

CategoryTheory.Functor.IsFiberedInGroupoids.full_and_faithful_iff_forall_fiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedInGroupoids/Fibrewise.lean, line 216. The attribute's comment: “(1)”. References: SGA 1 VI (6.10), “fibred in groupoids”.

Stacks 003Z (1). G is full and faithful if and only if for every object U of C the induced functor G_U : S_U ⥤ S'_U on fibres is full and faithful.

theorem IsFiberedInGroupoids.full_and_faithful_iff_forall_fiber (p : S ⥤ C) (p' : S' ⥤ C)
    (hp : p.IsFiberedInGroupoids) (hp' : p'.IsFiberedInGroupoids) (G : S ⥤ S')
    (hG : G ⋙ p' = p) : (G.Full ∧ G.Faithful) ↔
      ∀ U : C, ((Fiber.mapOfComp p p' G hG U).Full ∧ (Fiber.mapOfComp p p' G hG U).Faithful)

CategoryTheory.Functor.IsFiberedInGroupoids.isEquivalence_iff_forall_fiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedInGroupoids/Fibrewise.lean, line 279. The attribute's comment: “(1)”. References: SGA 1 VI (6.10), “fibred in groupoids”; SGA 1 VI (4.2), “(iii)”.

Stacks 003Z (1). G is an equivalence of categories if and only if for every object U of C the induced functor G_U : S_U ⥤ S'_U on fibres is an equivalence.

theorem IsFiberedInGroupoids.isEquivalence_iff_forall_fiber (p : S ⥤ C) (p' : S' ⥤ C)
    (hp : p.IsFiberedInGroupoids) (hp' : p'.IsFiberedInGroupoids) (G : S ⥤ S')
    (hG : G ⋙ p' = p) :
    G.IsEquivalence ↔ ∀ U : C, (Fiber.mapOfComp p p' G hG U).IsEquivalence

CategoryTheory.Functor.IsFiberedInGroupoids.isEquivalence_over, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedInGroupoids/Fibrewise.lean, line 367. The attribute's comment: “(2)”.

Stacks 003Z (2). If G is an equivalence of categories, then G is an equivalence in the 2-category of categories fibred in groupoids over C: there are a functor F : S' ⥤ S over C (that is, F ⋙ p = p') and natural isomorphisms G ⋙ F ≅ 𝟭 S and F ⋙ G ≅ 𝟭 S' all of whose components lie over identity morphisms of C.

theorem IsFiberedInGroupoids.isEquivalence_over (p : S ⥤ C) (p' : S' ⥤ C)
    (hp : p.IsFiberedInGroupoids) (hp' : p'.IsFiberedInGroupoids)
    (G : S ⥤ S') (hG : G ⋙ p' = p) (hGequiv : G.IsEquivalence) :
    ∃ (F : S' ⥤ S) (_ : F ⋙ p = p') (η : G ⋙ F ≅ 𝟭 S) (ε : F ⋙ G ≅ 𝟭 S'),
      (∀ x : S, p.IsHomLift (𝟙 (p.obj x)) (η.hom.app x)) ∧
      (∀ x' : S', p'.IsHomLift (𝟙 (p'.obj x')) (ε.hom.app x'))
Tag 04Z7, a lemma

Tag 04Z7 in the Stacks Project.

CategoryTheory.TwoFibreProductOver.full_and_faithful_iff_isEquivalence_diagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedInGroupoids/Diagonal.lean, line 252.

Stacks 04Z7. Let p𝒮 : 𝒮 ⥤ 𝒞 and p𝒮' : 𝒮' ⥤ 𝒞 be categories fibred in groupoids and let G : 𝒮 ⥤ 𝒮' be a 1-morphism over 𝒞. Then G is fully faithful if and only if the diagonal Δ_G : 𝒮 ⥤ 𝒮 ×_{G, 𝒮', G} 𝒮 is an equivalence.

theorem full_and_faithful_iff_isEquivalence_diagonal (h𝒮 : p𝒮.IsFiberedInGroupoids)
    (h𝒮' : p𝒮'.IsFiberedInGroupoids) (hG : G ⋙ p𝒮' = p𝒮) :
    (G.Full ∧ G.Faithful) ↔ (diagonal hG).IsEquivalence
Tag 03YT, a lemma

Tag 03YT in the Stacks Project.

main_theorem03YT, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedInGroupoids/Conjugation.lean, line 132. References: SGA 1 VI (4.5), “both displayed maps”.

Stacks 03YT. For 𝒮₁, …, 𝒮₄ over 𝒞 and equivalences φ : 𝒮₁ ⟶ 𝒮₂, ψ : 𝒮₃ ⟶ 𝒮₄ over 𝒞, conjugation α ↦ ψ ∘ α ∘ φ is an equivalence of hom-categories Mor_{Cat/𝒞}(𝒮₂, 𝒮₃) ⥤ Mor_{Cat/𝒞}(𝒮₁, 𝒮₄).

The source additionally assumes each 𝒮ᵢ is fibred in groupoids over 𝒞. Conjugation by equivalences is an equivalence in any bicategory, so that hypothesis is unused; it is omitted here and the statement proved is correspondingly more general than the tag.

theorem main_theorem03YT
    (𝒮₁ 𝒮₂ 𝒮₃ 𝒮₄ : BasedCategory 𝒞)
    (eφ : Bicategory.Equivalence 𝒮₁ 𝒮₂)
    (eψ : Bicategory.Equivalence 𝒮₃ 𝒮₄) :
    (conjugationFunctor eφ.hom eψ.hom).IsEquivalence
Tag 042I, a lemma

Tag 042I in the Stacks Project.

CategoryTheory.Functor.IsFiberedInGroupoids.absoluteInertia, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedInGroupoids/Inertia.lean, line 59.

Stacks 042I. If p : S ⥤ C is fibred in groupoids, then so is the inertia fibred category I_S ⥤ C.

theorem absoluteInertia (p : S ⥤ C) (hp : p.IsFiberedInGroupoids) :
    (relativeInertiaStruct p p).IsFiberedInGroupoids
Tag 02XT, a lemma

Tag 02XT in the Stacks Project.

CategoryTheory.Functor.IsFiberedInGroupoids.of_comp_over, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedInGroupoids/Slice.lean, line 89.

Stacks 02XT. If p : 𝒮 ⥤ 𝒞 is fibred in groupoids and factors through the slice category Over U as p' ⋙ Over.forget U = p, then p' : 𝒮 ⥤ Over U is fibred in groupoids: lifts of morphisms of Over U and unique fill-ins for p' are obtained from those for p, because the structure morphism of a lifted object is forced and Over.forget U is faithful.

theorem IsFiberedInGroupoids.of_comp_over
    {𝒮 𝒞 : Type*} [Category 𝒮] [Category 𝒞] (U : 𝒞)
    (p : 𝒮 ⥤ 𝒞) (p' : 𝒮 ⥤ Over U)
    (h : p' ⋙ Over.forget U = p) (hp : p.IsFiberedInGroupoids) :
    p'.IsFiberedInGroupoids
Tag 09WW, a lemma

Tag 09WW in the Stacks Project.

CategoryTheory.Functor.IsFiberedInGroupoids.comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedInGroupoids/Comp.lean, line 50.

Stacks 09WW. The composition of two functors that are fibred in groupoids is fibred in groupoids.

theorem IsFiberedInGroupoids.comp (p : 𝒜 ⥤ ℬ) (q : ℬ ⥤ 𝒞)
    (hp : p.IsFiberedInGroupoids) (hq : q.IsFiberedInGroupoids) :
    (p ⋙ q).IsFiberedInGroupoids
Tag 06N6, a lemma

Tag 06N6 in the Stacks Project.

CategoryTheory.Functor.IsFiberedInGroupoids.hasPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedInGroupoids/FibreProducts.lean, line 132. The attribute's comment: “(1)”.

Let p be fibred in groupoids and let gx : x ⟶ y, gz : z ⟶ y be morphisms of S. If the fibre product of p.map gx and p.map gz exists in C, then the fibre product of gx and gz exists in S.

theorem IsFiberedInGroupoids.hasPullback
    (p : S ⥤ C) (hp : p.IsFiberedInGroupoids)
    {x y z : S} (gx : x ⟶ y) (gz : z ⟶ y)
    [Limits.HasPullback (p.map gx) (p.map gz)] :
    Limits.HasPullback gx gz

CategoryTheory.Functor.IsFiberedInGroupoids.map_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedInGroupoids/FibreProducts.lean, line 145. The attribute's comment: “(2)”.

For any fibre product x ×_y z in S, realized by a pullback square with vertex P and projections pr₁ : P ⟶ x, pr₂ : P ⟶ z, the image p.obj P together with p.map pr₁ and p.map pr₂ is a fibre product of p.map gx and p.map gz in C: p carries the pullback square of S to a pullback square of C.

theorem IsFiberedInGroupoids.map_isPullback
    (p : S ⥤ C) (hp : p.IsFiberedInGroupoids)
    {x y z : S} (gx : x ⟶ y) (gz : z ⟶ y)
    [Limits.HasPullback (p.map gx) (p.map gz)]
    {P : S} (pr₁ : P ⟶ x) (pr₂ : P ⟶ z)
    (hP : IsPullback pr₁ pr₂ gx gz) :
    IsPullback (p.map pr₁) (p.map pr₂) (p.map gx) (p.map gz)
Tag 06N7, a lemma

Tag 06N7 in the Stacks Project.

CategoryTheory.Functor.IsFiberedInGroupoids.exists_factorization_isFiberedInGroupoids, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedInGroupoids/Factorization.lean, line 450.

Stacks 06N7 (Lemma 4.35.16). Let 𝒞 be a category and let 𝒳, 𝒴 be categories fibred in groupoids over 𝒞 via p : 𝒳 ⥤ 𝒞 and q : 𝒴 ⥤ 𝒞. Let F : 𝒳 ⥤ 𝒴 be a 1-morphism over 𝒞 (F ⋙ q = p). Then there exist a category 𝒳', a structure functor r : 𝒳' ⥤ 𝒞 and functors a : 𝒳 ⥤ 𝒳', t : 𝒳' ⥤ 𝒴 such that

  1. r is fibred in groupoids over 𝒞;
  2. a is a 1-morphism over 𝒞 (a ⋙ r = p) and an equivalence over 𝒞;
  3. t is a 1-morphism over 𝒞 (t ⋙ q = r) and is fibred in groupoids over 𝒴;
  4. a ⋙ t = F.
theorem IsFiberedInGroupoids.exists_factorization_isFiberedInGroupoids
    {𝒞 : Type u₂} [Category.{v₂} 𝒞]
    {𝒳 : Type u₁} [Category.{v₁} 𝒳] (p : 𝒳 ⥤ 𝒞) (hp : p.IsFiberedInGroupoids)
    {𝒴 : Type u₃} [Category.{v₃} 𝒴] (q : 𝒴 ⥤ 𝒞) (hq : q.IsFiberedInGroupoids)
    (F : 𝒳 ⥤ 𝒴) (hF : F ⋙ q = p) :
    ∃ (𝒳' : Type (max u₁ u₃ v₁ v₃)) (_ : Category.{max v₁ v₃} 𝒳')
      (r : 𝒳' ⥤ 𝒞) (a : 𝒳 ⥤ 𝒳') (t : 𝒳' ⥤ 𝒴),
      r.IsFiberedInGroupoids ∧
      (a ⋙ r = p) ∧ Nonempty (IsEquivalenceOver p r a) ∧
      (t ⋙ q = r) ∧ t.IsFiberedInGroupoids ∧
      (a ⋙ t = F)
Tag 06N8, a lemma

Tag 06N8 in the Stacks Project.

amelioration_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedInGroupoids/AmeliorationUniqueness.lean, line 42.

Stacks 06N8 (uniqueness of the factorization of 4.35.16 / 06N7).

Let F : 𝒳 ⥤ 𝒴 be a 1-morphism of categories fibred in groupoids over 𝒞. Suppose F is factored in two ways through categories fibred in groupoids over 𝒞: 𝒳 ⟶[a] 𝒳' ⟶[f] 𝒴 and 𝒳 ⟶[b] 𝒳'' ⟶[g] 𝒴, where

  • a, b are equivalences (over 𝒞);
  • the two factorizations agree with F: a ⋙ f ≅ F and b ⋙ g ≅ F.

Then there is an equivalence h : 𝒳'' ⥤ 𝒳' over 𝒴 (i.e. h.IsEquivalence together with h ⋙ f ≅ g) such that b ⋙ h ≅ a. In particular the intermediate category is unique up to equivalence over 𝒴, compatibly with the first legs.

The conclusion uses none of the remaining data of 06N8 — the structure functors p : 𝒳 ⥤ 𝒞, q : 𝒴 ⥤ 𝒞, p' : 𝒳' ⥤ 𝒞, p'' : 𝒳'' ⥤ 𝒞, their fiberedness in groupoids, that of f and g, and the compatibilities a ⋙ p' = p, b ⋙ p'' = p, f ⋙ q = p', g ⋙ q = p'' — so it is stated in the general form below, which specializes to 06N8 in the fibred setting.

theorem amelioration_unique
    {𝒞 : Type u₁} [Category.{v₁} 𝒞]
    {𝒳 : Type u₂} [Category.{v₂} 𝒳]
    {𝒴 : Type u₃} [Category.{v₃} 𝒴]
    {𝒳' : Type u₄} [Category.{v₄} 𝒳']
    {𝒳'' : Type u₅} [Category.{v₅} 𝒳'']
    (F : 𝒳 ⥤ 𝒴) (a : 𝒳 ⥤ 𝒳') (b : 𝒳 ⥤ 𝒳'')
    (f : 𝒳' ⥤ 𝒴) (g : 𝒳'' ⥤ 𝒴)
    (ha_equiv : a.IsEquivalence) (hb_equiv : b.IsEquivalence)
    (hleft : a ⋙ f ≅ F) (hright : b ⋙ g ≅ F) :
    ∃ (h : 𝒳'' ⥤ 𝒳') (_ : h.IsEquivalence) (_ : h ⋙ f ≅ g),
      Nonempty (b ⋙ h ≅ a)
Sources
LeanCategoryTheory.Functor.IsFiberedInGroupoids.existsUnique_vertical_factorisation · CategoryTheory.Functor.IsFiberedInGroupoids.twoStepLiftIso · CategoryTheory.Functor.IsFiberedInGroupoids.isIso_of_vertical_comp_eq · CategoryTheory.Functor.IsFiberedInGroupoids.iff_isFibered_and_fiber_isGroupoid · stronglyCartesianOver_isMultiplicative · CategoryTheory.CatFiberedInGroupoids · CategoryTheory.TwoFibreProductOver.isFiberedInGroupoids · CategoryTheory.Functor.IsFiberedInGroupoids.faithful_iff_forall_fiber

Section4.36 Presheaves of categories#

Section 4.36 of the Stacks Project, Tag 02XU. 4 tags here are carried by 8 declarations of the repository (all in StacksFrontier) and 4 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 02XV, an example

Tag 02XV in the Stacks Project.

CategoryTheory.presheafOfCategories, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedCategory/OfPresheaf.lean, line 87.

Stacks 02XV. The category 𝒮_F attached to a presheaf of categories F : 𝒞ᵒᵖ ⥤ Cat, together with its projection p_F : 𝒮_F ⥤ 𝒞, as an object of the 2-category of categories over 𝒞.

abbrev presheafOfCategories (F : 𝒞ᵒᵖ ⥤ Cat.{v₂, u₂}) : BasedCategory 𝒞

CategoryTheory.PresheafOfCategories.objEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedCategory/OfPresheaf.lean, line 108.

Stacks 02XV. Ob(𝒮_F) = {(U, x) | U ∈ Ob(𝒞), x ∈ Ob(F(U))}.

def objEquiv : ∫ᶜ F.toPseudofunctor' ≃ Σ U : 𝒞, F.obj (op U)

CategoryTheory.PresheafOfCategories.homEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedCategory/OfPresheaf.lean, line 117.

Stacks 02XV. Mor_{𝒮_F}((V, y), (U, x)) is the disjoint union over f : V ⟶ U of Mor_{F(V)}(y, f^* x).

def homEquiv (X Y : ∫ᶜ F.toPseudofunctor') :
    (X ⟶ Y) ≃ Σ f : X.base ⟶ Y.base, (X.fiber ⟶ (F.map f.op).toFunctor.obj Y.fiber)

CategoryTheory.PresheafOfCategories.comp_fiber, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedCategory/OfPresheaf.lean, line 128.

Stacks 02XV. The composition of 𝒮_F is the source's: the composite of ψ : z ⟶ g^* y with φ : y ⟶ f^* x is g^*(φ) ∘ ψ, read as a morphism z ⟶ (f ∘ g)^* x through pullback_comp_obj.

lemma comp_fiber {X Y Z : ∫ᶜ F.toPseudofunctor'} (u : X ⟶ Y) (v : Y ⟶ Z) :
    (u ≫ v).fiber = u.fiber ≫ (F.map u.base.op).toFunctor.map v.fiber ≫
      eqToHom (pullback_comp_obj F u.base v.base Z.fiber)

CategoryTheory.PresheafOfCategories.isFibered, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedCategory/OfPresheaf.lean, line 142. References: SGA 4 VI (6.1.3), “strict functor case”.

Stacks 02XV. The projection p_F : 𝒮_F ⥤ 𝒞 is a fibred category.

This bridge is load-bearing: instance resolution does not see Mathlib's CoGrothendieck.instIsFiberedForget through BasedCategory.ofFunctor's projection, so infer_instance fails on this goal without it.

instance isFibered : (presheafOfCategories F).p.IsFibered

Declarations registered for the tag:

Tag 02XW, a definition

Tag 02XW in the Stacks Project.

CategoryTheory.Functor.IsSplitFibered, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedCategory/Split.lean, line 43.

Stacks 02XW. A split fibred category over 𝒞 is a fibred category p : 𝒮 ⥤ 𝒞 that is isomorphic over 𝒞 to the fibred category 𝒮_F attached to some presheaf of categories F : 𝒞ᵒᵖ ⥤ Cat (Stacks 02XV). The source is explicit that isomorphism over 𝒞, and not merely equivalence over 𝒞, is meant.

def Functor.IsSplitFibered (p : 𝒮 ⥤ 𝒞) : Prop
Tag 02XX, a lemma

Tag 02XX in the Stacks Project.

CategoryTheory.Functor.isSplitFibered_iff_exists_isSplitCleavage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedCategory/Splitting.lean, line 847.

Stacks 02XX, with the source's condition on a choice of pullbacks replaced by CategoryTheory.Functor.ChoiceOfPullbacks.IsSplitCleavage: a fibred category is split (Stacks 02XW) if and only if some choice of pullbacks (Stacks 02XN) has its two canonical comparisons of Stacks 02XN equal to identities, i.e. has chosen cartesian lifts strictly compatible with identities and composition.

The source states the condition on the pullback functors, as (f ∘ g)^* = g^* ∘ f^*, and that biconditional is false: see the module docstring, and the two counterexamples CategoryTheory.SplittingCounterexample.compatibleWithComp_not_isSplitting and CategoryTheory.SplitCleavageCounterexample.isSplitting_not_isSplitFibered in StacksFrontier/CategoryTheory/FiberedCategory/SplittingCounterexample.lean.

theorem Functor.isSplitFibered_iff_exists_isSplitCleavage {p : 𝒳 ⥤ 𝒮} :
    p.IsSplitFibered ↔ ∃ c : p.ChoiceOfPullbacks, c.IsSplitCleavage
Tag 004A, a lemma

Tag 004A in the Stacks Project.

CategoryTheory.Functor.exists_isFibredEquivalenceOver_presheafOfCategories, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedCategory/Strictification.lean, line 916.

Stacks 004A. Every fibred category p : 𝒳 ⥤ 𝒞 is equivalent, in the 2-category of fibred categories over 𝒞, to the category 𝒮_F (Stacks 02XV, CategoryTheory.presheafOfCategories) attached to a contravariant functor F : 𝒞 ⥤ Cat; in other words, every fibred category is equivalent to a split one.

theorem exists_isFibredEquivalenceOver_presheafOfCategories :
    ∃ (F : 𝒞ᵒᵖ ⥤ Cat.{v₂, max u₁ u₂ v₁}) (Φ : 𝒳 ⥤ (presheafOfCategories F).obj),
      IsFibredEquivalenceOver p (presheafOfCategories F).p Φ
Sources
LeanCategoryTheory.presheafOfCategories · CategoryTheory.PresheafOfCategories.objEquiv · CategoryTheory.PresheafOfCategories.homEquiv · CategoryTheory.PresheafOfCategories.comp_fiber · CategoryTheory.PresheafOfCategories.isFibered · CategoryTheory.Pseudofunctor.CoGrothendieck · CategoryTheory.Pseudofunctor.CoGrothendieck.forget · CategoryTheory.Pseudofunctor.CoGrothendieck.instIsFiberedForget

Section4.37 Presheaves of groupoids#

Section 4.37 of the Stacks Project, Tag 0048. 3 tags here are carried by 3 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0049, an example

Tag 0049 in the Stacks Project.

CategoryTheory.isFiberedInGroupoids_presheafOfGroupoids, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedInGroupoids/OfPresheaf.lean, line 100. References: SGA 4 VI (6.1.3), “strict, groupoid fibers”; SGA 7 VI (1.1(a)), “groupoid-valued F”.

Stacks 0049. The category 𝒮_F attached to a presheaf of groupoids F : 𝒞ᵒᵖ ⥤ Grpd is fibred in groupoids over 𝒞: every morphism of 𝒞 lifts, and every fill-in problem has a unique solution.

theorem isFiberedInGroupoids_presheafOfGroupoids :
    (presheafOfGroupoids F).p.IsFiberedInGroupoids
Tag 04TL, a definition

Tag 04TL in the Stacks Project.

CategoryTheory.Functor.IsSplitFiberedInGroupoids, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedInGroupoids/Split.lean, line 89.

Stacks 04TL. A split category fibred in groupoids over 𝒞 is a category fibred in groupoids p : 𝒮 ⥤ 𝒞 that is isomorphic over 𝒞 to the category 𝒮_F attached to some presheaf of groupoids F : 𝒞ᵒᵖ ⥤ Grpd (Stacks 0049). The source is explicit that isomorphism over 𝒞, and not merely equivalence over 𝒞, is meant.

def Functor.IsSplitFiberedInGroupoids (p : 𝒮 ⥤ 𝒞) : Prop
Tag 02XY, a lemma

Tag 02XY in the Stacks Project.

CategoryTheory.Functor.exists_isFibredEquivalenceOver_presheafOfGroupoids, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedCategory/Strictification.lean, line 955.

Stacks 02XY. Every category fibred in groupoids p : 𝒳 ⥤ 𝒞 is equivalent, in the 2-category of fibred categories over 𝒞, to the category 𝒮_F (Stacks 0049, CategoryTheory.presheafOfGroupoids) attached to a contravariant functor F : 𝒞 ⥤ Groupoids; in other words, every category fibred in groupoids is equivalent to a split one.

theorem exists_isFibredEquivalenceOver_presheafOfGroupoids (p : 𝒳 ⥤ 𝒞)
    (hp : p.IsFiberedInGroupoids) :
    ∃ (F : 𝒞ᵒᵖ ⥤ Grpd.{v₂, max u₁ u₂ v₁}) (Φ : 𝒳 ⥤ (presheafOfGroupoids F).obj),
      IsFibredEquivalenceOver p (presheafOfGroupoids F).p Φ
Sources
LeanCategoryTheory.isFiberedInGroupoids_presheafOfGroupoids · CategoryTheory.Functor.IsSplitFiberedInGroupoids · CategoryTheory.Functor.exists_isFibredEquivalenceOver_presheafOfGroupoids

Section4.38 Categories fibred in sets#

Section 4.38 of the Stacks Project, Tag 0042. 6 tags here are carried by 8 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 02Y0, a definition

Tag 02Y0 in the Stacks Project.

Declarations registered for the tag:

Tag 04S8, a definition

Tag 04S8 in the Stacks Project.

CategoryTheory.CatFiberedInSets, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedInSets/TwoCategory.lean, line 149.

The 2-category of categories fibred in sets over 𝒞: the full sub-2-category of the 2-category BasedCategory 𝒞 of categories over 𝒞 spanned by the categories fibred in sets. Explicitly:

  1. its objects are the categories p : 𝒮 ⥤ 𝒞 over 𝒞 that are fibred in sets;
  2. its 1-morphisms (𝒮, p) ⟶ (𝒮', p') are the functors G : 𝒮 ⥤ 𝒮' with p' ∘ G = p;
  3. its 2-morphisms t : G ⟶ H are the morphisms of functors with p'(t_x) = 𝟙 (p x) for every object x of 𝒮.
abbrev CatFiberedInSets (𝒞 : Type u₁) [Category.{v₁} 𝒞]
Tag 0047, a lemma

Tag 0047 in the Stacks Project.

CategoryTheory.Functor.IsFiberedInSets.twoFibreProd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedInSets/TwoFibreProduct.lean, line 147.

Stacks 0047 (Lemma 4.38.4). The 2-category of categories fibred in sets over 𝒞 has 2-fibre products: if 𝒳, 𝒴, 𝒮 are fibred in sets over 𝒞 and F : 𝒳 ⥤ 𝒮, G : 𝒴 ⥤ 𝒮 are 1-morphisms over 𝒞, then the 2-fibre product 𝒳 ×_𝒮 𝒴 of Stacks 0040, with its structure functor, is again fibred in sets over 𝒞.

theorem Functor.IsFiberedInSets.twoFibreProd
    [pX.IsFiberedInSets] [pY.IsFiberedInSets] [pS.IsFiberedInSets]
    (hF : F ⋙ pS = pX) (hG : G ⋙ pS = pY) :
    (TwoFibreProd.proj pX pY pS F G).IsFiberedInSets
Tag 04TM, an example

Tag 04TM in the Stacks Project.

elementsCategory, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedInSets/OfPresheaf.lean, line 53. References: SGA 7 VI (1.1(a)), “set-valued F”.

Stacks 04TM. The category 𝒮_F attached to a presheaf F : Cᵒᵖ ⥤ Type*: objects are the pairs (U, x) with x ∈ F(U), and a morphism (V, y) ⟶ (U, x) is an f : V ⟶ U of C with f^* x = y. This is Mathlib's category of elements of F.

def elementsCategory {C : Type*} [Category C] (F : Cᵒᵖ ⥤ Type*) :
    Category F.Elements
Tag 02Y2, a lemma

Tag 02Y2 in the Stacks Project.

CategoryTheory.Functor.twoMorphisms_are_identity, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedInSets/TwoCategoryIsCategory.lean, line 137.

A 2-morphism over 𝒞 between two 1-morphisms into a category fibred in sets is an identity: the two 1-morphisms are equal.

theorem twoMorphisms_are_identity
    {𝒮 : Type u₂} [Category.{v₂} 𝒮] {𝒮' : Type u₃} [Category.{v₃} 𝒮']
    (p : 𝒮 ⥤ 𝒞) (p' : 𝒮' ⥤ 𝒞) [p'.IsFiberedInSets]
    (F G : 𝒮 ⥤ 𝒮') (hF : F ⋙ p' = p) (hG : G ⋙ p' = p)
    (η : F ⟶ G)
    (hη : ∀ x, HEq (p'.map (η.app x)) (𝟙 (p.obj x))) :
    F = G
Tag 0044, an example

Tag 0044 in the Stacks Project.

CategoryTheory.overEquivElementsOp, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Elements.lean, line 95.

C/X is the category of elements of h_X. The slice category C/X is equivalent to the category S_{h_X} = ((h_X).Elements)ᵒᵖ attached to the representable presheaf h_X = Mor_C(-, X).

Both round trips are the identity functor on the nose, so the unit and counit are identities.

def overEquivElementsOp : Over X ≌ ((yoneda.obj X).Elements)ᵒᵖ

CategoryTheory.overEquivElementsOpForget, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Elements.lean, line 113.

The equivalence of overEquivElementsOp is an equivalence over C. It carries the structure functor C/X → C to the structure functor S_{h_X} → C, which is (Functor.Elements.π h_X).leftOp. This is the sense in which C/X is canonically equivalent over C to S_{h_X}.

def overEquivElementsOpForget :
    (overEquivElementsOp X).functor ⋙ (Functor.Elements.π (yoneda.obj X)).leftOp
      ≅ Over.forget X

CategoryTheory.Over.eq_of_hom_left_id, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Elements.lean, line 268.

The fibre categories of C/X → C have only identities (existence part). If there is a morphism Over.mk f ⟶ Over.mk g of C/X lying over the identity of U, then f = g.

theorem eq_of_hom_left_id {U : C} {f g : U ⟶ X} (φ : Over.mk f ⟶ Over.mk g)
    (hφ : φ.left = 𝟙 U) : f = g

CategoryTheory.Over.hom_eq_id_of_left_id, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Elements.lean, line 277.

The fibre categories of C/X → C have only identities (uniqueness part). A morphism of C/X from an object to itself lying over the identity is the identity. Together with CategoryTheory.Over.eq_of_hom_left_id this says that the fibre category of C/X → C over U has the morphisms h : U ⟶ X as objects and only identities as morphisms.

theorem hom_eq_id_of_left_id {U : C} {f : U ⟶ X} (φ : Over.mk f ⟶ Over.mk f)
    (hφ : φ.left = 𝟙 U) : φ = 𝟙 (Over.mk f)
Sources
LeanCategoryTheory.IsDiscrete · CategoryTheory.CatFiberedInSets · CategoryTheory.Functor.IsFiberedInSets.twoFibreProd · elementsCategory · CategoryTheory.Functor.twoMorphisms_are_identity · CategoryTheory.overEquivElementsOp · CategoryTheory.overEquivElementsOpForget · CategoryTheory.Over.eq_of_hom_left_id

Section4.39 Categories fibred in setoids#

Section 4.39 of the Stacks Project, Tag 04S9. 8 tags here are carried by 15 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 02XZ, a definition

Tag 02XZ in the Stacks Project.

IsSetoidCategory, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedInSetoids/Setoid.lean, line 54. References: SGA 4 I (6.5.1), “discrete category def”.

Stacks 02XZ. A category C is a setoid when every morphism of C is an isomorphism and every endomorphism f : X ⟶ X is 𝟙 X; equivalently C is a thin groupoid, so a setoid is a set together with an equivalence relation on it.

def IsSetoidCategory (C : Type*) [Category C] : Prop
Tag 04SA, a definition

Tag 04SA in the Stacks Project.

CategoryTheory.Functor.IsFiberedInSetoids, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedInSetoids/Defs.lean, line 49.

Stacks 04SA. A functor p : 𝒳 ⥤ 𝒮 is a category fibred in setoids if it is fibred in groupoids and each fibre category p.Fiber S is a setoid, i.e. thin (its fibres are groupoids automatically, by Stacks 003V).

class IsFiberedInSetoids (p : 𝒳 ⥤ 𝒮) : Prop
Tag 02Y1, a definition

Tag 02Y1 in the Stacks Project.

CategoryTheory.CatFiberedInSetoids, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedInSetoids/TwoCategory.lean, line 40.

The 2-category of categories fibred in setoids over 𝒞: the full sub-2-category of the 2-category BasedCategory 𝒞 of categories over 𝒞 spanned by the categories fibred in setoids. Explicitly:

  1. its objects are the categories p : 𝒮 ⥤ 𝒞 over 𝒞 that are fibred in setoids;
  2. its 1-morphisms (𝒮, p) ⟶ (𝒮', p') are the functors G : 𝒮 ⥤ 𝒮' with p' ∘ G = p;
  3. its 2-morphisms t : G ⟶ H are the morphisms of functors with p'(t_x) = 𝟙 (p x) for every object x of 𝒮.
abbrev CatFiberedInSetoids (𝒞 : Type u₁) [Category.{v₁} 𝒞]
Tag 04SB, a lemma

Tag 04SB in the Stacks Project.

CategoryTheory.TwoFibreProd.proj_isFiberedInSetoids, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedInSetoids/TwoFibreProduct.lean, line 334.

The 2-fibre product of categories fibred in setoids. If 𝒳, 𝒴, 𝒮 are fibred in setoids over 𝒞 and F : 𝒳 ⥤ 𝒮, G : 𝒴 ⥤ 𝒮 are 1-morphisms over 𝒞, then the 2-fibre product 𝒳 ×_𝒮 𝒴 over 𝒞, with its structure functor, is again fibred in setoids over 𝒞.

theorem TwoFibreProd.proj_isFiberedInSetoids
    (hX : pX.IsFiberedInSetoids) (hY : pY.IsFiberedInSetoids) (hS : pS.IsFiberedInSetoids)
    (hF : F ⋙ pS = pX) (hG : G ⋙ pS = pY) :
    (TwoFibreProd.proj pX pY pS F G).IsFiberedInSetoids
Tag 0045, a lemma

Tag 0045 in the Stacks Project.

CategoryTheory.BasedCategory.Equivalence.isFiberedInSetoids_of_isFiberedInSets, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedInSetoids/EquivalentFiberedInSets.lean, line 115. The attribute's comment: “(1)(a)”. References: SGA 4 I (6.5.1), “more general”.

Stacks 0045 (1)(a). Let 𝒞 be a category and let 𝒳 be a category over 𝒞. If 𝒳 is equivalent over 𝒞 to a category 𝒴 fibred in sets over 𝒞, then 𝒳 is fibred in setoids over 𝒞.

Both fibre conditions are transported backwards along the equivalence: a category fibred in sets is fibred in groupoids with discrete, hence thin, fibres (Stacks 0043), and being fibred in groupoids and having thin fibres each transport.

theorem isFiberedInSetoids_of_isFiberedInSets (e : BasedCategory.Equivalence 𝒳 𝒴)
    (h : 𝒴.p.IsFiberedInSets) : 𝒳.p.IsFiberedInSetoids

CategoryTheory.BasedCategory.Equivalence.fiberMap_identifiesIsoClasses, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedInSetoids/EquivalentFiberedInSets.lean, line 132. The attribute's comment: “(1)(b)”.

Stacks 0045 (1)(b). Let 𝒞 be a category, let 𝒳 be a category over 𝒞 and let e be an equivalence over 𝒞 from 𝒳 to a category 𝒴 fibred in sets over 𝒞. For every object U of 𝒞 the induced map Ob(𝒳_U) → Ob(𝒴_U) on the objects of the fibres identifies its target with the set of isomorphism classes of its source: it is surjective, and two objects of 𝒳_U have the same image exactly when they are isomorphic in 𝒳_U.

The same content packaged as a bijection Ob(𝒳_U)/≅ ≃ Ob(𝒴_U) is CategoryTheory.BasedCategory.Equivalence.fiberQuotientEquiv; as there, the two categories over 𝒞 are taken in one pair of universes.

theorem fiberMap_identifiesIsoClasses {𝒳 𝒴 : BasedCategory.{v₂, u₂} 𝒞}
    (e : BasedCategory.Equivalence 𝒳 𝒴)
    (h : 𝒴.p.IsFiberedInSets) (U : 𝒞) :
    Function.Surjective (e.fiberMap (U := U)) ∧
      ∀ x y : 𝒳.p.Fiber U, e.fiberMap x = e.fiberMap y ↔ IsIsomorphic x y

CategoryTheory.Functor.isFiberedInSets_isoClassElementsProj, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedInSetoids/EquivalentFiberedInSets.lean, line 264. The attribute's comment: “(2), the category fibred in sets”.

Stacks 0045 (2), the category produced is fibred in sets. The lift of f : V ⟶ U at (U, ξ) is (V, f^*ξ), with the restriction map of the presheaf of isomorphism classes as the morphism, and it is the only one: a lift of f with target (U, ξ) has its underlying morphism of 𝒞 forced to be f, and then the class at its source is forced to be f^*ξ.

instance isFiberedInSets_isoClassElementsProj (p : 𝒮 ⥤ 𝒞) [p.IsFibered] :
    (isoClassElementsProj p).IsFiberedInSets

CategoryTheory.Functor.basedEquivalenceIsoClassElements, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedInSetoids/EquivalentFiberedInSets.lean, line 428. The attribute's comment: “(2), the equivalence over the base”.

Stacks 0045 (2), the equivalence. Let 𝒞 be a category and let p : 𝒮 ⥤ 𝒞 be a category fibred in setoids. Then can : 𝒮 ⥤ 𝒮' is an equivalence over 𝒞 onto the category of elements of the presheaf of isomorphism classes, which is fibred in sets by CategoryTheory.Functor.isFiberedInSets_isoClassElementsProj.

noncomputable def basedEquivalenceIsoClassElements (p : 𝒮 ⥤ 𝒞) [p.IsFiberedInSetoids] :
    BasedCategory.Equivalence (BasedCategory.ofFunctor p)
      (BasedCategory.ofFunctor (isoClassElementsProj p))
Tag 04SC, a lemma

Tag 04SC in the Stacks Project.

CategoryTheory.Functor.existsUnique_twoIso_of_isoClassMap_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedCategory/FiberedInSetoids.lean, line 360. The attribute's comment: “(1): a unique 2-isomorphism between two 1-morphisms with the same image under F.”.

Stacks 04SC (1). For two 1-morphisms f, g : 𝒮₁ ⟶ 𝒮₂ of categories fibred in setoids over 𝒞 with F(f) = F(g), that is inducing the same map on the presheaves of isomorphism classes of objects, there is a unique 2-isomorphism f ⟶ g.

theorem existsUnique_twoIso_of_isoClassMap_eq {G H : 𝒮 ⥤ 𝒯} (hG : G ⋙ q = p) (hH : H ⋙ q = p)
    (h : isoClassMapOfCompEq hG = isoClassMapOfCompEq hH) :
    ∃! e : G ≅ H, ∀ x : 𝒮, q.IsHomLift (𝟙 (p.obj x)) (e.hom.app x)

CategoryTheory.Functor.exists_oneMorphism_isoClassMap_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedCategory/FiberedInSetoids.lean, line 476. The attribute's comment: “(2): every map of the associated presheaves comes from a 1-morphism.”.

Stacks 04SC (2). Every morphism h : F(𝒮₁) ⟶ F(𝒮₂) of presheaves of isomorphism classes is F(f) for a 1-morphism f : 𝒮₁ ⟶ 𝒮₂ of categories fibred in setoids over 𝒞.

theorem exists_oneMorphism_isoClassMap_eq :
    ∃ (G : 𝒮 ⥤ 𝒯) (hG : G ⋙ q = p), isoClassMapOfCompEq hG = φ

CategoryTheory.Functor.isoClassMapEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedCategory/FiberedInSetoids.lean, line 526. The attribute's comment: “The bijection Mor(𝒮₁, 𝒮₂)/2-isomorphism = Mor_{PSh}(F₁, F₂).”.

Stacks 04SC, final form: for categories 𝒮₁, 𝒮₂ fibred in setoids over 𝒞, Mor_{Cat/𝒞}(𝒮₁, 𝒮₂) modulo 2-isomorphism is Mor_{PSh(𝒞)}(F₁, F₂), where F_i(U) is the set of isomorphism classes of objects of the fibre of 𝒮_i over U. The forward map sends a 1-morphism to the induced map of presheaves; it is surjective by Stacks 04SC (2) and injective by Stacks 04SC (1).

noncomputable def isoClassMapEquiv :
    _root_.Quotient (twoIsoSetoid p q) ≃ (p.isoClassPresheaf ⟶ q.isoClassPresheaf)

CategoryTheory.Functor.fiberPresheafIsoIsoClassPresheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedCategory/FiberedInSetoids.lean, line 584. The attribute's comment: “(3): for a category fibred in sets the presheaf of isomorphism classes of the fibres is the presheaf of objects of the fibres, i.e. 𝒮 = F(𝒮).”.

Stacks 04SC (3). A category fibred in sets 𝒮 is equal to F(𝒮): the presheaf of isomorphism classes of the fibres of 𝒮 is the presheaf U ↦ Ob(𝒮_U) of objects of the fibres, which is the presheaf that Stacks 02Y2 attaches to 𝒮. The isomorphism is the quotient map at each U, a bijection because the fibres are discrete, and it is natural because on both sides the restriction along f : V ⟶ U is x ↦ f^* x.

noncomputable def fiberPresheafIsoIsoClassPresheaf (hd : ∀ U : 𝒞, IsDiscrete (p.Fiber U)) :
    p.fiberPresheaf hd ≅ p.isoClassPresheaf
Tag 042J, a lemma

Tag 042J in the Stacks Project.

isFiberedInSetoids_iff_π_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedInSetoids/Inertia.lean, line 31.

Stacks 042J. A category fibred in groupoids p : 𝒮 ⥤ 𝒞 is fibred in setoids if and only if the forgetful 1-morphism π : I_𝒮 ⥤ 𝒮 of the absolute inertia is an equivalence. Since π is always faithful and essentially surjective, the content is that π is full exactly when the fibres of p are thin.

theorem isFiberedInSetoids_iff_π_isEquivalence (p : 𝒮 ⥤ 𝒞) (hp : p.IsFiberedInGroupoids) :
    p.IsFiberedInSetoids ↔ (RelativeInertia.π p : AbsoluteInertia p ⥤ 𝒮).IsEquivalence
Tag 04SD, a lemma

Tag 04SD in the Stacks Project.

CategoryTheory.Functor.twoFibreProductIsoClassEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedCategory/FiberedInSetoids.lean, line 837.

Stacks 04SD. The presheaf attached by Stacks 04SC to a 2-fibre product 𝒳 ×_𝒵 𝒴 over 𝒞 is the fibre product of the presheaves attached to 𝒳, 𝒴 and 𝒵: at every object U of 𝒞, Ob((𝒳 ×_𝒵 𝒴)_U)/≅ = Ob(𝒳_U)/≅ ×_{Ob(𝒵_U)/≅} Ob(𝒴_U)/≅, by the bijection sending the class of an object to the pair of the classes of its components. This is the display to which the source's proof reduces the lemma.

noncomputable def twoFibreProductIsoClassEquiv (U : 𝒞) :
    _root_.Quotient
        (isIsomorphicSetoid
          ((TwoFibreProductOver.structureFunctor p𝒳 p𝒴 p𝒵 F G).Fiber U)) ≃
      {ab : _root_.Quotient (isIsomorphicSetoid (p𝒳.Fiber U)) ×
            _root_.Quotient (isIsomorphicSetoid (p𝒴.Fiber U)) //
          (isoClassMap hF).app (op U) ab.1 = (isoClassMap hG).app (op U) ab.2}

CategoryTheory.Functor.twoFibreProductIsoClassMap_naturality, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedCategory/FiberedInSetoids.lean, line 852. The attribute's comment: “Naturality: the bijection is an isomorphism of presheaves.”.

Stacks 04SD, naturality: the bijection of CategoryTheory.Functor.twoFibreProductIsoClassEquiv commutes with restriction along a morphism of 𝒞, so it is an isomorphism of presheaves and not merely a family of bijections.

lemma twoFibreProductIsoClassMap_naturality
    [(TwoFibreProductOver.structureFunctor p𝒳 p𝒴 p𝒵 F G).IsFibered] {V U : 𝒞} (f : V ⟶ U)
    (c : (TwoFibreProductOver.structureFunctor p𝒳 p𝒴 p𝒵 F G).isoClassPresheaf.obj (op U)) :
    (twoFibreProductIsoClassMap hF hG V
        ((TwoFibreProductOver.structureFunctor p𝒳 p𝒴 p𝒵 F G).isoClassPresheaf.map f.op c)).val =
      (p𝒳.isoClassPresheaf.map f.op (twoFibreProductIsoClassMap hF hG U c).val.fst,
        p𝒴.isoClassPresheaf.map f.op (twoFibreProductIsoClassMap hF hG U c).val.snd)
Sources
LeanIsSetoidCategory · CategoryTheory.Functor.IsFiberedInSetoids · CategoryTheory.CatFiberedInSetoids · CategoryTheory.TwoFibreProd.proj_isFiberedInSetoids · CategoryTheory.BasedCategory.Equivalence.isFiberedInSetoids_of_isFiberedInSets · CategoryTheory.BasedCategory.Equivalence.fiberMap_identifiesIsoClasses · CategoryTheory.Functor.isFiberedInSets_isoClassElementsProj · CategoryTheory.Functor.basedEquivalenceIsoClassElements

Section4.40 Representable categories fibred in groupoids#

Section 4.40 of the Stacks Project, Tag 04SE. 3 tags here are carried by 5 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0046, a definition

Tag 0046 in the Stacks Project.

IsRepresentable, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedInGroupoids/Representability/Defs.lean, line 51.

A category fibred in groupoids p : 𝒮 ⥤ 𝒞 is representable if there exists an object X of 𝒞 and an equivalence j : 𝒮 ≌ Over X over 𝒞.

structure IsRepresentable {𝒞 : Type*} [Category 𝒞] {𝒮 : Type*} [Category 𝒮]
    (p : 𝒮 ⥤ 𝒞) [IsFibered p] : Prop
Tag 02Y3, a lemma

Tag 02Y3 in the Stacks Project.

StacksRepresentableCFG.representable_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedInGroupoids/Representability/Criterion.lean, line 829. The attribute's comment: “(1)”. References: SGA 4 I (6.5), “(ii)⇔(iv), special case”.

Stacks 02Y3 (part 1). A category fibred in groupoids p : S ⥤ C is representable if and only if S is fibred in setoids and its presheaf of isomorphism classes \overline{S} is representable.

theorem representable_iff (p : 𝒮 ⥤ 𝒞) :
    IsRepresentable p ↔ (p.IsFiberedInSetoids ∧ IsoClassRepresentable p)

StacksRepresentableCFG.representing_object_unique, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedInGroupoids/Representability/Criterion.lean, line 841. The attribute's comment: “(2)”.

Stacks 02Y3 (part 2). If p : S ⥤ C is representable by both X (via j) and X' (via j'), then the representing objects are canonically isomorphic in C: this is the isomorphism X' ≅ X induced by the composite equivalence over C, obtained by transporting the terminal object (X', 𝟙 X') of Over X' to the terminal object (X, 𝟙 X) of Over X.

noncomputable def representing_object_unique (p : 𝒮 ⥤ 𝒞)
    {X X' : 𝒞} (j : RepresentableBy p X) (j' : RepresentableBy p X') :
    X' ≅ X
Tag 04SF, a lemma

Tag 04SF in the Stacks Project.

CategoryTheory.Functor.exists_oneMorphism_inducing_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedCategory/RepresentableFibred.lean, line 195. The attribute's comment: “Given φ : X ⟶ Y there is a 1-morphism inducing it, unique up to unique 2-isomorphism.”.

Stacks 04SF, the precise form: given φ : X ⟶ Y there is a 1-morphism G : 𝒳 ⥤ 𝒴 over 𝒞 which induces φ on isomorphism classes of objects, and any 1-morphism inducing φ is related to it by a unique 2-isomorphism. Inducing φ is spelled out through the bijections \overline{𝒳}(U) ≃ (U ⟶ X) and \overline{𝒴}(U) ≃ (U ⟶ Y) that representability supplies.

theorem exists_oneMorphism_inducing_hom (φ : X ⟶ Y) :
    ∃ (G : 𝒳 ⥤ 𝒴) (hG : G ⋙ q = p),
      (∀ (U : 𝒞) (c : p.isoClassPresheaf.obj (op U)),
        hY.equiv U ((isoClassMapOfCompEq hG).app (op U) c) = hX.equiv U c ≫ φ) ∧
      ∀ (H : 𝒳 ⥤ 𝒴) (hH : H ⋙ q = p),
        (∀ (U : 𝒞) (c : p.isoClassPresheaf.obj (op U)),
          hY.equiv U ((isoClassMapOfCompEq hH).app (op U) c) = hX.equiv U c ≫ φ) →
        ∃! e : G ≅ H, ∀ x : 𝒳, q.IsHomLift (𝟙 (p.obj x)) (e.hom.app x)

CategoryTheory.Functor.twoIsoQuotientEquivHomOfRepresentableBy, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedCategory/RepresentableFibred.lean, line 225.

Stacks 04SF. Let 𝒳, 𝒴 be categories fibred in groupoids over 𝒞 representable by objects X, Y of 𝒞. Then Mor_{Cat/𝒞}(𝒳, 𝒴) modulo 2-isomorphism is Mor_𝒞(X, Y). The bijection is the composite of Stacks 04SC, which identifies the left-hand side with the maps \overline{𝒳} ⟶ \overline{𝒴} of presheaves of isomorphism classes, with the Yoneda step CategoryTheory.Functor.isoClassPresheafHomEquiv.

noncomputable def twoIsoQuotientEquivHomOfRepresentableBy :
    _root_.Quotient (twoIsoSetoid p q) ≃ (X ⟶ Y)
Sources
LeanIsRepresentable · StacksRepresentableCFG.representable_iff · StacksRepresentableCFG.representing_object_unique · CategoryTheory.Functor.exists_oneMorphism_inducing_hom · CategoryTheory.Functor.twoIsoQuotientEquivHomOfRepresentableBy

Section4.41 The 2-Yoneda lemma#

Section 4.41 of the Stacks Project, Tag 0GWH. 3 tags here are carried by 11 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0GWI, a lemma

Tag 0GWI in the Stacks Project.

CategoryTheory.Functor.FiberedMor, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoYoneda/Fibered.lean, line 67.

A morphism of fibred categories (𝒞/U, Over.forget U) ⟶ (𝒮, p), i.e. an object of the category Mor_{Fib/𝒞}(𝒞/U, 𝒮) of Stacks Definition 02XP(2) with source the slice fibration. It is a functor over 𝒞 — a BasedFunctor between the based categories attached to Over.forget U and to p, so the underlying functor Over U ⥤ 𝒮 commutes strictly with the projections to 𝒞 — which in addition preserves strongly Cartesian morphisms.

Since the slice projection Over.forget U is a fibration in which every morphism g : a ⟶ b of Over U is strongly Cartesian over its underlying 𝒞-arrow g.left = (Over.forget U).map g, the preservation condition specialises to the unconditional requirement that toFunctor.map g be strongly Cartesian over g.left.

structure FiberedMor (p : 𝒮 ⥤ 𝒞) (U : 𝒞) extends
    BasedCategory.ofFunctor (Over.forget U) ⥤ᵇ BasedCategory.ofFunctor p

CategoryTheory.Functor.fibYonedaEvaluation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoYoneda/Fibered.lean, line 139.

The evaluation, or "2-Yoneda", functor ev_U : Mor_{Fib/𝒞}(𝒞/U, 𝒮) ⥤ 𝒮_U, G ↦ G 1_U.

On objects it sends a morphism of fibred categories G to its value at the terminal object 1_U = (U, 𝟙 U) of 𝒞/U, which lies in the fibre over U because G ⋙ p = Over.forget U. On a 2-morphism t it returns the component of t at 1_U, which lies over 𝟙 U and is therefore a morphism of the fibre.

def fibYonedaEvaluation (p : 𝒮 ⥤ 𝒞) (U : 𝒞) : FiberedMor p U ⥤ p.Fiber U

CategoryTheory.Functor.fibYonedaEvaluation_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoYoneda/Fibered.lean, line 409.

The 2-Yoneda lemma for fibred categories (Stacks 0GWI). For a fibred category p : 𝒮 ⥤ 𝒞 and an object U : 𝒞, the evaluation functor ev_U : Mor_{Fib/𝒞}(𝒞/U, 𝒮) ⥤ 𝒮_U, G ↦ G 1_U, is an equivalence of categories.

theorem fibYonedaEvaluation_isEquivalence (p : 𝒮 ⥤ 𝒞) [p.IsFibered] (U : 𝒞) :
    (fibYonedaEvaluation p U).IsEquivalence
Tag 004B, a lemma

Tag 004B in the Stacks Project.

CategoryTheory.Functor.twoYonedaEvaluation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoYoneda/Basic.lean, line 124.

The evaluation functor ev : Mor_{Cat/C}(C/U, S) ⥤ S_U of the 2-Yoneda lemma.

On objects it sends a functor over C, G : C/U ⥤ S (packaged as a based functor), to G(id_U) = G(Over.mk (𝟙 U)), which lies in the fibre over U since p ∘ G = π_U and π_U (Over.mk (𝟙 U)) = U.

On a 2-morphism η : G ⟶ G' (a based natural transformation) it returns the component η_{(U, 𝟙 U)}, which lies over 𝟙 U and is therefore a morphism of S_U.

noncomputable def Functor.twoYonedaEvaluation (p : S ⥤ C) (U : C) :
    (BasedCategory.ofFunctor (Over.forget U) ⥤ᵇ BasedCategory.ofFunctor p) ⥤ p.Fiber U

CategoryTheory.Functor.twoYonedaEvaluation_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoYoneda/Basic.lean, line 368.

The 2-Yoneda lemma (Stacks 004B). Let p : S ⥤ C be fibred in groupoids and let U be an object of C. Then the evaluation functor ev : Mor_{Cat/C}(C/U, S) ⥤ S_U, G ↦ G(id_U), is an equivalence of categories.

It is faithful, full and essentially surjective by Functor.twoYonedaEvaluation_faithful, Functor.twoYonedaEvaluation_full and Functor.twoYonedaEvaluation_essSurj, and a functor with these three properties is an equivalence.

theorem Functor.twoYonedaEvaluation_isEquivalence (p : S ⥤ C) (hp : p.IsFiberedInGroupoids)
    (U : C) : (Functor.twoYonedaEvaluation p U).IsEquivalence

CategoryTheory.Functor.TwoYoneda.liftBasedEvaluationIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoYoneda/RepresentedPoint.lean, line 65. The attribute's comment: “essential surjectivity of evaluation, as data”.

Stacks 004B, essential surjectivity as data. The functor over C on the slice C/U assembled from the chosen cartesian lifts of an object x of the fibre of p over U evaluates at the terminal object to an object canonically isomorphic to x: the chosen lift at 𝟙 U is an arrow of the fibre, and the fibre of a category fibred in groupoids is a groupoid.

noncomputable def liftBasedEvaluationIso (p : S ⥤ C) (hp : p.IsFiberedInGroupoids) (U : C)
    (x : p.Fiber U) :
    (Functor.twoYonedaEvaluation p U).obj (liftBased p hp U x) ≅ x

CategoryTheory.Functor.TwoYoneda.hom₂OfFiberHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoYoneda/RepresentedPoint.lean, line 80. The attribute's comment: “fullness of evaluation, as data”.

Stacks 004B, fullness as data. The 2-morphism of functors over C on the slice C/U representing a morphism of the fibre objects they evaluate to.

noncomputable def hom₂OfFiberHom
    (φ : (Functor.twoYonedaEvaluation p U).obj G ⟶ (Functor.twoYonedaEvaluation p U).obj G') :
    G ⟶ G'
Tag 076J, a remark

Tag 076J in the Stacks Project.

CategoryTheory.Functor.twoYonedaPresheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoYoneda/SplitModel.lean, line 154.

The contravariant functor F : 𝒞 ⥤ Groupoids with F(U) = Mor_{Cat/𝒞}(𝒞/U, 𝒮) and F(f) : F(V) ⥤ F(U) given by precomposition with the functor 𝒞/U ⥤ 𝒞/V induced by f : U ⟶ V.

noncomputable def Functor.twoYonedaPresheaf (p : 𝒮 ⥤ 𝒞) (hp : p.IsFiberedInGroupoids) :
    𝒞ᵒᵖ ⥤ Grpd.{max u₁ v₁ v₂, max u₁ v₁ u₂ v₂}

CategoryTheory.Functor.twoYonedaComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoYoneda/SplitModel.lean, line 237.

The functor G : 𝒮' ⥤ 𝒮 sending the pair (U, x) to x(id_U).

noncomputable def twoYonedaComparison (hp : p.IsFiberedInGroupoids) :
    ∫ᶜ (p.twoYonedaPresheaf hp ⋙ Grpd.forgetToCat).toPseudofunctor' ⥤
      (BasedCategory.ofFunctor p).obj

CategoryTheory.Functor.twoYonedaComparison_comp, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoYoneda/SplitModel.lean, line 287.

The functor G is a functor over 𝒞: its composite with p is the projection of the category 𝒮' attached to F.

lemma twoYonedaComparison_comp (hp : p.IsFiberedInGroupoids) :
    p.twoYonedaComparison hp ⋙ p = (presheafOfGroupoids (p.twoYonedaPresheaf hp)).p

CategoryTheory.Functor.twoYonedaComparison_isEquivalenceOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoYoneda/SplitModel.lean, line 337.

The functor G is an equivalence in the 2-category of categories fibred in groupoids over 𝒞: it admits a quasi-inverse which is again a functor over 𝒞, and the unit and counit have all their components lying over identity morphisms of 𝒞.

theorem twoYonedaComparison_isEquivalenceOver (hp : p.IsFiberedInGroupoids) :
    ∃ (H : 𝒮 ⥤ (presheafOfGroupoids (p.twoYonedaPresheaf hp)).obj)
      (_ : H ⋙ (presheafOfGroupoids (p.twoYonedaPresheaf hp)).p = p)
      (η : p.twoYonedaComparison hp ⋙ H ≅ 𝟭 _)
      (ε : H ⋙ p.twoYonedaComparison hp ≅ 𝟭 _),
      (∀ a, (presheafOfGroupoids (p.twoYonedaPresheaf hp)).p.IsHomLift
          (𝟙 ((presheafOfGroupoids (p.twoYonedaPresheaf hp)).p.obj a)) (η.hom.app a)) ∧
      (∀ z, p.IsHomLift (𝟙 (p.obj z)) (ε.hom.app z))
Sources
LeanCategoryTheory.Functor.FiberedMor · CategoryTheory.Functor.fibYonedaEvaluation · CategoryTheory.Functor.fibYonedaEvaluation_isEquivalence · CategoryTheory.Functor.twoYonedaEvaluation · CategoryTheory.Functor.twoYonedaEvaluation_isEquivalence · CategoryTheory.Functor.TwoYoneda.liftBasedEvaluationIso · CategoryTheory.Functor.TwoYoneda.hom₂OfFiberHom · CategoryTheory.Functor.twoYonedaPresheaf

Section4.42 Representable 1-morphisms#

Section 4.42 of the Stacks Project, Tag 02Y4. 6 tags here are carried by 7 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 02Y5, a lemma

Tag 02Y5 in the Stacks Project.

CategoryTheory.TwoFibreProductOver.FstFiber.objEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedInGroupoids/Representability/Fibres.lean, line 117. The attribute's comment: “(1)”.

Stacks 02Y5 (1). The objects of the fibre category of (𝒞/U) ×_𝒴 𝒳 over an object f : V ⟶ U of 𝒞/U are the pairs (x, φ) consisting of an object x of the fibre 𝒳_V and a morphism φ : G(f) ⟶ F(x) of the fibre 𝒴_V.

noncomputable def objEquiv (h𝒴 : p𝒴.IsFiberedInGroupoids) :
    (fst (Over.forget U) p𝒳 p𝒴 G F).Fiber f ≃
      Σ x : p𝒳.Fiber f.left, {φ : G.obj f ⟶ F.obj x.1 // p𝒴.IsHomLift (𝟙 f.left) φ}

CategoryTheory.TwoFibreProductOver.FstFiber.homEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedInGroupoids/Representability/Fibres.lean, line 188. The attribute's comment: “(2)”.

Stacks 02Y5 (2). The morphisms of the fibre category of (𝒞/U) ×_𝒴 𝒳 over an object f : V ⟶ U of 𝒞/U between two objects (x, φ) and (x', φ') are exactly the morphisms ψ : x ⟶ x' of the fibre 𝒳_V with F(ψ) = φ' ∘ φ⁻¹.

def homEquiv (A B : (fst (Over.forget U) p𝒳 p𝒴 G F).Fiber f) :
    (A ⟶ B) ≃ {ψ : A.1.y ⟶ B.1.y // p𝒳.IsHomLift (𝟙 f.left) ψ ∧
      F.map ψ = (phiIso A).inv ≫ (phiIso B).hom}
Tag 02Y6, a lemma

Tag 02Y6 in the Stacks Project.

CategoryTheory.TwoFibreProductOver.fst_isFiberedInGroupoids, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedInGroupoids/Representability/SliceProduct.lean, line 77.

Stacks 02Y6. Let 𝒳, 𝒴 be categories fibred in groupoids over 𝒞, let F : 𝒳 ⥤ 𝒴 and G : 𝒞/U ⥤ 𝒴 be 1-morphisms over 𝒞. Then the first projection of the 2-fibre product (𝒞/U) ×_𝒴 𝒳 ⟶ 𝒞/U is a category fibred in groupoids over the slice 𝒞/U.

theorem TwoFibreProductOver.fst_isFiberedInGroupoids (U : 𝒞) (p𝒳 : 𝒳 ⥤ 𝒞) (p𝒴 : 𝒴 ⥤ 𝒞)
    (F : 𝒳 ⥤ 𝒴) (G : Over U ⥤ 𝒴)
    (h𝒳 : p𝒳.IsFiberedInGroupoids) (h𝒴 : p𝒴.IsFiberedInGroupoids)
    (hF : F ⋙ p𝒴 = p𝒳) (hG : G ⋙ p𝒴 = Over.forget U) :
    (TwoFibreProductOver.fst (Over.forget U) p𝒳 p𝒴 G F).IsFiberedInGroupoids
Tag 02Y7, a definition

Tag 02Y7 in the Stacks Project.

Stacks.RepresentableMorphism.IsRepresentableMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedInGroupoids/Representability/FibreFunctors.lean, line 142.

Stacks 02Y7. F : 𝒳 ⥤ 𝒴 (a 1-morphism over 𝒞) is representable, equivalently 𝒳 is relatively representable over 𝒴, when for every object U of 𝒞 and every 1-morphism G : 𝒞/U ⥤ 𝒴 over 𝒞 (i.e. G ⋙ q = Over.forget U), the first projection (𝒞/U) ×_𝒴 𝒳 ⥤ 𝒞/U of the 2-fibre product over 𝒞 is a representable category fibred in groupoids.

The source states this for 𝒳, 𝒴 fibred in groupoids over 𝒞; the predicate here does not assume that, so it is the same condition stated for an arbitrary 1-morphism and specialises to the source's notion.

def IsRepresentableMorphism (p : 𝒳 ⥤ 𝒞) (q : 𝒴 ⥤ 𝒞) (F : 𝒳 ⥤ 𝒴) : Prop
Tag 02Y8, a lemma

Tag 02Y8 in the Stacks Project.

Stacks.RepresentableMorphism.inducedFiberFunctor_faithful_of_isRepresentableMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedInGroupoids/Representability/FibreFunctors.lean, line 770.

Stacks 02Y8 (Lemma 4.42.4), the stated implication. If F : 𝒳 ⥤ 𝒴 is a representable 1-morphism over 𝒞 between categories fibred in groupoids, then for every object U of 𝒞 the induced functor on fibre categories F_U : 𝒳_U ⥤ 𝒴_U is faithful. The converse is not proved here.

theorem inducedFiberFunctor_faithful_of_isRepresentableMorphism
    (p : 𝒳 ⥤ 𝒞) (q : 𝒴 ⥤ 𝒞)
    (hq : q.IsFiberedInGroupoids)
    (F : 𝒳 ⥤ 𝒴) (hF : F ⋙ q = p)
    (hrep : IsRepresentableMorphism p q F) (U : 𝒞) :
    (inducedFiberFunctor p q F hF U).Faithful
Tag 02Y9, a lemma

Tag 02Y9 in the Stacks Project.

CategoryTheory.isRepresentableMorphism_of_faithful_of_isRepresentable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedInGroupoids/Representability/MorphismCriterion.lean, line 46.

Let 𝒳, 𝒴 be categories fibred in groupoids over 𝒞, let F : 𝒳 ⥤ 𝒴 be a 1-morphism over 𝒞 and let c be a choice of pullbacks for 𝒴. If every functor F_U : 𝒳_U ⥤ 𝒴_U on fibre categories is faithful, and if for every U and every object y of 𝒴_U the presheaf on 𝒞/U of isomorphism classes of pairs (x, φ : f^* y ⟶ F(x)) is representable, then F is a representable 1-morphism in the sense of Stacks 02Y7.

theorem isRepresentableMorphism_of_faithful_of_isRepresentable (p𝒳 : 𝒳 ⥤ 𝒞) (p𝒴 : 𝒴 ⥤ 𝒞)
    (F : 𝒳 ⥤ 𝒴) (hF : F ⋙ p𝒴 = p𝒳) (h𝒳 : p𝒳.IsFiberedInGroupoids)
    (h𝒴 : p𝒴.IsFiberedInGroupoids) (c : p𝒴.ChoiceOfPullbacks)
    (hfaithful : ∀ U : 𝒞, (Stacks.RepresentableMorphism.inducedFiberFunctor p𝒳 p𝒴 F hF U).Faithful)
    (hrepresentable : ∀ (U : 𝒞) (y : p𝒴.Fiber U),
      (PairIsoClass.presheaf F c y h𝒳 h𝒴 hF).IsRepresentable) :
    Stacks.RepresentableMorphism.IsRepresentableMorphism p𝒳 p𝒴 F
Tag 02YA, a lemma

Tag 02YA in the Stacks Project.

CategoryTheory.Functor.relativelyRepresentable.diagonal_representable_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedInGroupoids/Representability/Diagonal.lean, line 62.

Stacks 02YA. The diagonal is representable iff every morphism out of a representable object is representable. Here F : C ⥤ D is full and preserves binary products and pullbacks (the classifying functor of a category fibred in groupoids), 𝒞 has products of pairs and fibre products, and X : D.

theorem diagonal_representable_iff
    {C : Type*} [Category C] {D : Type*} [Category D] (F : C ⥤ D) (X : D)
    [HasPullbacks C] [HasBinaryProducts C]
    [HasBinaryProducts D] [HasPullbacks D] [HasTerminal D]
    [F.Full] [PreservesLimitsOfShape (Discrete WalkingPair) F]
    [PreservesLimitsOfShape WalkingCospan F] :
    F.relativelyRepresentable (Limits.diag X) ↔
      ∀ ⦃a : C⦄ (g : F.obj a ⟶ X), F.relativelyRepresentable g
Sources
LeanCategoryTheory.TwoFibreProductOver.FstFiber.objEquiv · CategoryTheory.TwoFibreProductOver.FstFiber.homEquiv · CategoryTheory.TwoFibreProductOver.fst_isFiberedInGroupoids · Stacks.RepresentableMorphism.IsRepresentableMorphism · Stacks.RepresentableMorphism.inducedFiberFunctor_faithful_of_isRepresentableMorphism · CategoryTheory.isRepresentableMorphism_of_faithful_of_isRepresentable · CategoryTheory.Functor.relativelyRepresentable.diagonal_representable_iff

Section4.43 Monoidal categories#

Section 4.43 of the Stacks Project, Tag 0FFJ. 10 tags here are carried by 16 declarations of the repository (all in StacksFrontier) and 8 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0FFL, a definition

Tag 0FFL in the Stacks Project.

Declarations registered for the tag:

Tag 0FFM, a lemma

Tag 0FFM in the Stacks Project.

CategoryTheory.MonoidalCategory.invertible_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Monoidal/InvertibleObject.lean, line 116.

For an object X of a monoidal category, the following are equivalent: 1. tensorLeft X is an equivalence; 2. tensorRight X is an equivalence; 3. X is invertible, i.e. it has a two-sided tensor inverse.

theorem invertible_tfae (X : C) :
    [ (tensorLeft X).IsEquivalence,
      (tensorRight X).IsEquivalence,
      IsInvertible X ].TFAE
Tag 0FFN, a definition

Tag 0FFN in the Stacks Project.

CategoryTheory.MonoidalCategory.HasInverse, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Monoidal/InvertibleObject.lean, line 38.

A two-sided tensor inverse for an object X of a monoidal category: an object inv together with isomorphisms X ⊗ inv ≅ 𝟙_ C and inv ⊗ X ≅ 𝟙_ C.

structure HasInverse (X : C)

CategoryTheory.MonoidalCategory.IsInvertible, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Monoidal/InvertibleObject.lean, line 49.

An object X of a monoidal category is invertible if it admits a two-sided tensor inverse, i.e. an object X' with X ⊗ X' ≅ 𝟙_ C and X' ⊗ X ≅ 𝟙_ C.

def IsInvertible (X : C) : Prop
Tag 0FFP, a definition

Tag 0FFP in the Stacks Project.

Declarations registered for the tag:

Tag 0FFQ, a lemma

Tag 0FFQ in the Stacks Project.

CategoryTheory.tensorRightHomEquiv_whiskerRight_comp_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Monoidal/DualHomBijections.lean, line 59. The attribute's comment: “first bijection, natural in Z and Z'”.

Stacks Project, Tag 0FFQ, first bijection. If Y is a left dual of X (in Mathlib, [ExactPairing X Y]), then tensorRightHomEquiv Z' X Y Z : Mor(Z' ⊗ X, Z) ≃ Mor(Z', Z ⊗ Y) is natural in Z and Z': for a : Z₂' ⟶ Z₁' and b : Z₁ ⟶ Z₂ it carries (a ⊗ 1_X) ≫ f ≫ b to a ≫ e(f) ≫ (b ⊗ 1_Y).

theorem tensorRightHomEquiv_whiskerRight_comp_comp (X Y : C) [ExactPairing X Y] {Z₁' Z₂' Z₁ Z₂ : C}
    (a : Z₂' ⟶ Z₁') (f : Z₁' ⊗ X ⟶ Z₁) (b : Z₁ ⟶ Z₂) :
    tensorRightHomEquiv Z₂' X Y Z₂ (a ▷ X ≫ f ≫ b) =
      a ≫ tensorRightHomEquiv Z₁' X Y Z₁ f ≫ b ▷ Y

CategoryTheory.tensorLeftHomEquiv_whiskerLeft_comp_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Monoidal/DualHomBijections.lean, line 71. The attribute's comment: “second bijection, natural in Z and Z'”.

Stacks Project, Tag 0FFQ, second bijection. If Y is a left dual of X (in Mathlib, [ExactPairing X Y]), then tensorLeftHomEquiv Z' X Y Z : Mor(Y ⊗ Z', Z) ≃ Mor(Z', X ⊗ Z) is natural in Z and Z': for a : Z₂' ⟶ Z₁' and b : Z₁ ⟶ Z₂ it carries (1_Y ⊗ a) ≫ f ≫ b to a ≫ e(f) ≫ (1_X ⊗ b).

theorem tensorLeftHomEquiv_whiskerLeft_comp_comp (X Y : C) [ExactPairing X Y] {Z₁' Z₂' Z₁ Z₂ : C}
    (a : Z₂' ⟶ Z₁') (f : Y ⊗ Z₁' ⟶ Z₁) (b : Z₁ ⟶ Z₂) :
    tensorLeftHomEquiv Z₂' X Y Z₂ (Y ◁ a ≫ f ≫ b) =
      a ≫ tensorLeftHomEquiv Z₁' X Y Z₁ f ≫ X ◁ b

Declarations registered for the tag:

Tag 0FFR, a remark

Tag 0FFR in the Stacks Project.

CategoryTheory.Adjunction.IsTensorCompatible, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Monoidal/RigidAdjunction.lean, line 93.

An adjunction adj : tensorRight X ⊣ tensorRight Y, i.e. a bijection Mor(Z' ⊗ X, Z) ≃ Mor(Z', Z ⊗ Y) functorial in Z and Z', is compatible with the tensor structure if for all W, Z, Z' the square

  Mor(Z' ⊗ X, Z)         →  Mor(Z', Z ⊗ Y)
   | id_W ⊗ -                | id_W ⊗ -
   v                         v
  Mor(W ⊗ Z' ⊗ X, W ⊗ Z) →  Mor(W ⊗ Z', W ⊗ Z ⊗ Y)

commutes, the two vertical maps being f ↦ 𝟙 W ⊗ f read through the associators.

def IsTensorCompatible (adj : tensorRight X ⊣ tensorRight Y) : Prop

CategoryTheory.Adjunction.unit_app_comp_tensorEvaluation_whiskerRight, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Monoidal/RigidAdjunction.lean, line 150.

The first identity that an adjunction tensorRight X ⊣ tensorRight Y supplies for free, with no compatibility with the tensor structure assumed: (ε ⊗ 1_Y) ∘ η_Y = 1_Y, where η_Y is the component of the unit at Y.

theorem unit_app_comp_tensorEvaluation_whiskerRight :
    adj.unit.app Y ≫ adj.tensorEvaluation ▷ Y = (λ_ Y).inv

CategoryTheory.Adjunction.tensorCoevaluation_whiskerRight_comp_counit_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Monoidal/RigidAdjunction.lean, line 163.

The second identity that an adjunction tensorRight X ⊣ tensorRight Y supplies for free, with no compatibility with the tensor structure assumed: ε_X ∘ (η ⊗ 1_X) = 1_X, where ε_X is the component of the counit at X.

theorem tensorCoevaluation_whiskerRight_comp_counit_app :
    adj.tensorCoevaluation ▷ X ≫ adj.counit.app X = (λ_ X).hom

CategoryTheory.ExactPairing.isTensorCompatible_tensorRightAdjunction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Monoidal/RigidAdjunction.lean, line 177.

The adjunction tensorRight X ⊣ tensorRight Y attached to an exact pairing is compatible with the tensor structure.

theorem ExactPairing.isTensorCompatible_tensorRightAdjunction (X Y : C) [ExactPairing X Y] :
    (tensorRightAdjunction X Y).IsTensorCompatible

CategoryTheory.Adjunction.IsTensorCompatible.exactPairing, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Monoidal/RigidAdjunction.lean, line 272.

The converse direction of Stacks 0FFR. A tensor-compatible adjunction tensorRight X ⊣ tensorRight Y exhibits Y as a left dual of X: its candidate coevaluation and evaluation satisfy both triangle identities of an exact pairing.

def exactPairing (h : adj.IsTensorCompatible) : ExactPairing X Y

Declarations registered for the tag:

Tag 0FFS, a lemma

Tag 0FFS in the Stacks Project.

Declarations registered for the tag:

Tag 0FN8, a lemma

Tag 0FN8 in the Stacks Project.

Declarations registered for the tag:

Tag 0FFY, a definition

Tag 0FFY in the Stacks Project.

Declarations registered for the tag:

Tag 0GWJ, a remark

Tag 0GWJ in the Stacks Project.

InternalHom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Monoidal/InternalHom.lean, line 42. References: SGA 4 IV (10.2).

Definition 1 (Internal hom). An internal hom on a monoidal category C consists of a bifunctor hom : Cᵒᵖ ⥤ C ⥤ C (contravariant in the first variable, covariant in the second) together with, for all objects X, Y, Z, a bijection Φ X Y Z : Mor(X, hom(Y, Z)) ≃ Mor(X ⊗ Y, Z) that is natural in X, in Y, and in Z.

This is the opening clause of Stacks 0GWJ: C has an internal hom if for every pair X, Y there is an object hom(X, Y) with Mor(X, hom(Y, Z)) = Mor(X ⊗ Y, Z) functorially in X, Y, Z.

structure InternalHom (C : Type u) [Category.{v} C] [MonoidalCategory C]

InternalHom.ev, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Monoidal/InternalHom.lean, line 76. The attribute's comment: “(1)”. References: SGA 7 VIII (1.6), “more general”.

Construction of (1) Evaluation. ev_{X,Y} := Φ (id_{hom(X,Y)}), the image of the identity under Φ.

def ev (X Y : C) : ih.homObj X Y ⊗ X ⟶ Y

InternalHom.comp, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Monoidal/InternalHom.lean, line 84. The attribute's comment: “(2)”.

Construction of (2) Composition. c_{X,Y,Z} is the image under Φ⁻¹ (using X as the tensoring object) of the composite hom(Y,Z) ⊗ hom(X,Y) ⊗ X → hom(Y,Z) ⊗ Y → Z given by (id ⊗ ev_{X,Y}) followed by ev_{Y,Z}.

def comp (X Y Z : C) : ih.homObj Y Z ⊗ ih.homObj X Y ⟶ ih.homObj X Z

InternalHom.tensorLeftMor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Monoidal/InternalHom.lean, line 92. The attribute's comment: “(3)”.

Construction of (3) Tensor on the left. t_{X,Y,Z} is the image under Φ⁻¹ of id_Z ⊗ ev_{X,Y} : Z ⊗ hom(X,Y) ⊗ X → Z ⊗ Y.

def tensorLeftMor (X Y Z : C) : Z ⊗ ih.homObj X Y ⟶ ih.homObj X (Z ⊗ Y)

InternalHom.coev, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Monoidal/InternalHom.lean, line 103. The attribute's comment: “(4)”.

Construction of (4) Unit / coevaluation. η_{X,Y} := ρ_Y⁻¹ ≫ (id_Y ⊗ u_X) ≫ t_{X,X,Y}.

def coev (X Y : C) : Y ⟶ ih.homObj X (Y ⊗ X)

InternalHom.internalCurryMor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Monoidal/InternalHom.lean, line 111. The attribute's comment: “(5)”.

Construction of (5) Internalized currying (symmetric case). d_{X,Y,Z} is the image under Φ⁻¹ (using hom(X,Y) as the tensoring object) of the composite hom(Y,Z) ⊗ X ⊗ hom(X,Y) → hom(Y,Z) ⊗ hom(X,Y) ⊗ X → hom(Y,Z) ⊗ Y → Z, where the first arrow uses the braiding σ_{X, hom(X,Y)}.

def internalCurryMor [BraidedCategory C] (X Y Z : C) :
    ih.homObj Y Z ⊗ X ⟶ ih.homObj (ih.homObj X Y) Z
Sources
LeanCategoryTheory.Functor.Monoidal · CategoryTheory.MonoidalCategory.invertible_tfae · CategoryTheory.MonoidalCategory.HasInverse · CategoryTheory.MonoidalCategory.IsInvertible · CategoryTheory.ExactPairing · CategoryTheory.tensorRightHomEquiv_whiskerRight_comp_comp · CategoryTheory.tensorLeftHomEquiv_whiskerLeft_comp_comp · CategoryTheory.tensorRightAdjunction

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.