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 𝒳.

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.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 φ

noncomputable def CategoryTheory.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.IsPreFibered.pullbackObj ha f = Classical.choose ⋯

noncomputable def CategoryTheory.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.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.IsPreFibered.pullbackMap ha f = Classical.choose ⋯

instance CategoryTheory.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.IsPreFibered.pullbackMap ha f)

Equations

• ⋯ = ⋯

theorem CategoryTheory.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.IsPreFibered.pullbackObj ha f) = R