Fibered categories

This file defines what it means for a functor p : 𝒳 ⥤ 𝒮 to be (pre)fibered.

Main definitions

• IsPreFibered p expresses 𝒳 is fibered over 𝒮 via a functor p : 𝒳 ⥤ 𝒮, as in SGA VI.6.1. This means that any morphism in the base 𝒮 can be lifted to a cartesian morphism in 𝒳.

• IsFibered p expresses 𝒳 is fibered over 𝒮 via a functor p : 𝒳 ⥤ 𝒮, as in SGA VI.6.1. This means that it is prefibered, and that the composition of any two cartesian morphisms is cartesian.

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

• A. Grothendieck, M. Raynaud, SGA 1

class CategoryTheory.Functor.IsPreFibered {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] (p : CategoryTheory.Functor 𝒳 𝒮) : Prop

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 φ

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 φ

class CategoryTheory.Functor.IsFibered {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] (p : CategoryTheory.Functor 𝒳 𝒮) extends p.IsPreFibered : Prop

Definition of a fibered category.

See SGA 1 VI.6.1.

• exists_isCartesian' : ∀ {a : 𝒳} {R : 𝒮} (f : R ⟶ p.obj a), ∃ (b : 𝒳), ∃ (φ : b ⟶ a), p.IsCartesian f φ
• comp : ∀ {R S T : 𝒮} (f : R ⟶ S) (g : S ⟶ T) {a b c : 𝒳} (φ : a ⟶ b) (ψ : b ⟶ c) [inst : p.IsCartesian f φ] [inst : p.IsCartesian g ψ], p.IsCartesian (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.comp φ ψ)

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 ψ] : p.IsCartesian (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.comp φ ψ)

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

• CategoryTheory.Functor.IsPreFibered.pullbackObj ha f = Classical.choose ⋯

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) : CategoryTheory.Functor.IsPreFibered.pullbackObj ha f ⟶ a

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

• CategoryTheory.Functor.IsPreFibered.pullbackMap ha f = Classical.choose ⋯

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) : p.IsCartesian f (CategoryTheory.Functor.IsPreFibered.pullbackMap ha f)

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) : p.obj (CategoryTheory.Functor.IsPreFibered.pullbackObj ha f) = R

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) : CategoryTheory.Functor.IsPreFibered.pullbackObj ha (CategoryTheory.CategoryStruct.comp g f) ≅ CategoryTheory.Functor.IsPreFibered.pullbackObj ⋯ g

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.