{"id":4970,"date":"2015-08-16T20:26:10","date_gmt":"2015-08-16T18:26:10","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=4970"},"modified":"2015-08-16T20:27:09","modified_gmt":"2015-08-16T18:27:09","slug":"resena-representations-of-finite-groups","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-representations-of-finite-groups\/","title":{"rendered":"Rese\u00f1a: Representations of finite groups"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en <a href=\"http:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle\">Isabelle\/HOL<\/a> sobre \u00e1lgebra titulado <a href=\"http:\/\/afp.sourceforge.net\/browser_info\/current\/AFP\/Rep_Fin_Groups\/document.pdf\">Representations of finite groups<\/a>.<\/p>\n<p>Su autor es <a href=\"http:\/\/www.ualberta.ca\/~jsylvest\">Jeremy Sylvestre<\/a> (de la Univ. de Alberta en Canad\u00e1).<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\n  We provide a formal framework for the theory of representations of finite groups, as modules over the group ring. Along the way, we develop the general theory of groups (relying on the group_add class for the basics), modules, and vector spaces, to the extent required for theory of group representations. We then provide formal proofs of several important introductory theorems in the subject, including Maschke&#8217;s theorem, Schur&#8217;s lemma, and Frobenius reciprocity. We also prove that every irreducible representation is isomorphic to a submodule of the group ring, leading to the fact that for a finite group there are only finitely many isomorphism classes of irreducible representations. In all of this, no restriction is made on the characteristic of the ring or field of scalars until the definition of a group representation, and then the only restriction made is that the characteristic must not divide the order of the group.\n<\/p><\/blockquote>\n<p>El trabajo se ha publicado el 12 de agosto en <a href=\"http:\/\/afp.sourceforge.net\/entries\/Rep_Fin_Groups.shtml\">AFP<\/a> (<em>The Archive of Formal Proofs<\/em>).<\/p>\n<p>El c\u00f3digo de las correspondientes teor\u00edas en Isabelle\/HOL se encuentra <a href=\"http:\/\/bit.ly\/1hGh4Z6\">aqu\u00ed<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Isabelle\/HOL sobre \u00e1lgebra titulado Representations of finite groups. Su autor es Jeremy Sylvestre (de la Univ. de Alberta en Canad\u00e1). Su resumen es We provide a formal framework for the theory of representations of finite groups, as modules over the group ring. Along the way, we&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[100],"tags":[144,285],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4970"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=4970"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4970\/revisions"}],"predecessor-version":[{"id":4972,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4970\/revisions\/4972"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=4970"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=4970"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=4970"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}