Module

FiniteLimitsAndColimits.lean

Nyll.EtaleFundamentalGroups.ContinuousActions.FiniteLimitsAndColimits

11 declarations indexed from sourceView source ↗

Module documentation

Finite limits and colimits of finite continuous actions

Finite limits and finite colimits of continuous actions on finite discrete spaces are again continuous. Consequently the inherited forgetful functor from finite continuous actions to finite sets preserves both.

This is the categorical exactness foundation used for Stacks Project, Tag 0BMV.

Imports6

Mathlib.CategoryTheory.Action.Continuous
Mathlib.CategoryTheory.Action.Limits
Mathlib.CategoryTheory.Limits.FintypeCat
Mathlib.CategoryTheory.Limits.FullSubcategory
Mathlib.Topology.Category.FinTopCat
Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic

Imported by6

lemma

hom_apply_rho

L42 ↗

CategoryTheory.ContAction.hom_apply_rho

Source context 8 commands

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

@[expose] public section
universe u v w
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.ContAction
variable {G : Type v} [Monoid G] [TopologicalSpace G]
omit [TopologicalSpace G] in

Lean source · statement

lemma hom_apply_rho {X Y : Action FintypeCat.{u} G}
    (f : X ⟶ Y) (g : G) (x : X.V) :
    ConcreteCategory.hom f.hom (ConcreteCategory.hom (X.ρ g) x) =
      ConcreteCategory.hom (Y.ρ g) (ConcreteCategory.hom f.hom x)

lemma

isContinuous_of_finite_limit

L49 ↗

CategoryTheory.ContAction.isContinuous_of_finite_limit

Source context 7 commands

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

@[expose] public section
universe u v w
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.ContAction
variable {G : Type v} [Monoid G] [TopologicalSpace G]

Lean source · statement

lemma isContinuous_of_finite_limit
    {J : Type} [SmallCategory J] [FinCategory J]
    (F : J ⥤ Action FintypeCat.{u} G) (c : Cone F) (hc : IsLimit c)
    (hF : ∀ j, Action.IsContinuous (F.obj j)) :
    Action.IsContinuous c.pt

lemma

isContinuous_of_finite_colimit

L90 ↗

CategoryTheory.ContAction.isContinuous_of_finite_colimit

Source context 7 commands

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

@[expose] public section
universe u v w
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.ContAction
variable {G : Type v} [Monoid G] [TopologicalSpace G]

Lean source · statement

lemma isContinuous_of_finite_colimit
    {J : Type} [SmallCategory J] [FinCategory J]
    (F : J ⥤ Action FintypeCat.{u} G) (c : Cocone F) (hc : IsColimit c)
    (hF : ∀ j, Action.IsContinuous (F.obj j)) :
    Action.IsContinuous c.pt

instance

isClosedUnderLimitsOfShape_isContinuous

L119 ↗

CategoryTheory.ContAction.isClosedUnderLimitsOfShape_isContinuous

Documentation

Continuity of an action on a finite discrete space is closed under limits indexed by finite categories.

Source context 7 commands

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

@[expose] public section
universe u v w
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.ContAction
variable {G : Type v} [Monoid G] [TopologicalSpace G]

Lean source · full declaration

instance isClosedUnderLimitsOfShape_isContinuous
    {J : Type} [SmallCategory J] [FinCategory J] :
    ObjectProperty.IsClosedUnderLimitsOfShape
      (Action.IsContinuous (V := FintypeCat.{u}) (G := G)) J where
  limitsOfShape_le _ h := by
    obtain ⟨h⟩ := h
    exact isContinuous_of_finite_limit h.diag h.toLimitPresentation.cone
      h.isLimit h.prop_diag_obj

instance

isClosedUnderColimitsOfShape_isContinuous

L130 ↗

CategoryTheory.ContAction.isClosedUnderColimitsOfShape_isContinuous

Documentation

Continuity of an action on a finite discrete space is closed under colimits indexed by finite categories.

Source context 7 commands

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

@[expose] public section
universe u v w
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.ContAction
variable {G : Type v} [Monoid G] [TopologicalSpace G]

Lean source · full declaration

