SpecificationCategory

Difficulty: optional — 3 definitions, 0 abbreviations, 0 lemmas, 4 theorems, 0 examples.

definition theorem
legend
instance Specification.category {I : InterfaceOld} : CategoryTheory.Category.{0, 0} (Specification I)
Show details 
| Specification.category = Preorder.smallCategory (Specification I)

Complexity: 29 (size of the value term)

Outer dependencies: InterfaceOld, Specification

Inner dependencies: InterfaceOld.Value

Mathlib dependencies: CategoryTheory.Category

Used by: Specification.binaryCone, Specification.cartesianMonoidalCategory, Specification.closed, Specification.monoidalClosed, Specification.terminalCone

def Specification.terminalCone.{u_1} {I : InterfaceOld} :
  CategoryTheory.Limits.LimitCone (CategoryTheory.Functor.empty (Specification I))
Show details 
| Specification.terminalCone =
  {
    cone :=
      { pt := ⊤,
        π :=
          { app := fun X => ⋯.mpr (CategoryTheory.Discrete.casesOn X fun as => ⋯.elim),
            naturality := ⋯ } },
    isLimit :=
      CategoryTheory.Limits.isLimitChangeEmptyCone (Specification I)
        (Preorder.isTerminalTop (Specification I))
        { pt := ⊤,
          π :=
            { app := fun X => ⋯.mpr (CategoryTheory.Discrete.casesOn X fun as => ⋯.elim),
              naturality := ⋯ } }
        (CategoryTheory.Iso.refl (CategoryTheory.Limits.asEmptyCone ⊤).pt) }

Complexity: 1749 (size of the value term)

Outer dependencies: InterfaceOld, Specification, Specification.category

Inner dependencies: InterfaceOld.Value

Mathlib dependencies: CategoryTheory.Discrete, CategoryTheory.Functor, CategoryTheory.Functor.const, CategoryTheory.Functor.const_obj_map, CategoryTheory.Functor.const_obj_obj, CategoryTheory.Functor.empty, CategoryTheory.Iso.refl, CategoryTheory.Limits.LimitCone, CategoryTheory.Limits.asEmptyCone, CategoryTheory.Limits.isLimitChangeEmptyCone, CategoryTheory.congrArg_cast_hom_left, CategoryTheory.eqToHom, Preorder.isTerminalTop

Lean core dependencies: Eq, Eq.mpr, Eq.trans, False.elim, PEmpty, True, congr, congrArg, congrFun', eq_self, forall_congr, id, implies_true, of_eq_true

Used by: Specification.cartesianMonoidalCategory

def Specification.binaryCone {I : InterfaceOld} (A B : Specification I) :
  CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair A B)
Show details 
| A.binaryCone B =
  {
    cone :=
      CategoryTheory.Limits.BinaryFan.mk (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯),
    isLimit := Preorder.isLimitBinaryFan A B }

Complexity: 341 (size of the value term)

Outer dependencies: InterfaceOld, Specification, Specification.category

Inner dependencies: InterfaceOld.Value

Mathlib dependencies: CategoryTheory.Discrete, CategoryTheory.Limits.BinaryFan.mk, CategoryTheory.Limits.LimitCone, CategoryTheory.Limits.WalkingPair, CategoryTheory.Limits.pair, CategoryTheory.homOfLE, Preorder.isLimitBinaryFan, inf_le_left, inf_le_right

Used by: Specification.cartesianMonoidalCategory

instance Specification.cartesianMonoidalCategory {I : InterfaceOld} :
  CategoryTheory.CartesianMonoidalCategory (Specification I)
Show details 
| Specification.cartesianMonoidalCategory =
  CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts Specification.terminalCone
    Specification.binaryCone

Complexity: 19 (size of the value term)

Outer dependencies: InterfaceOld, Specification, Specification.category

Inner dependencies: Specification.binaryCone, Specification.terminalCone

Mathlib dependencies: CategoryTheory.CartesianMonoidalCategory, CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts

Used by: Specification.closed, Specification.monoidalClosed

theorem Specification.galoisConnection {I : InterfaceOld} (A : Specification I) :
  GaloisConnection (fun C => A ⊓ C) fun B => A ⇨ B
Show details 
fun {I} A x x_1 => Iff.symm le_himp_iff'

Complexity: 257 (size of the value term)

Dependencies: InterfaceOld, InterfaceOld.Value, Specification

Mathlib dependencies: GaloisConnection, le_himp_iff'

Lean core dependencies: Iff.symm

Used by: Specification.closed

def Specification.closed {I : InterfaceOld} (A : Specification I) : CategoryTheory.Closed A
Show details 
| A.closed =
  { rightAdj := ⋯.functor,
    adj :=
      have h := ⋯;
      ⋯.mpr ⋯.adjunction }

Complexity: 856 (size of the value term)

Outer dependencies: InterfaceOld, Specification, Specification.cartesianMonoidalCategory, Specification.category

Inner dependencies: InterfaceOld.Value, Specification.galoisConnection

Mathlib dependencies: CategoryTheory.Adjunction, CategoryTheory.Closed, CategoryTheory.Functor, CategoryTheory.Functor.ext, CategoryTheory.MonoidalCategory.tensorLeft, CategoryTheory.eqToHom, GaloisConnection.adjunction, GaloisConnection.monotone_l, GaloisConnection.monotone_u, Monotone.functor

Lean core dependencies: Eq, Eq.mpr, Eq.symm, Subsingleton.elim, congrArg, id, rfl

Used by: Specification.monoidalClosed

instance Specification.monoidalClosed {I : InterfaceOld} : CategoryTheory.MonoidalClosed (Specification I)
Show details 
| Specification.monoidalClosed = { closed := fun A => A.closed }

Complexity: 45 (size of the value term)

Outer dependencies: InterfaceOld, Specification, Specification.cartesianMonoidalCategory, Specification.category

Inner dependencies: Specification.closed

Mathlib dependencies: CategoryTheory.MonoidalClosed

Used by: (none)

Dependency diagram

Drag to pan, Ctrl+scroll (or Cmd+scroll, or pinch on a touch screen) to zoom, click a node to jump to it.

definitiontheoremdeclared elsewheredependencyproof dependency
legend