 572  rfl
 573
 574/-- The ambient real flow space on a finite node set. -/
 575abbrev FlowSpace (n : ℕ) := Fin n → Fin n → ℝ
 576
 577/-- Antisymmetry condition for ledger flows. -/
 578def IsAntisymmetricFlow {n : ℕ} (f : FlowSpace n) : Prop :=
 579  ∀ u v, f u v = -f v u
 580
 581/-- Node-wise conservation condition for ledger flows. -/
 582def IsConservedFlow {n : ℕ} (f : FlowSpace n) : Prop :=
 583  ∀ u, (Finset.univ.sum fun v => f u v) = 0
 584
 585/-- Objects in `LedgerAlg` are subspaces of admissible flows. -/
 586structure LedgerAlgObj (n : ℕ) where
 587  carrier : Submodule ℝ (FlowSpace n)
 588  antisymm : ∀ f : carrier, IsAntisymmetricFlow f.1
 589  conserved : ∀ f : carrier, IsConservedFlow f.1
 590
 591/-- Morphisms in `LedgerAlg` are linear maps between admissible-flow spaces. -/
 592structure LedgerAlgHom {n : ℕ} (A B : LedgerAlgObj n) where
 593  map : A.carrier →ₗ[ℝ] B.carrier
 594
 595/-- The full subspace of antisymmetric conserved flows. -/
 596def admissibleFlows (n : ℕ) : Submodule ℝ (FlowSpace n) where
 597  carrier := { f | IsAntisymmetricFlow f ∧ IsConservedFlow f }
 598  zero_mem' := by
 599    constructor
 600    · intro u v
 601      simp
 602    · intro u
 603      simp
 604  add_mem' := by
 605    intro f g hf hg

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.