phiRing_comp_assoc

formal source

 553  phi_relation := PhiRing.phiInt_sq
 554
 555/-- Associativity of `PhiRing` composition on underlying maps. -/
 556theorem phiRing_comp_assoc {A B C D : PhiRingObj}
 557    (h : PhiRingHom C D) (g : PhiRingHom B C) (f : PhiRingHom A B) :
 558    (phiRing_comp h (phiRing_comp g f)).map = (phiRing_comp (phiRing_comp h g) f).map := by
 559  funext x
 560  rfl
 561
 562/-- Left identity law for `PhiRing` morphisms on underlying maps. -/
 563theorem phiRing_id_left {A B : PhiRingObj} (f : PhiRingHom A B) :
 564    (phiRing_comp (phiRing_id B) f).map = f.map := by
 565  funext x
 566  rfl
 567
 568/-- Right identity law for `PhiRing` morphisms on underlying maps. -/
 569theorem phiRing_id_right {A B : PhiRingObj} (f : PhiRingHom A B) :
 570    (phiRing_comp f (phiRing_id A)).map = f.map := by
 571  funext x
 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