TopologyDynamicsCategory

Difficulty: optional — 12 definitions, 2 abbreviations, 1 lemmas, 0 theorems, 0 examples.

definition abbreviation lemma

legend

NoteTopology.Coverage

abbrev Topology.Coverage {Topo : Topology} (S : Set Topo.Block) : Type

Show details

| Topology.Coverage S = Set ↑S

Complexity: 17 (size of the value term)

Outer dependencies: Topology

Mathlib dependencies: Set, Set.Elem

Used by: Topology.IsNerveCover, Topology.Step.coverageFunctor, Topology.isNerveCover_inter, Topology.joinCoverage, Topology.joinFunctor, Topology.joinHistory, Topology.leaveCoverage, Topology.nerveCoverage, Topology.nerveTopology, Topology.restrictPresieve, Topology.runArrows, Topology.runArrows'

NoteTopology.joinCoverage

def Topology.joinCoverage {Topo : Topology} {S : Set Topo.Block} (b : Topo.Block) :
  CategoryTheory.Functor (Topology.Coverage S) (Topology.Coverage (insert b S))

Show details

| Topology.joinCoverage b = Monotone.functor ⋯

Complexity: 427 (size of the value term)

Outer dependencies: Topology, Topology.Coverage

Mathlib dependencies: CategoryTheory.Functor, Monotone.functor, Set, Set.Elem, Set.image, Set.image_mono, Set.mem_insert_of_mem

Used by: Topology.Step.coverageFunctor, Topology.joinFunctor

NoteTopology.leaveCoverage

def Topology.leaveCoverage {Topo : Topology} {S : Set Topo.Block} (b : Topo.Block) :
  CategoryTheory.Functor (Topology.Coverage S) (Topology.Coverage (S \ {b}))

Show details

| Topology.leaveCoverage b = Monotone.functor ⋯

Complexity: 633 (size of the value term)

Outer dependencies: Topology, Topology.Coverage

Mathlib dependencies: CategoryTheory.Functor, Monotone.functor, Set, Set.Elem, setOf

Lean core dependencies: Not, Subtype

Used by: Topology.Step.coverageFunctor

NoteTopology.joinHistory

def Topology.joinHistory {Topo : Topology} (S : Set Topo.Block) (b : Topo.Block) :
  Bool → CategoryTheory.Cat

Show details

| Topology.joinHistory S b false = CategoryTheory.Cat.of (Topology.Coverage S)
| Topology.joinHistory S b true = CategoryTheory.Cat.of (Topology.Coverage (insert b S))

Complexity: 317 (size of the value term)

Outer dependencies: Topology

Inner dependencies: Topology.Coverage

Mathlib dependencies: CategoryTheory.Cat, CategoryTheory.Cat.of, Set, Set.Elem

Lean core dependencies: Bool, Unit, Unit.unit

Used by: Topology.joinFunctor

NoteTopology.joinFunctor

def Topology.joinFunctor {Topo : Topology} (S : Set Topo.Block) (b : Topo.Block) :
  CategoryTheory.Functor Bool CategoryTheory.Cat

Show details

| Topology.joinFunctor S b =
  { obj := Topology.joinHistory S b,
    map := fun {x y} h =>
      Bool.casesOn (motive := fun x =>
        (x ⟶ y) → (Topology.joinHistory S b x ⟶ Topology.joinHistory S b y)) x
        (fun h =>
          Bool.casesOn (motive := fun x =>
            (false ⟶ x) → (Topology.joinHistory S b false ⟶ Topology.joinHistory S b x)) y
            (fun h => (CategoryTheory.Functor.id (Topology.Coverage S)).toCatHom)
            (fun h => (Topology.joinCoverage b).toCatHom) h)
        (fun h =>
          Bool.casesOn (motive := fun x =>
            (true ⟶ x) → (Topology.joinHistory S b true ⟶ Topology.joinHistory S b x)) y
            (fun h => absurd ⋯ Topology.joinFunctor._proof_2)
            (fun h => (CategoryTheory.Functor.id (Topology.Coverage (insert b S))).toCatHom) h)
        h,
    map_id := ⋯, map_comp := ⋯ }

Complexity: 1673 (size of the value term)

Outer dependencies: Topology

Inner dependencies: Topology.Coverage, Topology.joinCoverage, Topology.joinHistory

