Module

CategoricalDescent.lean

Nyll.EtaleFundamentalGroups.GenericTensor.FilteredColimit.CategoricalDescent

8 declarations indexed from sourceView source ↗

Module documentation

Finite-presentation descent through the actual pushout functor

The only compactness inputs are finite presentability of the two original models. No descent map, comparison, or inverse equation is an input field.

Imports8

Nyll.EtaleFundamentalGroups.GenericTensor.FilteredColimit.CategoricalPushout
Mathlib.CategoryTheory.Adjunction.Limits
Mathlib.CategoryTheory.Filtered.Connected
Mathlib.CategoryTheory.Functor.Const
Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
Mathlib.CategoryTheory.Limits.Preserves.Over
Mathlib.CategoryTheory.Presentable.Finite
Mathlib.CategoryTheory.Presentable.Basic

Imported by4

theorem

map_preservesColimit

L35 ↗

CategoryTheory.CategoricalTensorDescent.map_preservesColimit

Documentation

Restriction along an arrow preserves connected colimits: after forgetting the base arrow it is the original underlying diagram.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory CategoryTheory.Limits
universe u v w
namespace CategoryTheory.CategoricalTensorDescent
variable {C : Type u} [Category.{v} C] {R : C}

Lean source · statement

theorem map_preservesColimit
    {J : Type w} [SmallCategory J] [IsFiltered J]
    {X Y : C} (f : X ⟶ Y) (F : J ⥤ Under Y) :
    PreservesColimit F (Under.map f)

theorem

coefficientFunctor_preservesColimit

L48 ↗

CategoryTheory.CategoricalTensorDescent.coefficientFunctor_preservesColimit

Documentation

Push out along the model and restrict the base. Both colimit-preservation facts are supplied by existing adjunction and connected-colimit machinery.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory CategoryTheory.Limits
universe u v w
namespace CategoryTheory.CategoricalTensorDescent
variable {C : Type u} [Category.{v} C] {R : C}
variable [HasPushouts C]

Lean source · statement

theorem coefficientFunctor_preservesColimit
    {J : Type w} [SmallCategory J] [IsFiltered J]
    (D : Under R) (F : J ⥤ Under R) :
    PreservesColimit F (coefficientFunctor D)

theorem

exists_hom_stage

L59 ↗

CategoryTheory.CategoricalTensorDescent.exists_hom_stage

Documentation

An arbitrary map after coefficient colimit descends from its transpose, using compactness of the original source model.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory CategoryTheory.Limits
universe u v w
namespace CategoryTheory.CategoricalTensorDescent
variable {C : Type u} [Category.{v} C] {R : C}
variable [HasPushouts C]

Lean source · statement

theorem exists_hom_stage
    {J : Type w} [SmallCategory J] [IsFiltered J]
    (B D : Under R) [IsFinitelyPresentable.{w} B]
    (F : J ⥤ Under R) (c : Cocone F) (hc : IsColimit c)
    (f : model c.pt B ⟶ model c.pt D) :
    ∃ (i : J) (fi : model (F.obj i) B ⟶ model (F.obj i) D),
      extend (c.ι.app i) fi = f

theorem

exists_eq_stage

L77 ↗

CategoryTheory.CategoricalTensorDescent.exists_eq_stage

Documentation

Equality after passage to the coefficient colimit holds at a later stage. Compactness is applied to the original source, not to the stage coefficient.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory CategoryTheory.Limits
universe u v w
namespace CategoryTheory.CategoricalTensorDescent
variable {C : Type u} [Category.{v} C] {R : C}
variable [HasPushouts C]

Lean source · statement

theorem exists_eq_stage
    {J : Type w} [SmallCategory J] [IsFiltered J]
    (B D : Under R) [IsFinitelyPresentable.{w} B]
    (F : J ⥤ Under R) (c : Cocone F) (hc : IsColimit c)
    (i : J) (f g : model (F.obj i) B ⟶ model (F.obj i) D)
    (hfg : extend (c.ι.app i) f = extend (c.ι.app i) g) :
    ∃ (j : J) (hij : i ⟶ j), extend (F.map hij) f = extend (F.map hij) g

theorem

extend_to_colimit

L99 ↗

