LedgerAlgHom

formal source

 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
 606    rcases hf with ⟨hfA, hfC⟩
 607    rcases hg with ⟨hgA, hgC⟩
 608    constructor
 609    · intro u v
 610      change f u v + g u v = -(f v u + g v u)
 611      rw [hfA u v, hgA u v]
 612      ring
 613    · intro u
 614      change (∑ v, (f u v + g u v)) = 0
 615      rw [Finset.sum_add_distrib, hfC u, hgC u]
 616      norm_num
 617  smul_mem' := by
 618    intro c f hf
 619    rcases hf with ⟨hfA, hfC⟩
 620    constructor
 621    · intro u v
 622      change c * f u v = -(c * f v u)