Mathlib dependencies: CategoryTheory.Cat, CategoryTheory.Functor, CategoryTheory.Functor.id, CategoryTheory.Functor.toCatHom, CategoryTheory.leOfHom, Set, Set.Elem

Lean core dependencies: Bool, Decidable.decide, Eq, Eq.symm, Not, absurd, id, of_decide_eq_true

Used by: Topology.joinGrothendieck

NoteTopology.joinGrothendieck

abbrev Topology.joinGrothendieck {Topo : Topology} (S : Set Topo.Block) (b : Topo.Block) : Type

Show details

| Topology.joinGrothendieck S b = CategoryTheory.Grothendieck (Topology.joinFunctor S b)

Complexity: 33 (size of the value term)

Outer dependencies: Topology

Inner dependencies: Topology.joinFunctor

Mathlib dependencies: CategoryTheory.Grothendieck, Set

Lean core dependencies: Bool

Used by: (none)

NoteTopology.IsNerveCover

def Topology.IsNerveCover {Topo : Topology} {S : Set Topo.Block} {T : Topology.Coverage S}
  (P : CategoryTheory.Presieve T) : Prop

Show details

| Topology.IsNerveCover P =
  (⋃ Y ∈ {Y | ∃ (h : Y ⊆ T), P (CategoryTheory.homOfLE h)}, Y = T ∧
    ∀ (x y : ↑S),
      (SimpleGraph.induce S Topo.external).Adj x y →
        x ∈ T → y ∈ T → ∃ Y ∈ {Y | ∃ (h : Y ⊆ T), P (CategoryTheory.homOfLE h)}, x ∈ Y ∧ y ∈ Y)

Complexity: 773 (size of the value term)

Outer dependencies: Topology, Topology.Coverage

Mathlib dependencies: CategoryTheory.Presieve, CategoryTheory.homOfLE, Set, Set.Elem, Set.iUnion, SimpleGraph.induce, setOf

Lean core dependencies: And, Eq, Exists

Used by: Topology.isNerveCover_inter, Topology.nerveCoverage

NoteTopology.restrictPresieve

def Topology.restrictPresieve {Topo : Topology} {S : Set Topo.Block} {T : Topology.Coverage S}
  (P : CategoryTheory.Presieve T) (Y : Topology.Coverage S) : CategoryTheory.Presieve Y

Show details

| Topology.restrictPresieve P Y x✝ = ∃ W, (∃ (h : W ⊆ T), P (CategoryTheory.homOfLE h)) ∧ Z = W ∩ Y

Complexity: 341 (size of the value term)

Outer dependencies: Topology, Topology.Coverage

Mathlib dependencies: CategoryTheory.Presieve, CategoryTheory.homOfLE, Set, Set.Elem

Lean core dependencies: And, Eq, Exists

Used by: Topology.isNerveCover_inter, Topology.nerveCoverage

TipTopology.isNerveCover_inter

theorem Topology.isNerveCover_inter {Topo : Topology} {S : Set Topo.Block} {T : Topology.Coverage S}
  {P : CategoryTheory.Presieve T} (hP : Topology.IsNerveCover P) (Y : Topology.Coverage S)
  (f : Y ⟶ T) : Topology.IsNerveCover (Topology.restrictPresieve P Y)

Show details

fun {Topo} {S} {T} {P} hP Y f =>
  And.casesOn hP fun hunion hnerve =>
    have hYT := CategoryTheory.leOfHom f;
    id
      (id
        ⟨subset_antisymm
            (Eq.mpr
              (id
                (Eq.trans Topology.isNerveCover_inter._simp_1_1
                  (forall_congr fun i => Topology.isNerveCover_inter._simp_1_1)))
              fun Z i =>
              Exists.casesOn i fun w h =>
                Exists.casesOn h fun W h =>
                  And.casesOn h fun left right =>
                    Eq.ndrec (motive := fun Z => Z ⊆ Y → Z ⊆ Y) (fun w => Set.inter_subset_right)
                      (Eq.symm right) w)
            fun ⦃x⦄ hx =>
            have hxT := hYT hx;
            Exists.casesOn
              (Eq.mp
                (Eq.trans Topology.isNerveCover_inter._simp_1_2
                  (congrArg Exists (funext fun i => Topology.isNerveCover_inter._simp_1_2)))
                (Eq.mp (congrArg (fun _a => x ∈ _a) (Eq.symm hunion)) hxT))
              fun W h =>
              Exists.casesOn h fun w hxW =>
                Exists.casesOn w fun h hPW =>
                  Eq.mpr
                    (id
                      (Eq.trans Topology.isNerveCover_inter._simp_1_2
                        (congrArg Exists (funext fun i => Topology.isNerveCover_inter._simp_1_2))))
                    (Exists.intro (W ∩ Y)
                      (Exists.intro
                        (Exists.intro Set.inter_subset_right
                          (Exists.intro W ⟨Exists.intro h hPW, rfl⟩))
                        ⟨hxW, hx⟩)),
          fun x y hadj hx hy =>
          have hxT := hYT hx;
          have hyT := hYT hy;
          Exists.casesOn (hnerve x y hadj hxT hyT) fun W h =>
            And.casesOn h fun left right =>
              Exists.casesOn left fun h hPW =>
                And.casesOn right fun hxW hyW =>
                  Exists.intro (W ∩ Y)
                    ⟨Exists.intro Set.inter_subset_right (Exists.intro W ⟨Exists.intro h hPW, rfl⟩),
                      ⟨⟨hxW, hx⟩, ⟨hyW, hy⟩⟩⟩⟩)

