`phiRing_comp`

definition

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Algebra.RecognitionCategory on GitHub at line 505.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

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.