LayerSysPlusHom

formal source

 726
 727/-- Morphisms in `LayerSys⁺` are tuples of morphisms in the four layer
 728    categories. -/
 729structure LayerSysPlusHom {n : ℕ} (A B : LayerSysPlusObj n) where
 730  costHom : RecAlgHom A.costLayer B.costLayer
 731  phiHom : PhiRingHom A.phiLayer B.phiLayer
 732  ledgerHom : LedgerAlgHom A.ledgerLayer B.ledgerLayer
 733  octaveHom : OctaveAlgHom A.octaveLayer B.octaveLayer
 734
 735/-- Identity morphism in `LayerSys⁺`. -/
 736def layerSysPlus_id {n : ℕ} (A : LayerSysPlusObj n) : LayerSysPlusHom A A where
 737  costHom := recAlg_id A.costLayer
 738  phiHom := phiRing_id A.phiLayer
 739  ledgerHom := ledgerAlg_id A.ledgerLayer
 740  octaveHom := octaveAlg_id A.octaveLayer
 741
 742/-- Composition in `LayerSys⁺`. -/
 743def layerSysPlus_comp {n : ℕ} {A B C : LayerSysPlusObj n}
 744    (g : LayerSysPlusHom B C) (f : LayerSysPlusHom A B) : LayerSysPlusHom A C where
 745  costHom := recAlg_comp g.costHom f.costHom
 746  phiHom := phiRing_comp g.phiHom f.phiHom
 747  ledgerHom := ledgerAlg_comp g.ledgerHom f.ledgerHom
 748  octaveHom := octaveAlg_comp g.octaveHom f.octaveHom
 749
 750/-- The canonical linked system built from the verified cost, `φ`, ledger, and
 751    octave layers. -/
 752noncomputable def canonicalLayerSysPlus (n : ℕ) : LayerSysPlusObj n where
 753  costLayer := canonicalCostAlgebra
 754  phiLayer := canonicalPhiRingObj
 755  ledgerLayer := canonicalLedgerAlgObj n
 756  octaveLayer := canonicalOctaveAlgObj
 757  bridge_cost_phi := by
 758    simpa [canonicalCostAlgebra] using PhiRing.J_at_phi
 759  bridge_phi_octave := OctaveAlgebra.modeToken_card