instance isClosedUnderColimitsOfShape_isContinuous
    {J : Type} [SmallCategory J] [FinCategory J] :
    ObjectProperty.IsClosedUnderColimitsOfShape
      (Action.IsContinuous (V := FintypeCat.{u}) (G := G)) J where
  colimitsOfShape_le _ h := by
    obtain ⟨h⟩ := h
    exact isContinuous_of_finite_colimit h.diag h.toColimitPresentation.cocone
      h.isColimit h.prop_diag_obj

instance

hasFiniteLimits

L140 ↗

CategoryTheory.ContAction.hasFiniteLimits

Documentation

Finite continuous actions of a topological monoid have finite limits.

Source context 7 commands

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

@[expose] public section
universe u v w
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.ContAction
variable {G : Type v} [Monoid G] [TopologicalSpace G]

Lean source · full declaration

instance hasFiniteLimits :
    HasFiniteLimits (ContAction FintypeCat.{u} G) where
  out _ _ _ := inferInstance

instance

hasFiniteColimits

L145 ↗

CategoryTheory.ContAction.hasFiniteColimits

Documentation

Finite continuous actions of a topological monoid have finite colimits.

Source context 7 commands

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

@[expose] public section
universe u v w
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.ContAction
variable {G : Type v} [Monoid G] [TopologicalSpace G]

Lean source · full declaration

instance hasFiniteColimits :
    HasFiniteColimits (ContAction FintypeCat.{u} G) where
  out _ _ _ := inferInstance

instance

forgetPreservesFiniteLimits

L151 ↗

CategoryTheory.ContAction.forgetPreservesFiniteLimits

Documentation

The inherited forgetful functor from finite continuous actions to finite sets preserves finite limits.

Source context 7 commands

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

@[expose] public section
universe u v w
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.ContAction
variable {G : Type v} [Monoid G] [TopologicalSpace G]

Lean source · full declaration

instance forgetPreservesFiniteLimits :
    PreservesFiniteLimits
      (forget₂ (ContAction FintypeCat.{u} G) FintypeCat) where
  preservesFiniteLimits _ _ _ := by
    change PreservesLimitsOfShape _
      (ObjectProperty.ι
          (Action.IsContinuous (V := FintypeCat.{u}) (G := G)) ⋙
        Action.forget FintypeCat G)
    infer_instance

instance

forgetPreservesFiniteColimits

L163 ↗

CategoryTheory.ContAction.forgetPreservesFiniteColimits

Documentation

The inherited forgetful functor from finite continuous actions to finite sets preserves finite colimits.

Source context 7 commands

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

@[expose] public section
universe u v w
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.ContAction
variable {G : Type v} [Monoid G] [TopologicalSpace G]

Lean source · full declaration

instance forgetPreservesFiniteColimits :
    PreservesFiniteColimits
      (forget₂ (ContAction FintypeCat.{u} G) FintypeCat) where
  preservesFiniteColimits _ _ _ := by
    change PreservesColimitsOfShape _
      (ObjectProperty.ι
          (Action.IsContinuous (V := FintypeCat.{u}) (G := G)) ⋙
        Action.forget FintypeCat G)
    infer_instance

instance

resPreservesFiniteLimits

L174 ↗

CategoryTheory.ContAction.resPreservesFiniteLimits

Documentation

Restriction of finite continuous actions preserves finite limits.

Source context 7 commands

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

@[expose] public section
universe u v w
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.ContAction
variable {G : Type v} [Monoid G] [TopologicalSpace G]

Lean source · statement

instance resPreservesFiniteLimits
    {H : Type w} [Monoid H] [TopologicalSpace H]
    (f : G →ₜ* H) :
    PreservesFiniteLimits (ContAction.res FintypeCat.{u} f)

instance

resPreservesFiniteColimits

L198 ↗

CategoryTheory.ContAction.resPreservesFiniteColimits

Documentation

Restriction of finite continuous actions preserves finite colimits.

Source context 7 commands

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

@[expose] public section
universe u v w
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.ContAction
variable {G : Type v} [Monoid G] [TopologicalSpace G]

Lean source · statement

instance resPreservesFiniteColimits
    {H : Type w} [Monoid H] [TopologicalSpace H]
    (f : G →ₜ* H) :
    PreservesFiniteColimits (ContAction.res FintypeCat.{u} f)

Module documentation

Finite limits and colimits of finite continuous actions

Declarations