`OctaveAlgHom`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Algebra.RecognitionCategory on GitHub at line 678.

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

 675attribute [instance] OctaveAlgObj.instAddCommGroup OctaveAlgObj.instFintype
 676
 677/-- Morphisms in `OctaveAlg` are additive homomorphisms. -/
 678structure OctaveAlgHom (A B : OctaveAlgObj) where
 679  map : A.Carrier →+ B.Carrier
 680
 681/-- The canonical octave object represented by `ZMod 8`. -/
 682def canonicalOctaveAlgObj : OctaveAlgObj where
 683  Carrier := ZMod 8
 684  instAddCommGroup := inferInstance
 685  instFintype := inferInstance
 686  equivZModEight := AddEquiv.refl _
 687
 688/-- Identity morphism in `OctaveAlg`. -/
 689def octaveAlg_id (A : OctaveAlgObj) : OctaveAlgHom A A where
 690  map := AddMonoidHom.id A.Carrier
 691
 692/-- Composition in `OctaveAlg`. -/
 693def octaveAlg_comp {A B C : OctaveAlgObj}
 694    (g : OctaveAlgHom B C) (f : OctaveAlgHom A B) : OctaveAlgHom A C where
 695  map := g.map.comp f.map
 696
 697/-- Associativity of `OctaveAlg` composition on underlying maps. -/
 698theorem octaveAlg_comp_assoc {A B C D : OctaveAlgObj}
 699    (h : OctaveAlgHom C D) (g : OctaveAlgHom B C) (f : OctaveAlgHom A B) :
 700    (octaveAlg_comp h (octaveAlg_comp g f)).map = (octaveAlg_comp (octaveAlg_comp h g) f).map := by
 701  ext x
 702  rfl
 703
 704/-- Left identity law for `OctaveAlg` morphisms. -/
 705theorem octaveAlg_id_left {A B : OctaveAlgObj} (f : OctaveAlgHom A B) :
 706    (octaveAlg_comp (octaveAlg_id B) f).map = f.map := by
 707  ext x
 708  rfl

papers checked against this theorem

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