`OctaveAlgObj`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Algebra.RecognitionCategory on GitHub at line 669.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

used by

formal source

 666  rfl
 667
 668/-- Objects in `OctaveAlg` are additive groups explicitly equivalent to `ZMod 8`. -/
 669structure OctaveAlgObj where
 670  Carrier : Type u
 671  instAddCommGroup : AddCommGroup Carrier
 672  instFintype : Fintype Carrier
 673  equivZModEight : Carrier ≃+ ZMod 8
 674
 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) :

papers checked against this theorem

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