phiRing_id_left

formal source

 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
 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