Complexity: 31749 (size of the value term)

Dependencies: Topology, Topology.Coverage, Topology.IsNerveCover, Topology.restrictPresieve

Mathlib dependencies: CategoryTheory.Presieve, CategoryTheory.homOfLE, CategoryTheory.leOfHom, Set, Set.Elem, Set.iUnion, Set.iUnion_subset_iff, Set.inter_subset_right, Set.mem_iUnion, SimpleGraph.induce, setOf, subset_antisymm

Lean core dependencies: And, Eq, Eq.mp, Eq.mpr, Eq.symm, Eq.trans, Exists, congrArg, forall_congr, funext, id, rfl

Used by: Topology.nerveCoverage

NoteTopology.nerveCoverage

def Topology.nerveCoverage (Topo : Topology) (S : Set Topo.Block) :
  CategoryTheory.Coverage (Topology.Coverage S)

Show details

| Topo.nerveCoverage S = { coverings := fun _T => {P | Topology.IsNerveCover P}, pullback := ⋯ }

Complexity: 299 (size of the value term)

Outer dependencies: Topology, Topology.Coverage

Inner dependencies: Topology.IsNerveCover, Topology.isNerveCover_inter, Topology.restrictPresieve

Mathlib dependencies: CategoryTheory.Coverage, CategoryTheory.Presieve, CategoryTheory.Presieve.FactorsThruAlong, CategoryTheory.homOfLE, Set, Set.Elem, Set.inter_subset_left, setOf

Lean core dependencies: And, Eq, Eq.symm, Exists, Subsingleton.elim

Used by: Topology.nerveTopology

NoteTopology.nerveTopology

def Topology.nerveTopology (Topo : Topology) (S : Set Topo.Block) :
  CategoryTheory.GrothendieckTopology (Topology.Coverage S)

Show details

| Topo.nerveTopology S = (Topo.nerveCoverage S).toGrothendieck

Complexity: 79 (size of the value term)

Outer dependencies: Topology, Topology.Coverage

Inner dependencies: Topology.nerveCoverage

Mathlib dependencies: CategoryTheory.Coverage.toGrothendieck, CategoryTheory.GrothendieckTopology, Set, Set.Elem

Used by: (none)

NoteTopology.Step.coverageFunctor

def Topology.Step.coverageFunctor {Topo : Topology} [Fintype Topo.Block] (st : Topo.membership.Step) :
  CategoryTheory.Functor (Topology.Coverage st.current) (Topology.Coverage st.next)

Show details

| Topology.Step.coverageFunctor st =
  match h : st.input with
  | Topology.Event.idle =>
    have heq := ⋯;
    heq ▸ CategoryTheory.Functor.id (Topology.Coverage st.next)
  | Topology.Event.join b =>
    if hb : b ∈ st.current then
      have heq := ⋯;
      heq ▸ CategoryTheory.Functor.id (Topology.Coverage st.next)
    else
      have heq := ⋯;
      ⋯ ▸ Topology.joinCoverage b
  | Topology.Event.leave b =>
    if hb : b ∈ st.current then
      have heq := ⋯;
      ⋯ ▸ Topology.leaveCoverage b
    else
      have heq := ⋯;
      heq ▸ CategoryTheory.Functor.id (Topology.Coverage st.next)

Complexity: 8050 (size of the value term)

