Documentation

Mathlib.CategoryTheory.FiberedCategory.Fibered

Fibered categories #

This file defines what it means for a functor p : š’³ ā„¤ š’® to be (pre)fibered.

Main definitions #

In the literature one often sees the notion of a fibered category defined as the existence of strongly cartesian morphisms lying over any given morphism in the base. This is equivalent to the notion above, and we give an alternate constructor IsFibered.of_exists_isCartesian' for constructing a fibered category this way.

Implementation #

The constructor of IsPreFibered is called exists_isCartesian'. The reason for the prime is that when wanting to apply this condition, it is recommended to instead use the lemma exists_isCartesian (without the prime), which is more applicable with respect to non-definitional equalities.

References #

Definition of a prefibered category.

See SGA 1 VI.6.1.

  • exists_isCartesian' : āˆ€ {a : š’³} {R : š’®} (f : R āŸ¶ p.obj a), āˆƒ (b : š’³), āˆƒ (Ļ† : b āŸ¶ a), p.IsCartesian f Ļ†
Instances
    theorem CategoryTheory.Functor.IsPreFibered.exists_isCartesian' {š’® : Type uā‚} {š’³ : Type uā‚‚} [CategoryTheory.Category.{vā‚, uā‚} š’®] [CategoryTheory.Category.{vā‚‚, uā‚‚} š’³] {p : CategoryTheory.Functor š’³ š’®} [self : p.IsPreFibered] {a : š’³} {R : š’®} (f : R āŸ¶ p.obj a) :
    āˆƒ (b : š’³), āˆƒ (Ļ† : b āŸ¶ a), p.IsCartesian f Ļ†
    theorem CategoryTheory.IsPreFibered.exists_isCartesian {š’® : Type uā‚} {š’³ : Type uā‚‚} [CategoryTheory.Category.{vā‚, uā‚} š’®] [CategoryTheory.Category.{vā‚‚, uā‚‚} š’³] (p : CategoryTheory.Functor š’³ š’®) [p.IsPreFibered] {a : š’³} {R : š’®} {S : š’®} (ha : p.obj a = S) (f : R āŸ¶ S) :
    āˆƒ (b : š’³), āˆƒ (Ļ† : b āŸ¶ a), p.IsCartesian f Ļ†

    Definition of a fibered category.

    See SGA 1 VI.6.1.

    Instances
      theorem CategoryTheory.Functor.IsFibered.comp {š’® : Type uā‚} {š’³ : Type uā‚‚} [CategoryTheory.Category.{vā‚, uā‚} š’®] [CategoryTheory.Category.{vā‚‚, uā‚‚} š’³] {p : CategoryTheory.Functor š’³ š’®} [self : p.IsFibered] {R : š’®} {S : š’®} {T : š’®} (f : R āŸ¶ S) (g : S āŸ¶ T) {a : š’³} {b : š’³} {c : š’³} (Ļ† : a āŸ¶ b) (Ļˆ : b āŸ¶ c) [p.IsCartesian f Ļ†] [p.IsCartesian g Ļˆ] :
      instance CategoryTheory.instIsCartesianCompOfIsFibered {š’® : Type uā‚} {š’³ : Type uā‚‚} [CategoryTheory.Category.{vā‚, uā‚} š’®] [CategoryTheory.Category.{vā‚‚, uā‚‚} š’³] (p : CategoryTheory.Functor š’³ š’®) [p.IsFibered] {R : š’®} {S : š’®} {T : š’®} (f : R āŸ¶ S) (g : S āŸ¶ T) {a : š’³} {b : š’³} {c : š’³} (Ļ† : a āŸ¶ b) (Ļˆ : b āŸ¶ c) [p.IsCartesian f Ļ†] [p.IsCartesian g Ļˆ] :
      Equations
      • ā‹Æ = ā‹Æ
      noncomputable def CategoryTheory.Functor.IsPreFibered.pullbackObj {š’® : Type uā‚} {š’³ : Type uā‚‚} [CategoryTheory.Category.{vā‚, uā‚} š’®] [CategoryTheory.Category.{vā‚‚, uā‚‚} š’³] {p : CategoryTheory.Functor š’³ š’®} [p.IsPreFibered] {R : š’®} {S : š’®} {a : š’³} (ha : p.obj a = S) (f : R āŸ¶ S) :
      š’³

      Given a fibered category p : š’³ ā„¤ š’«, a morphism f : R āŸ¶ S and an object a lying over S, then pullbackObj is the domain of some choice of a cartesian morphism lying over f with codomain a.

      Equations
      Instances For
        noncomputable def CategoryTheory.Functor.IsPreFibered.pullbackMap {š’® : Type uā‚} {š’³ : Type uā‚‚} [CategoryTheory.Category.{vā‚, uā‚} š’®] [CategoryTheory.Category.{vā‚‚, uā‚‚} š’³] {p : CategoryTheory.Functor š’³ š’®} [p.IsPreFibered] {R : š’®} {S : š’®} {a : š’³} (ha : p.obj a = S) (f : R āŸ¶ S) :

        Given a fibered category p : š’³ ā„¤ š’«, a morphism f : R āŸ¶ S and an object a lying over S, then pullbackMap is a choice of a cartesian morphism lying over f with codomain a.

        Equations
        Instances For
          instance CategoryTheory.Functor.IsPreFibered.pullbackMap.IsCartesian {š’® : Type uā‚} {š’³ : Type uā‚‚} [CategoryTheory.Category.{vā‚, uā‚} š’®] [CategoryTheory.Category.{vā‚‚, uā‚‚} š’³] {p : CategoryTheory.Functor š’³ š’®} [p.IsPreFibered] {R : š’®} {S : š’®} {a : š’³} (ha : p.obj a = S) (f : R āŸ¶ S) :
          Equations
          • ā‹Æ = ā‹Æ
          theorem CategoryTheory.Functor.IsPreFibered.pullbackObj_proj {š’® : Type uā‚} {š’³ : Type uā‚‚} [CategoryTheory.Category.{vā‚, uā‚} š’®] [CategoryTheory.Category.{vā‚‚, uā‚‚} š’³] {p : CategoryTheory.Functor š’³ š’®} [p.IsPreFibered] {R : š’®} {S : š’®} {a : š’³} (ha : p.obj a = S) (f : R āŸ¶ S) :
          instance CategoryTheory.Functor.IsFibered.isStronglyCartesian_of_isCartesian {š’® : Type uā‚} {š’³ : Type uā‚‚} [CategoryTheory.Category.{vā‚, uā‚} š’®] [CategoryTheory.Category.{vā‚‚, uā‚‚} š’³] (p : CategoryTheory.Functor š’³ š’®) [p.IsFibered] {R : š’®} {S : š’®} (f : R āŸ¶ S) {a : š’³} {b : š’³} (Ļ† : a āŸ¶ b) [p.IsCartesian f Ļ†] :
          p.IsStronglyCartesian f Ļ†

          In a fibered category, any cartesian morphism is strongly cartesian.

          Equations
          • ā‹Æ = ā‹Æ
          theorem CategoryTheory.Functor.IsFibered.isStronglyCartesian_of_exists_isCartesian {š’® : Type uā‚} {š’³ : Type uā‚‚} [CategoryTheory.Category.{vā‚, uā‚} š’®] [CategoryTheory.Category.{vā‚‚, uā‚‚} š’³] (p : CategoryTheory.Functor š’³ š’®) (h : āˆ€ (a : š’³) (R : š’®) (f : R āŸ¶ p.obj a), āˆƒ (b : š’³), āˆƒ (Ļ† : b āŸ¶ a), p.IsStronglyCartesian f Ļ†) {R : š’®} {S : š’®} (f : R āŸ¶ S) {a : š’³} {b : š’³} (Ļ† : a āŸ¶ b) [p.IsCartesian f Ļ†] :
          p.IsStronglyCartesian f Ļ†

          In a category which admits strongly cartesian pullbacks, any cartesian morphism is strongly cartesian. This is a helper-lemma for the fact that admitting strongly cartesian pullbacks implies being fibered.

          theorem CategoryTheory.Functor.IsFibered.of_exists_isStronglyCartesian {š’® : Type uā‚} {š’³ : Type uā‚‚} [CategoryTheory.Category.{vā‚, uā‚} š’®] [CategoryTheory.Category.{vā‚‚, uā‚‚} š’³] {p : CategoryTheory.Functor š’³ š’®} (h : āˆ€ (a : š’³) (R : š’®) (f : R āŸ¶ p.obj a), āˆƒ (b : š’³), āˆƒ (Ļ† : b āŸ¶ a), p.IsStronglyCartesian f Ļ†) :
          p.IsFibered

          Alternate constructor for IsFibered, a functor p : š’³ ā„¤ š’“ is fibered if any diagram of the form

                    a
                    -
                    |
                    v
          R --f--> p(a)
          

          admits a strongly cartesian lift b āŸ¶ a of f.

          noncomputable def CategoryTheory.Functor.IsFibered.pullbackPullbackIso {š’® : Type uā‚} {š’³ : Type uā‚‚} [CategoryTheory.Category.{vā‚, uā‚} š’®] [CategoryTheory.Category.{vā‚‚, uā‚‚} š’³] {p : CategoryTheory.Functor š’³ š’®} [p.IsFibered] {R : š’®} {S : š’®} {T : š’®} {a : š’³} (ha : p.obj a = S) (f : R āŸ¶ S) (g : T āŸ¶ R) :

          Given a diagram

                            a
                            -
                            |
                            v
          T --g--> R --f--> S
          

          we have an isomorphism T Ɨ_S a ā‰… T Ɨ_R (R Ɨ_S a)

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For