Documentation

LeanPool.DirectedTopologyLean4.DTop

LeanPool.DirectedTopologyLean4.DTop #

source
structure dTopCat :
Type (u + 1)

The category of directed topological spaces.

  • carrier : Type u

    The underlying type of a directed topological space.

  • str : DirectedSpace ↑self
Instances For
    source
    @[implicit_reducible]
    instance dTopCat.instCoeSortType :
    CoeSort dTopCat (Type u)
    Equations
    source
    def dTopCat.of (X : Type u) [DirectedSpace X] :
    dTopCat

    Construct a bundled dTopCat from the underlying type and the typeclass.

    Equations
    Instances For
      source
      @[simp]
      theorem dTopCat.coe_of (X : Type u) [DirectedSpace X] :
      ↑(of X) = X
      source
      structure dTopCat.Hom (X Y : dTopCat) :
      Type u

      The type of morphisms in dTopCat.

      Instances For
        source
        theorem dTopCat.Hom.ext_iff {X Y : dTopCat} {x y : X.Hom Y} :
        x = y ↔ x.hom' = y.hom'
        source
        theorem dTopCat.Hom.ext {X Y : dTopCat} {x y : X.Hom Y} (hom' : x.hom' = y.hom') :
        x = y
        source
        @[implicit_reducible]
        instance dTopCat.instCategory :
        CategoryTheory.Category.{u_1, u_1 + 1} dTopCat
        Equations
        • One or more equations did not get rendered due to their size.
        source
        @[implicit_reducible]
        instance dTopCat.concreteCategory :
        CategoryTheory.ConcreteCategory dTopCat fun (X Y : dTopCat) => D(↑X,↑Y)
        Equations
        • One or more equations did not get rendered due to their size.
        source
        @[reducible, inline]
        abbrev dTopCat.Hom.hom {X Y : dTopCat} (f : X.Hom Y) :
        D(↑X,↑Y)

        Turn a morphism in dTopCat back into a DirectedMap.

        Equations
        Instances For
          source
          @[reducible, inline]
          abbrev dTopCat.ofHom {X Y : Type u} [DirectedSpace X] [DirectedSpace Y] (f : D(X,Y)) :
          of X ⟶ of Y

          Typecheck a DirectedMap as a morphism in dTopCat.

          Equations
          Instances For
            source
            @[simp]
            theorem dTopCat.hom_id {X : dTopCat} :
            Hom.hom (CategoryTheory.CategoryStruct.id X) = DirectedMap.id ↑X
            source
            @[simp]
            theorem dTopCat.id_app (X : dTopCat) (x : ↑X) :
            (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) x = x
            source
            @[simp]
            theorem dTopCat.hom_comp {X Y Z : dTopCat} (f : X ⟶ Y) (g : Y ⟶ Z) :
            Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (Hom.hom g).comp (Hom.hom f)
            source
            @[simp]
            theorem dTopCat.comp_app {X Y Z : dTopCat} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↑X) :
            (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x = (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)
            source
            theorem dTopCat.hom_ext {X Y : dTopCat} {f g : X ⟶ Y} (hf : Hom.hom f = Hom.hom g) :
            f = g
            source
            theorem dTopCat.hom_ext_iff {X Y : dTopCat} {f g : X ⟶ Y} :
            f = g ↔ Hom.hom f = Hom.hom g
            source
            theorem dTopCat.ext {X Y : dTopCat} {f g : X ⟶ Y} (w : ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x) :
            f = g
            source
            theorem dTopCat.ext_iff {X Y : dTopCat} {f g : X ⟶ Y} :
            f = g ↔ ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x
            source
            @[simp]
            theorem dTopCat.hom_ofHom {X Y : Type u} [DirectedSpace X] [DirectedSpace Y] (f : D(X,Y)) :
            Hom.hom (ofHom f) = f
            source
            @[simp]
            theorem dTopCat.ofHom_hom {X Y : dTopCat} (f : X ⟶ Y) :
            ofHom (Hom.hom f) = f
            source
            @[simp]
            theorem dTopCat.ofHom_id {X : Type u} [DirectedSpace X] :
            ofHom (DirectedMap.id X) = CategoryTheory.CategoryStruct.id (of X)
            source
            @[simp]
            theorem dTopCat.ofHom_comp {X Y Z : Type u} [DirectedSpace X] [DirectedSpace Y] [DirectedSpace Z] (f : D(X,Y)) (g : D(Y,Z)) :
            ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (ofHom f) (ofHom g)
            source
            @[implicit_reducible]
            instance dTopCat.subspaceCoe {X : dTopCat} :
            CoeTC (Set ↑X) dTopCat
            Equations
            source
            def dTopCat.DirectedSubtypeHom {X : dTopCat} (Y : Set ↑X) :
            of ↑Y ⟶ X

            The inclusion of a directed subspace into its ambient space.

            Equations
            Instances For
              source
              def dTopCat.DirectedSubsetHom {X : dTopCat} {Y₀ Y₁ : Set ↑X} (h : Y₀ ⊆ Y₁) :
              of ↑Y₀ ⟶ of ↑Y₁

              The inclusion between two directed subspaces, given a subset relation.

              Equations
              Instances For