TopologyDynamicsCategory

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

definition abbreviation lemma
legend
Topology.Coverage {Topo : Topology} (S : Set Topo.Block) : Type
Show details 
fun {Topo} 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'

Topology.joinCoverage {Topo : Topology} {S : Set Topo.Block} (b : Topo.Block) :
  CategoryTheory.Functor (Topology.Coverage S) (Topology.Coverage (insert b S))
Show details 
fun {Topo} {S} 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

Topology.leaveCoverage {Topo : Topology} {S : Set Topo.Block} (b : Topo.Block) :
  CategoryTheory.Functor (Topology.Coverage S) (Topology.Coverage (S \ {b}))
Show details 
fun {Topo} {S} 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

Topology.joinHistory {Topo : Topology} (S : Set Topo.Block) (b : Topo.Block) :
  Bool → CategoryTheory.Cat
Show details 
fun {Topo} S b x =>
  match x with
  | false => CategoryTheory.Cat.of (Topology.Coverage S)
  | 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

Topology.joinFunctor {Topo : Topology} (S : Set Topo.Block) (b : Topo.Block) :
  CategoryTheory.Functor Bool CategoryTheory.Cat
Show details 
fun {Topo} 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

Topology.joinGrothendieck {Topo : Topology} (S : Set Topo.Block) (b : Topo.Block) : Type
Show details 
fun {Topo} 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)

Topology.IsNerveCover {Topo : Topology} {S : Set Topo.Block} {T : Topology.Coverage S}
  (P : CategoryTheory.Presieve T) : Prop
Show details 
fun {Topo} {S} {T} 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

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 
fun {Topo} {S} {T} P Y ⦃Z⦄ 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

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

Topology.nerveCoverage (Topo : Topology) (S : Set Topo.Block) :
  CategoryTheory.Coverage (Topology.Coverage S)
Show details 
fun Topo 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

Topology.nerveTopology (Topo : Topology) (S : Set Topo.Block) :
  CategoryTheory.GrothendieckTopology (Topology.Coverage S)
Show details 
fun Topo 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)

Topology.Step.coverageFunctor {Topo : Topology} [Fintype Topo.Block] (st : Topo.membership.Step) :
  CategoryTheory.Functor (Topology.Coverage st.current) (Topology.Coverage st.next)
Show details 
fun {Topo} [Fintype Topo.Block] 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: Classical.propDecidable, 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'

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 
fun {Topo} [Fintype Topo.Block] x x_1 x_2 =>
  InformationSystem.Chain.brecOn x_2 Topology.runArrows'._f

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

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 
fun {Topo} [Fintype Topo.Block] {s s'} 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

Topology.runGrothendieck {Topo : Topology} [Fintype Topo.Block] (r : Topo.membership.Run) : Type
Show details 
fun {Topo} [Fintype Topo.Block] 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