CategoryTheory.CategoricalTensorDescent.extend_to_colimit

Documentation

Extending a descended map farther along the diagram preserves its exact image at the colimit. This is functoriality and the cocone equation.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory CategoryTheory.Limits
universe u v w
namespace CategoryTheory.CategoricalTensorDescent
variable {C : Type u} [Category.{v} C] {R : C}
variable [HasPushouts C]

Lean source · statement

theorem extend_to_colimit
    {J : Type w} [SmallCategory J]
    {B D : Under R} (F : J ⥤ Under R) (c : Cocone F)
    {i j : J} (h : i ⟶ j) (f : model (F.obj i) B ⟶ model (F.obj i) D) :
    extend (c.ι.app j) (extend (F.map h) f) = extend (c.ι.app i) f

theorem

exists_hom_pair_stage

L107 ↗

CategoryTheory.CategoricalTensorDescent.exists_hom_pair_stage

Documentation

Both arbitrary arrows descend to a common coefficient stage.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory CategoryTheory.Limits
universe u v w
namespace CategoryTheory.CategoricalTensorDescent
variable {C : Type u} [Category.{v} C] {R : C}
variable [HasPushouts C]

Lean source · statement

theorem exists_hom_pair_stage
    {J : Type w} [SmallCategory J] [IsFiltered J]
    (B D : Under R) [IsFinitelyPresentable.{w} B] [IsFinitelyPresentable.{w} D]
    (F : J ⥤ Under R) (c : Cocone F) (hc : IsColimit c)
    (f : model c.pt B ⟶ model c.pt D) (g : model c.pt D ⟶ model c.pt B) :
    ∃ (k : J) (fk : model (F.obj k) B ⟶ model (F.obj k) D)
      (gk : model (F.obj k) D ⟶ model (F.obj k) B),
      extend (c.ι.app k) fk = f ∧ extend (c.ι.app k) gk = g

theorem

exists_inverse_pair_stage

L125 ↗

CategoryTheory.CategoricalTensorDescent.exists_inverse_pair_stage

Documentation

The two inverse equations can be imposed consecutively along a common tail. The first survives the second extension by functoriality.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory CategoryTheory.Limits
universe u v w
namespace CategoryTheory.CategoricalTensorDescent
variable {C : Type u} [Category.{v} C] {R : C}
variable [HasPushouts C]

Lean source · statement

theorem exists_inverse_pair_stage
    {J : Type w} [SmallCategory J] [IsFiltered J]
    (B D : Under R) [IsFinitelyPresentable.{w} B] [IsFinitelyPresentable.{w} D]
    (F : J ⥤ Under R) (c : Cocone F) (hc : IsColimit c)
    (e : model c.pt B ≅ model c.pt D) :
    ∃ (k : J) (fk : model (F.obj k) B ⟶ model (F.obj k) D)
      (gk : model (F.obj k) D ⟶ model (F.obj k) B),
      fk ≫ gk = 𝟙 (model (F.obj k) B) ∧
      gk ≫ fk = 𝟙 (model (F.obj k) D) ∧
      extend (c.ι.app k) fk = e.hom ∧ extend (c.ι.app k) gk = e.inv

theorem

exists_iso_stage

L168 ↗

CategoryTheory.CategoricalTensorDescent.exists_iso_stage

Documentation

An arbitrary base-changed isomorphism descends, retaining both exact coefficient-extension equations.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory CategoryTheory.Limits
universe u v w
namespace CategoryTheory.CategoricalTensorDescent
variable {C : Type u} [Category.{v} C] {R : C}
variable [HasPushouts C]

Lean source · statement

theorem exists_iso_stage
    {J : Type w} [SmallCategory J] [IsFiltered J]
    (B D : Under R) [IsFinitelyPresentable.{w} B] [IsFinitelyPresentable.{w} D]
    (F : J ⥤ Under R) (c : Cocone F) (hc : IsColimit c)
    (e : model c.pt B ≅ model c.pt D) :
    ∃ (k : J) (ek : model (F.obj k) B ≅ model (F.obj k) D),
      extend (c.ι.app k) ek.hom = e.hom ∧ extend (c.ι.app k) ek.inv = e.inv

Module documentation

Finite-presentation descent through the actual pushout functor

Declarations