Outer dependencies: InformationSystem.Step, Topology, Topology.Coverage, Topology.Event, Topology.Signal, Topology.membership, instNonemptyEvent, instNonemptySignal, instNormEvent, instNormSetBlock, instNormSignal

Inner dependencies: Topology.joinCoverage, Topology.leaveCoverage, Topology.step, Topology.step_conserves

Mathlib dependencies: CategoryTheory.Functor, CategoryTheory.Functor.id, Fintype, Set, Set.Elem

Lean core dependencies: Eq, Eq.mp, Eq.symm, Not, Prod, congrArg, dite, eq_false, eq_true, id, ite_cond_eq_false, ite_cond_eq_true

Used by: Topology.runArrows'

NoteTopology.runArrows'

def Topology.runArrows' {Topo : Topology} [Fintype Topo.Block] {s s' : Set Topo.Block}
  (c : Topo.membership.Chain s s') :
  (F : CategoryTheory.ComposableArrows CategoryTheory.Cat c.length) ×'
    F.left = CategoryTheory.Cat.of (Topology.Coverage s)

Show details

| Topology.runArrows' (InformationSystem.Chain.nil x✝) =
  ⟨CategoryTheory.ComposableArrows.mk₀ (CategoryTheory.Cat.of (Topology.Coverage x✝)), ⋯⟩
| Topology.runArrows' (InformationSystem.Chain.cons st rest) =
  match Topology.runArrows' rest with
  | ⟨F, hF⟩ => ⟨F.precomp (⋯ ▸ (Topology.Step.coverageFunctor st).toCatHom), ⋯⟩

Complexity: 401 (size of the value term)

Outer dependencies: InformationSystem.Chain, InformationSystem.Chain.length, Topology, Topology.Coverage, Topology.Event, Topology.Signal, Topology.membership, instNonemptyEvent, instNonemptySignal, instNormEvent, instNormSetBlock, instNormSignal

Inner dependencies: InformationSystem.Step, Topology.Step.coverageFunctor

Mathlib dependencies: CategoryTheory.Cat, CategoryTheory.Cat.of, CategoryTheory.ComposableArrows, CategoryTheory.ComposableArrows.left, CategoryTheory.ComposableArrows.mk₀, CategoryTheory.ComposableArrows.precomp, CategoryTheory.Functor.toCatHom, Fintype, Set, Set.Elem

Lean core dependencies: Eq, Eq.symm, HEq, PSigma, eq_of_heq, rfl

Used by: Topology.runArrows

NoteTopology.runArrows

def Topology.runArrows {Topo : Topology} [Fintype Topo.Block] {s s' : Set Topo.Block}
  (c : Topo.membership.Chain s s') : CategoryTheory.ComposableArrows CategoryTheory.Cat c.length

Show details

| Topology.runArrows c = (Topology.runArrows' c).fst

Complexity: 305 (size of the value term)

Outer dependencies: InformationSystem.Chain, InformationSystem.Chain.length, Topology, Topology.Event, Topology.Signal, Topology.membership, instNonemptyEvent, instNonemptySignal, instNormEvent, instNormSetBlock, instNormSignal

Inner dependencies: Topology.Coverage, Topology.runArrows'

Mathlib dependencies: CategoryTheory.Cat, CategoryTheory.Cat.of, CategoryTheory.ComposableArrows, CategoryTheory.ComposableArrows.left, Fintype, Set, Set.Elem

Lean core dependencies: Eq

Used by: Topology.runGrothendieck

NoteTopology.runGrothendieck

def Topology.runGrothendieck {Topo : Topology} [Fintype Topo.Block] (r : Topo.membership.Run) : Type

Show details

| Topology.runGrothendieck r = CategoryTheory.Grothendieck (Topology.runArrows r.toChain)

Complexity: 953 (size of the value term)

Outer dependencies: InformationSystem.Run, Topology, Topology.Event, Topology.Signal, Topology.membership, instNonemptyEvent, instNonemptySignal, instNormEvent, instNormSetBlock, instNormSignal

Inner dependencies: InformationSystem.Chain.length, InformationSystem.Run.final, InformationSystem.Run.initial, InformationSystem.Run.toChain, Topology.runArrows

Mathlib dependencies: CategoryTheory.Grothendieck, Fintype, Set

Lean core dependencies: Fin, Nat

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.

definitionabbreviationlemmadeclared elsewheredependencyproof dependency

legend