Module

TopCatCompat.lean

Nyll.EtaleFundamentalGroups.ContinuousActions.TopCatCompat

4 declarations indexed from sourceView source ↗

Module documentation

The identity forgetful functor on `TopCat`

HasForget₂ deliberately has no general self-instance. The continuous-action API nevertheless needs the canonical identity forgetful functor when its ambient concrete category is TopCat itself.

Imports1

Mathlib.CategoryTheory.Action.Continuous

Imported by3

instance

topCatHasForget₂Self

L28 ↗

CategoryTheory.topCatHasForget₂Self

Documentation

The canonical identity forgetful functor from TopCat to itself.

Source context 4 commands

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

@[expose] public section
open CategoryTheory
namespace CategoryTheory
universe u v

Lean source · full declaration

instance topCatHasForget₂Self : HasForget₂ TopCat.{u} TopCat.{u} where
  forget₂ := 𝟭 TopCat.{u}

instance

topCatConcrete

L36 ↗

CategoryTheory.DiscreteContAction.topCatConcrete

Source context 5 commands

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

@[expose] public section
open CategoryTheory
namespace CategoryTheory
universe u v
namespace DiscreteContAction

-- `DiscreteContAction` is a non-reducible full subcategory in mathlib.  Make
-- its canonical concrete and forgetful instances available for `TopCat`
-- without relying on consumers unfolding that definition during search.

Lean source · full declaration

instance topCatConcrete {G : Type v} [Monoid G] [TopologicalSpace G] :
    ConcreteCategory (DiscreteContAction TopCat.{u} G)
      (fun S T => Action.HomSubtype TopCat.{u} G S.obj.obj T.obj.obj) := by
  exact ObjectProperty.FullSubcategory.concreteCategory
    (ContAction.IsDiscrete (V := TopCat.{u}) (G := G))

instance

topCatHasForget₂

L42 ↗

CategoryTheory.DiscreteContAction.topCatHasForget₂

Source context 5 commands

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

@[expose] public section
open CategoryTheory
namespace CategoryTheory
universe u v
namespace DiscreteContAction

-- `DiscreteContAction` is a non-reducible full subcategory in mathlib.  Make
-- its canonical concrete and forgetful instances available for `TopCat`
-- without relying on consumers unfolding that definition during search.

Lean source · statement

instance topCatHasForget₂ {G : Type v} [Monoid G] [TopologicalSpace G] :
    HasForget₂ (DiscreteContAction TopCat.{u} G) TopCat.{u}

instance

carrierMulAction

L50 ↗

CategoryTheory.DiscreteContAction.carrierMulAction

Documentation

The carrier of a discrete continuous TopCat-action has the original multiplicative action.

Source context 5 commands

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

@[expose] public section
open CategoryTheory
namespace CategoryTheory
universe u v
namespace DiscreteContAction

-- `DiscreteContAction` is a non-reducible full subcategory in mathlib.  Make
-- its canonical concrete and forgetful instances available for `TopCat`
-- without relying on consumers unfolding that definition during search.

Lean source · statement

instance carrierMulAction {G : Type v} [Monoid G] [TopologicalSpace G]
    (S : DiscreteContAction TopCat.{u} G) :
    MulAction G
      ((forget₂ (DiscreteContAction TopCat.{u} G) TopCat.{u}).obj S)

Module documentation

The identity forgetful functor on TopCat

Declarations

topCatHasForget₂Self

topCatConcrete

topCatHasForget₂

carrierMulAction

The identity forgetful functor on `TopCat`