PhiRingHom

formal source

 482
 483/-- Morphisms in the paper-facing `PhiRing` category preserve all ring
 484    structure and the distinguished golden element. -/
 485structure PhiRingHom (A B : PhiRingObj) where
 486  map : A.Carrier → B.Carrier
 487  map_zero : map A.zero = B.zero
 488  map_one : map A.one = B.one
 489  map_add : ∀ a b, map (A.add a b) = B.add (map a) (map b)
 490  map_neg : ∀ a, map (A.neg a) = B.neg (map a)
 491  map_mul : ∀ a b, map (A.mul a b) = B.mul (map a) (map b)
 492  map_phi : map A.phi = B.phi
 493
 494/-- Identity morphism in `PhiRing`. -/
 495def phiRing_id (A : PhiRingObj) : PhiRingHom A A where
 496  map := id
 497  map_zero := rfl
 498  map_one := rfl
 499  map_add := fun _ _ => rfl
 500  map_neg := fun _ => rfl
 501  map_mul := fun _ _ => rfl
 502  map_phi := rfl
 503
 504/-- Composition of `PhiRing` morphisms. -/
 505def phiRing_comp {A B C : PhiRingObj} (g : PhiRingHom B C) (f : PhiRingHom A B) :
 506    PhiRingHom A C where
 507  map := g.map ∘ f.map
 508  map_zero := by
 509    change g.map (f.map A.zero) = C.zero
 510    rw [f.map_zero]
 511    exact g.map_zero
 512  map_one := by
 513    change g.map (f.map A.one) = C.one
 514    rw [f.map_one]
 515    exact g.map_one