`phiRing_comp`

definition

show as: view math explainer →

module: IndisputableMonolith.Algebra.RecognitionCategory
domain: Algebra
line: 505 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Algebra.RecognitionCategory on GitHub at line 505.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 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
 516  map_add := by
 517    intro a b
 518    simp [Function.comp, f.map_add, g.map_add]
 519  map_neg := by
 520    intro a
 521    simp [Function.comp, f.map_neg, g.map_neg]
 522  map_mul := by
 523    intro a b
 524    simp [Function.comp, f.map_mul, g.map_mul]
 525  map_phi := by
 526    change g.map (f.map A.phi) = C.phi
 527    rw [f.map_phi]
 528    exact g.map_phi
 529
 530/-- The canonical object of the `PhiRing` category is `ℤ[φ]`. -/
 531def canonicalPhiRingObj : PhiRingObj where
 532  Carrier := PhiRing.PhiInt
 533  zero := PhiRing.PhiInt.zero
 534  one := PhiRing.PhiInt.one
 535  add := PhiRing.PhiInt.add

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.