<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<link href="coqdoc.css" rel="stylesheet" type="text/css" />
<title>mathcomp.solvable.gfunctor</title>
</head>

<body>

<div id="page">

<div id="header">
</div>

<div id="main">

<h1 class="libtitle">Library mathcomp.solvable.gfunctor</h1>

<div class="code">
<span class="comment">(*&nbsp;(c)&nbsp;Copyright&nbsp;2006-2016&nbsp;Microsoft&nbsp;Corporation&nbsp;and&nbsp;Inria.&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<br/>
&nbsp;Distributed&nbsp;under&nbsp;the&nbsp;terms&nbsp;of&nbsp;CeCILL-B.&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;*)</span><br/>
<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#"><span class="id" title="library">mathcomp.ssreflect.ssreflect</span></a>.<br/>

<br/>
</div>

<div class="doc">
   This file provides basic interfaces for the notion of "generic"          
 characteristic subgroups; these amount to subfunctors of the identity      
 functor in some category of groups.                                        
 See "Generic Proof Tools And Finite Group Theory",                         
 Francois Garillot, PhD, 2011, Chapter 3.                                   
 The implementation proposed here is fairly basic, relying on first order   
 function matching and on structure telescopes, both of which are somewhat  
 limited and fragile. It should switch in the future to more general and    
 more robust quotation matching.                                            
   The definitions in this file (types, properties and structures) are all  
 packaged under the GFunctor submodule, i.e., client code should refer to   
 GFunctor.continuous, GFunctor.map, etc. Notations, Coercions and Lemmas    
 are exported and thus directly available, however.                         
   We provide the following:                                                
      object_map == the type of the (polymorphic) object map of a group     
                    functor; the %gF scope is bound to object_map.          
                 := forall gT : finGroupType, {set gT} -&gt; {set gT}.         
  We define two operations on object_map (with notations in the %gF scope): 
        F1 \o F2 == the composite map; (F1 \o F2) G expands to F1 (F2 G).   
        F1 %% F2 == F1 computed modulo F2; we have                          
                    (F1 %% F2) G / F2 G = F1 (G / F2 G)                     
 We define the following (type-polymorphic) properties of an object_map F:  
     group_valued F &lt;-&gt; F G is a group when G is a group                    
           closed F &lt;-&gt; F G is a subgroup o fG when G is a group            
       continuous F &lt;-&gt; F is continuous with respect to morphism image:     
                        for any f : {morphism G &gt;-&gt; ..}, f @* (F G) is a    
                        a subgroup of F (f @* G); equivalently, F is        
                        functorial in the category Grp of groups.           
                        Most common "characteristic subgroup" are produced  
                        continuous object maps.                             
   iso_continuous F &lt;-&gt; F is continuous with respect to isomorphism image;  
                        equivalently, F is functorial in the Grp groupoid.  
                        The Puig and the Thompson J subgroups are examples  
                        of iso_continuous maps that are not continuous.     
      pcontinuous F &lt;-&gt; F is continuous with respect to partial morphism    
                        image, i.e., functorial in the category of groups   
                        and partial morphisms. The center and p-core are    
                        examples of pcontinuous maps.                       
       hereditary F &lt;-&gt; inclusion in the image of F is hereditary, i.e.,    
                        for any subgroup H of G, the intersection of H with 
                        F G is included in H. Note that F is pcontinuous    
                        iff it is continuous and hereditary; indeed proofs  
                        of pcontinuous F coerce to proofs of hereditary F   
                        and continuous F.                                   
        monotonic F &lt;-&gt; F is monotonic with respect to inclusion: for any   
                        subgroup H of G, F H is a subgroup of F G. The      
                        derived and lower central series are examples of    
                        monotonic maps.                                     
 Four structures provide interfaces to these properties:                    
    GFunctor.iso_map == structure for object maps that are group_valued,    
                        closed, and iso_continuous.                         
  [igFun by Fsub &amp; !Fcont] == the iso_map structure for an object map F     
                        such that F G is canonically a group when G is, and 
                        given Fsub : closed F and Fcont : iso_continuous F. 
  [igFun by Fsub &amp; Fcont] == as above, but expecting Fcont : continuous F.  
        [igFun of F] == clone an existing GFunctor.iso_map structure for F. 
        GFunctor.map == structure for continuous object maps, inheriting    
                        from the GFunctor.iso_map structure.                
     [gFun by Fcont] == the map structure for an F with a canonical iso_map 
                        structure, given Fcont : continuous F.              
         [gFun of F] == clone an existing GFunctor.map structure for F.     
       GFunctor.pmap == structure for pcontinuous object maps, inheriting   
                        from the GFunctor.map structure.                    
    [pgFun by Fher] == the pmap structure for an F with a canonical map     
                        structure, given Fher : hereditary F.               
        [pgFun of F] == clone an existing GFunctor.pmap structure for F.    
   GFunctor.mono_map == structure for monotonic, continuous object maps     
                        inheriting from the GFunctor.map structure.         
     [mgFun by Fmon] == the mono_map structure for an F with a canonical    
                        map structure, given Fmon : monotonic F.            
        [mgFun of F] == clone an existing GFunctor.mono_map structure for F 
 Lemmas for these group functors use either a 'gF' prefix or an 'F' suffix. 
 The (F1 \o F2) and (F1 %% F2) operations have canonical GFunctor.map       
 structures when F1 is monotonic or hereditary, respectively.                
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Import</span> <span class="id" title="var">GroupScope</span>.<br/>

<br/>
<span class="id" title="keyword">Set Implicit Arguments</span>.<br/>

<br/>
<span class="id" title="keyword">Delimit</span> <span class="id" title="keyword">Scope</span> <span class="id" title="var">gFun_scope</span> <span class="id" title="keyword">with</span> <span class="id" title="var">gF</span>.<br/>

<br/>
<span class="id" title="keyword">Module</span> <a name="GFunctor"><span class="id" title="module">GFunctor</span></a>.<br/>

<br/>
<span class="id" title="keyword">Definition</span> <a name="GFunctor.object_map"><span class="id" title="definition">object_map</span></a> := <span class="id" title="keyword">∀</span> <span class="id" title="var">gT</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>, <a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">}</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">}</span></a>.<br/>

<br/>

<br/>
<span class="id" title="keyword">Section</span> <a name="GFunctor.Definitions"><span class="id" title="section">Definitions</span></a>.<br/>

<br/>
<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> <span class="id" title="var">gT</span> <span class="id" title="var">hT</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>.<br/>

<br/>
<span class="id" title="keyword">Variable</span> <a name="GFunctor.Definitions.F"><span class="id" title="variable">F</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.object_map"><span class="id" title="definition">object_map</span></a>.<br/>

<br/>
</div>

<div class="doc">
 Group closure.  
</div>
<div class="code">
<span class="id" title="keyword">Definition</span> <a name="GFunctor.group_valued"><span class="id" title="definition">group_valued</span></a> := <span class="id" title="keyword">∀</span> <span class="id" title="var">gT</span> (<span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>), <a class="idref" href="mathcomp.fingroup.fingroup.html#group_set"><span class="id" title="definition">group_set</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Definitions.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a>).<br/>

<br/>
</div>

<div class="doc">
 Subgroup closure.  
</div>
<div class="code">
<span class="id" title="keyword">Definition</span> <a name="GFunctor.closed"><span class="id" title="definition">closed</span></a> := <span class="id" title="keyword">∀</span> <span class="id" title="var">gT</span> (<span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>), <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Definitions.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a>.<br/>

<br/>
</div>

<div class="doc">
 General functoriality, i.e., continuity of the object map  
</div>
<div class="code">
<span class="id" title="keyword">Definition</span> <a name="GFunctor.continuous"><span class="id" title="definition">continuous</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">∀</span> <span class="id" title="var">gT</span> <span class="id" title="var">hT</span> (<span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">phi</span> : <a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">morphism</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">&gt;-&gt;</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#hT"><span class="id" title="variable">hT</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">}</span></a>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.solvable.gfunctor.html#phi"><span class="id" title="variable">phi</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Definitions.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Definitions.F"><span class="id" title="variable">F</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#phi"><span class="id" title="variable">phi</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a>).<br/>

<br/>
</div>

<div class="doc">
 Functoriality on the Grp groupoid (arrows are restricted to isos).  
</div>
<div class="code">
<span class="id" title="keyword">Definition</span> <a name="GFunctor.iso_continuous"><span class="id" title="definition">iso_continuous</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">∀</span> <span class="id" title="var">gT</span> <span class="id" title="var">hT</span> (<span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">phi</span> : <a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">morphism</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">&gt;-&gt;</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#hT"><span class="id" title="variable">hT</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">}</span></a>),<br/>
&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.fingroup.morphism.html#14bfb149f00fa839cfb11397f4fe629f"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#14bfb149f00fa839cfb11397f4fe629f"><span class="id" title="notation">injm</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#phi"><span class="id" title="variable">phi</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#phi"><span class="id" title="variable">phi</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Definitions.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Definitions.F"><span class="id" title="variable">F</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#phi"><span class="id" title="variable">phi</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a>).<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="GFunctor.continuous_is_iso_continuous"><span class="id" title="lemma">continuous_is_iso_continuous</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.continuous"><span class="id" title="definition">continuous</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.iso_continuous"><span class="id" title="definition">iso_continuous</span></a>.<br/>
 
<br/>
</div>

<div class="doc">
 Functoriality on Grp with partial morphisms.  
</div>
<div class="code">
<span class="id" title="keyword">Definition</span> <a name="GFunctor.pcontinuous"><span class="id" title="definition">pcontinuous</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">∀</span> <span class="id" title="var">gT</span> <span class="id" title="var">hT</span> (<span class="id" title="var">G</span> <span class="id" title="var">D</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">phi</span> : <a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">morphism</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">&gt;-&gt;</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#hT"><span class="id" title="variable">hT</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">}</span></a>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.solvable.gfunctor.html#phi"><span class="id" title="variable">phi</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Definitions.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Definitions.F"><span class="id" title="variable">F</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#phi"><span class="id" title="variable">phi</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a>).<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="GFunctor.pcontinuous_is_continuous"><span class="id" title="lemma">pcontinuous_is_continuous</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.pcontinuous"><span class="id" title="definition">pcontinuous</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.continuous"><span class="id" title="definition">continuous</span></a>.<br/>
 
<br/>
</div>

<div class="doc">
 Heredity with respect to inclusion  
</div>
<div class="code">
<span class="id" title="keyword">Definition</span> <a name="GFunctor.hereditary"><span class="id" title="definition">hereditary</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">∀</span> <span class="id" title="var">gT</span> (<span class="id" title="var">H</span> <span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>), <a class="idref" href="mathcomp.solvable.gfunctor.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Definitions.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#cb41714a5a23482f7a48a98975fa8c59"><span class="id" title="notation">:&amp;:</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Definitions.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#H"><span class="id" title="variable">H</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="GFunctor.pcontinuous_is_hereditary"><span class="id" title="lemma">pcontinuous_is_hereditary</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.pcontinuous"><span class="id" title="definition">pcontinuous</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.hereditary"><span class="id" title="definition">hereditary</span></a>.<br/>

<br/>
</div>

<div class="doc">
 Monotonicity with respect to inclusion  
</div>
<div class="code">
<span class="id" title="keyword">Definition</span> <a name="GFunctor.monotonic"><span class="id" title="definition">monotonic</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">∀</span> <span class="id" title="var">gT</span> (<span class="id" title="var">H</span> <span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>), <a class="idref" href="mathcomp.solvable.gfunctor.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Definitions.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Definitions.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a>.<br/>

<br/>
</div>

<div class="doc">
 Self-expanding composition, and modulo  
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Variables</span> (<a name="GFunctor.Definitions.k"><span class="id" title="variable">k</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#unit"><span class="id" title="inductive">unit</span></a>) (<a name="GFunctor.Definitions.F1"><span class="id" title="variable">F1</span></a> <a name="GFunctor.Definitions.F2"><span class="id" title="variable">F2</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.object_map"><span class="id" title="definition">object_map</span></a>).<br/>

<br/>
<span class="id" title="keyword">Definition</span> <a name="GFunctor.comp_head"><span class="id" title="definition">comp_head</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.object_map"><span class="id" title="definition">object_map</span></a> := <span class="id" title="keyword">fun</span> <span class="id" title="var">gT</span> <span class="id" title="var">A</span> ⇒ <span class="id" title="keyword">let</span>: <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#tt"><span class="id" title="constructor">tt</span></a> := <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Definitions.k"><span class="id" title="variable">k</span></a> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Definitions.F1"><span class="id" title="variable">F1</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Definitions.F2"><span class="id" title="variable">F2</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#A"><span class="id" title="variable">A</span></a>).<br/>

<br/>
<span class="id" title="keyword">Definition</span> <a name="GFunctor.modulo"><span class="id" title="definition">modulo</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.object_map"><span class="id" title="definition">object_map</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">fun</span> <span class="id" title="var">gT</span> <span class="id" title="var">A</span> ⇒ <a class="idref" href="mathcomp.fingroup.quotient.html#coset"><span class="id" title="definition">coset</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Definitions.F2"><span class="id" title="variable">F2</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#A"><span class="id" title="variable">A</span></a>) <a class="idref" href="mathcomp.fingroup.morphism.html#619a2190d60a66179f3396458e2a09ae"><span class="id" title="notation">@*^-1</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#619a2190d60a66179f3396458e2a09ae"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Definitions.F1"><span class="id" title="variable">F1</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.fingroup.quotient.html#c7768147d2d560601601fbf95706ddcc"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.fingroup.quotient.html#c7768147d2d560601601fbf95706ddcc"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Definitions.F2"><span class="id" title="variable">F2</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.quotient.html#c7768147d2d560601601fbf95706ddcc"><span class="id" title="notation">)</span></a>)<a class="idref" href="mathcomp.fingroup.morphism.html#619a2190d60a66179f3396458e2a09ae"><span class="id" title="notation">)</span></a>.<br/>

<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Definitions"><span class="id" title="section">Definitions</span></a>.<br/>

<br/>
<span class="id" title="keyword">Section</span> <a name="GFunctor.ClassDefinitions"><span class="id" title="section">ClassDefinitions</span></a>.<br/>

<br/>
<span class="id" title="keyword">Structure</span> <a name="GFunctor.iso_map"><span class="id" title="record">iso_map</span></a> := <a name="GFunctor.IsoMap"><span class="id" title="constructor">IsoMap</span></a> {<br/>
&nbsp;&nbsp;<a name="GFunctor.apply"><span class="id" title="projection">apply</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.object_map"><span class="id" title="definition">object_map</span></a>;<br/>
&nbsp;&nbsp;<span class="id" title="var">_</span> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.group_valued"><span class="id" title="definition">group_valued</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#apply"><span class="id" title="method">apply</span></a>;<br/>
&nbsp;&nbsp;<span class="id" title="var">_</span> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.closed"><span class="id" title="definition">closed</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#apply"><span class="id" title="method">apply</span></a>;<br/>
&nbsp;&nbsp;<span class="id" title="var">_</span> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.iso_continuous"><span class="id" title="definition">iso_continuous</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#apply"><span class="id" title="method">apply</span></a><br/>
}.<br/>

<br/>
<span class="id" title="keyword">Structure</span> <a name="GFunctor.map"><span class="id" title="record">map</span></a> := <a name="GFunctor.Map"><span class="id" title="constructor">Map</span></a> { <a name="GFunctor.iso_of_map"><span class="id" title="projection">iso_of_map</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.iso_map"><span class="id" title="record">iso_map</span></a>; <span class="id" title="var">_</span> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.continuous"><span class="id" title="definition">continuous</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#iso_of_map"><span class="id" title="method">iso_of_map</span></a> }.<br/>

<br/>
<span class="id" title="keyword">Structure</span> <a name="GFunctor.pmap"><span class="id" title="record">pmap</span></a> := <a name="GFunctor.Pmap"><span class="id" title="constructor">Pmap</span></a> { <a name="GFunctor.map_of_pmap"><span class="id" title="projection">map_of_pmap</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.map"><span class="id" title="record">map</span></a>; <span class="id" title="var">_</span> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.hereditary"><span class="id" title="definition">hereditary</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#map_of_pmap"><span class="id" title="method">map_of_pmap</span></a> }.<br/>

<br/>
<span class="id" title="keyword">Structure</span> <a name="GFunctor.mono_map"><span class="id" title="record">mono_map</span></a> := <a name="GFunctor.MonoMap"><span class="id" title="constructor">MonoMap</span></a> { <a name="GFunctor.map_of_mono"><span class="id" title="projection">map_of_mono</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.map"><span class="id" title="record">map</span></a>; <span class="id" title="var">_</span> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.monotonic"><span class="id" title="definition">monotonic</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#map_of_mono"><span class="id" title="method">map_of_mono</span></a> }.<br/>

<br/>
<span class="id" title="keyword">Definition</span> <a name="GFunctor.pack_iso"><span class="id" title="definition">pack_iso</span></a> <span class="id" title="var">F</span> <span class="id" title="var">Fcont</span> <span class="id" title="var">Fgrp</span> <span class="id" title="var">Fsub</span> := @<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.IsoMap"><span class="id" title="constructor">IsoMap</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#Fgrp"><span class="id" title="variable">Fgrp</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#Fsub"><span class="id" title="variable">Fsub</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#Fcont"><span class="id" title="variable">Fcont</span></a>.<br/>

<br/>
<span class="id" title="keyword">Definition</span> <a name="GFunctor.clone_iso"><span class="id" title="definition">clone_iso</span></a> (<span class="id" title="var">F</span> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.object_map"><span class="id" title="definition">object_map</span></a>) :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">fun</span> <span class="id" title="var">Fgrp</span> <span class="id" title="var">Fsub</span> <span class="id" title="var">Fcont</span> (<span class="id" title="var">isoF</span> := @<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.IsoMap"><span class="id" title="constructor">IsoMap</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#Fgrp"><span class="id" title="variable">Fgrp</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#Fsub"><span class="id" title="variable">Fsub</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#Fcont"><span class="id" title="variable">Fcont</span></a>) ⇒<br/>
&nbsp;&nbsp;<span class="id" title="keyword">fun</span> <span class="id" title="var">isoF0</span> &amp; <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.apply"><span class="id" title="projection">apply</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#isoF0"><span class="id" title="variable">isoF0</span></a>) <a class="idref" href="mathcomp.solvable.gfunctor.html#F"><span class="id" title="variable">F</span></a> &amp; <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#isoF"><span class="id" title="variable">isoF</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#isoF0"><span class="id" title="variable">isoF0</span></a> ⇒ <a class="idref" href="mathcomp.solvable.gfunctor.html#isoF"><span class="id" title="variable">isoF</span></a>.<br/>

<br/>
<span class="id" title="keyword">Definition</span> <a name="GFunctor.clone"><span class="id" title="definition">clone</span></a> (<span class="id" title="var">F</span> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.object_map"><span class="id" title="definition">object_map</span></a>) :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">fun</span> <span class="id" title="var">isoF</span> &amp; <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.apply"><span class="id" title="projection">apply</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#isoF"><span class="id" title="variable">isoF</span></a>) <a class="idref" href="mathcomp.solvable.gfunctor.html#F"><span class="id" title="variable">F</span></a> ⇒<br/>
&nbsp;&nbsp;<span class="id" title="keyword">fun</span> (<span class="id" title="var">funF0</span> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.map"><span class="id" title="record">map</span></a>) &amp; <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.apply"><span class="id" title="projection">apply</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#funF0"><span class="id" title="variable">funF0</span></a>) <a class="idref" href="mathcomp.solvable.gfunctor.html#F"><span class="id" title="variable">F</span></a> ⇒<br/>
&nbsp;&nbsp;<span class="id" title="keyword">fun</span> <span class="id" title="var">Fcont</span> (<span class="id" title="var">funF</span> := @<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Map"><span class="id" title="constructor">Map</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#isoF"><span class="id" title="variable">isoF</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#Fcont"><span class="id" title="variable">Fcont</span></a>) &amp; <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#funF0"><span class="id" title="variable">funF0</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#funF"><span class="id" title="variable">funF</span></a> ⇒ <a class="idref" href="mathcomp.solvable.gfunctor.html#funF"><span class="id" title="variable">funF</span></a>.<br/>

<br/>
<span class="id" title="keyword">Definition</span> <a name="GFunctor.clone_pmap"><span class="id" title="definition">clone_pmap</span></a> (<span class="id" title="var">F</span> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.object_map"><span class="id" title="definition">object_map</span></a>) :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">fun</span> (<span class="id" title="var">funF</span> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.map"><span class="id" title="record">map</span></a>) &amp; <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.apply"><span class="id" title="projection">apply</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#funF"><span class="id" title="variable">funF</span></a>) <a class="idref" href="mathcomp.solvable.gfunctor.html#F"><span class="id" title="variable">F</span></a> ⇒<br/>
&nbsp;&nbsp;<span class="id" title="keyword">fun</span> (<span class="id" title="var">pfunF0</span> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.pmap"><span class="id" title="record">pmap</span></a>) &amp; <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.apply"><span class="id" title="projection">apply</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#pfunF0"><span class="id" title="variable">pfunF0</span></a>) <a class="idref" href="mathcomp.solvable.gfunctor.html#F"><span class="id" title="variable">F</span></a> ⇒<br/>
&nbsp;&nbsp;<span class="id" title="keyword">fun</span> <span class="id" title="var">Fher</span> (<span class="id" title="var">pfunF</span> := @<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Pmap"><span class="id" title="constructor">Pmap</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#funF"><span class="id" title="variable">funF</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#Fher"><span class="id" title="variable">Fher</span></a>) &amp; <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#pfunF0"><span class="id" title="variable">pfunF0</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#pfunF"><span class="id" title="variable">pfunF</span></a> ⇒ <a class="idref" href="mathcomp.solvable.gfunctor.html#pfunF"><span class="id" title="variable">pfunF</span></a>.<br/>

<br/>
<span class="id" title="keyword">Definition</span> <a name="GFunctor.clone_mono"><span class="id" title="definition">clone_mono</span></a> (<span class="id" title="var">F</span> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.object_map"><span class="id" title="definition">object_map</span></a>) :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">fun</span> (<span class="id" title="var">funF</span> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.map"><span class="id" title="record">map</span></a>) &amp; <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.apply"><span class="id" title="projection">apply</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#funF"><span class="id" title="variable">funF</span></a>) <a class="idref" href="mathcomp.solvable.gfunctor.html#F"><span class="id" title="variable">F</span></a> ⇒<br/>
&nbsp;&nbsp;<span class="id" title="keyword">fun</span> (<span class="id" title="var">mfunF0</span> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.mono_map"><span class="id" title="record">mono_map</span></a>) &amp; <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.apply"><span class="id" title="projection">apply</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#mfunF0"><span class="id" title="variable">mfunF0</span></a>) <a class="idref" href="mathcomp.solvable.gfunctor.html#F"><span class="id" title="variable">F</span></a> ⇒<br/>
&nbsp;&nbsp;<span class="id" title="keyword">fun</span> <span class="id" title="var">Fmon</span> (<span class="id" title="var">mfunF</span> := @<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.MonoMap"><span class="id" title="constructor">MonoMap</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#funF"><span class="id" title="variable">funF</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#Fmon"><span class="id" title="variable">Fmon</span></a>) &amp; <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#mfunF0"><span class="id" title="variable">mfunF0</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#mfunF"><span class="id" title="variable">mfunF</span></a> ⇒ <a class="idref" href="mathcomp.solvable.gfunctor.html#mfunF"><span class="id" title="variable">mfunF</span></a>.<br/>

<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.ClassDefinitions"><span class="id" title="section">ClassDefinitions</span></a>.<br/>

<br/>
<span class="id" title="keyword">Module</span> <a name="GFunctor.Exports"><span class="id" title="module">Exports</span></a>.<br/>

<br/>
<span class="id" title="keyword">Identity</span> <span class="id" title="keyword">Coercion</span> <span class="id" title="var">fun_of_object_map</span> : <span class="id" title="var">object_map</span> &gt;-&gt; <span class="id" title="var">Funclass</span>.<br/>
<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.apply"><span class="id" title="projection">apply</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.apply"><span class="id" title="projection">:</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.apply"><span class="id" title="projection">iso_map</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.apply"><span class="id" title="projection">&gt;-&gt;</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.apply"><span class="id" title="projection">object_map</span></a>.<br/>
<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.iso_of_map"><span class="id" title="projection">iso_of_map</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.iso_of_map"><span class="id" title="projection">:</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.iso_of_map"><span class="id" title="projection">map</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.iso_of_map"><span class="id" title="projection">&gt;-&gt;</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.iso_of_map"><span class="id" title="projection">iso_map</span></a>.<br/>
<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.map_of_pmap"><span class="id" title="projection">map_of_pmap</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.map_of_pmap"><span class="id" title="projection">:</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.map_of_pmap"><span class="id" title="projection">pmap</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.map_of_pmap"><span class="id" title="projection">&gt;-&gt;</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.map_of_pmap"><span class="id" title="projection">map</span></a>.<br/>
<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.map_of_mono"><span class="id" title="projection">map_of_mono</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.map_of_mono"><span class="id" title="projection">:</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.map_of_mono"><span class="id" title="projection">mono_map</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.map_of_mono"><span class="id" title="projection">&gt;-&gt;</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.map_of_mono"><span class="id" title="projection">map</span></a>.<br/>
<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.continuous_is_iso_continuous"><span class="id" title="lemma">continuous_is_iso_continuous</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.continuous_is_iso_continuous"><span class="id" title="lemma">:</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.continuous_is_iso_continuous"><span class="id" title="lemma">continuous</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.continuous_is_iso_continuous"><span class="id" title="lemma">&gt;-&gt;</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.continuous_is_iso_continuous"><span class="id" title="lemma">iso_continuous</span></a>.<br/>
<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.pcontinuous_is_continuous"><span class="id" title="lemma">pcontinuous_is_continuous</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.pcontinuous_is_continuous"><span class="id" title="lemma">:</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.pcontinuous_is_continuous"><span class="id" title="lemma">pcontinuous</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.pcontinuous_is_continuous"><span class="id" title="lemma">&gt;-&gt;</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.pcontinuous_is_continuous"><span class="id" title="lemma">continuous</span></a>.<br/>
<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.pcontinuous_is_hereditary"><span class="id" title="lemma">pcontinuous_is_hereditary</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.pcontinuous_is_hereditary"><span class="id" title="lemma">:</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.pcontinuous_is_hereditary"><span class="id" title="lemma">pcontinuous</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.pcontinuous_is_hereditary"><span class="id" title="lemma">&gt;-&gt;</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.pcontinuous_is_hereditary"><span class="id" title="lemma">hereditary</span></a>.<br/>

<br/>
<span class="id" title="keyword">Notation</span> <a name="a1ae11930941a680f6750f6723874923"><span class="id" title="notation">&quot;</span></a>[ 'igFun' 'by' Fsub &amp; Fcont ]" :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.pack_iso"><span class="id" title="definition">pack_iso</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.continuous_is_iso_continuous"><span class="id" title="lemma">continuous_is_iso_continuous</span></a> <span class="id" title="var">Fcont</span>) (<span class="id" title="keyword">fun</span> <span class="id" title="var">gT</span> <span class="id" title="var">G</span> ⇒ <a class="idref" href="mathcomp.fingroup.fingroup.html#groupP"><span class="id" title="lemma">groupP</span></a> <span class="id" title="var">_</span>) <span class="id" title="var">Fsub</span>)<br/>
&nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "[ 'igFun'  'by'  Fsub  &amp;  Fcont ]") : <span class="id" title="var">form_scope</span>.<br/>

<br/>
<span class="id" title="keyword">Notation</span> <a name="6a21e731147765f65bc5f2e922126efc"><span class="id" title="notation">&quot;</span></a>[ 'igFun' 'by' Fsub &amp; ! Fcont ]" :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.pack_iso"><span class="id" title="definition">pack_iso</span></a> <span class="id" title="var">Fcont</span> (<span class="id" title="keyword">fun</span> <span class="id" title="var">gT</span> <span class="id" title="var">G</span> ⇒ <a class="idref" href="mathcomp.fingroup.fingroup.html#groupP"><span class="id" title="lemma">groupP</span></a> <span class="id" title="var">_</span>) <span class="id" title="var">Fsub</span>)<br/>
&nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "[ 'igFun'  'by'  Fsub  &amp;  ! Fcont ]") : <span class="id" title="var">form_scope</span>.<br/>

<br/>
<span class="id" title="keyword">Notation</span> <a name="0d3cf0514afe70d7a29245834117002f"><span class="id" title="notation">&quot;</span></a>[ 'igFun' 'of' F ]" := (@<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.clone_iso"><span class="id" title="definition">clone_iso</span></a> <span class="id" title="var">F</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a>)<br/>
&nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "[ 'igFun'  'of'  F ]") : <span class="id" title="var">form_scope</span>.<br/>

<br/>
<span class="id" title="keyword">Notation</span> <a name="f83b8fb103ae042d25e7034a8b11b7e7"><span class="id" title="notation">&quot;</span></a>[ 'gFun' 'by' Fcont ]" := (<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Map"><span class="id" title="constructor">Map</span></a> <span class="id" title="var">Fcont</span>)<br/>
&nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "[ 'gFun'  'by'  Fcont ]") : <span class="id" title="var">form_scope</span>.<br/>

<br/>
<span class="id" title="keyword">Notation</span> <a name="607d805a80d936daf34262a28a285db3"><span class="id" title="notation">&quot;</span></a>[ 'gFun' 'of' F ]" := (@<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.clone"><span class="id" title="definition">clone</span></a> <span class="id" title="var">F</span> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a>)<br/>
&nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "[ 'gFun'  'of'  F ]") : <span class="id" title="var">form_scope</span>.<br/>

<br/>
<span class="id" title="keyword">Notation</span> <a name="75f5bf98333ce9930f3fc4415f01e6a0"><span class="id" title="notation">&quot;</span></a>[ 'pgFun' 'by' Fher ]" := (<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Pmap"><span class="id" title="constructor">Pmap</span></a> <span class="id" title="var">Fher</span>)<br/>
&nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "[ 'pgFun'  'by'  Fher ]") : <span class="id" title="var">form_scope</span>.<br/>

<br/>
<span class="id" title="keyword">Notation</span> <a name="ee155ab488843b0ecc37c27fc7341f64"><span class="id" title="notation">&quot;</span></a>[ 'pgFun' 'of' F ]" := (@<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.clone_pmap"><span class="id" title="definition">clone_pmap</span></a> <span class="id" title="var">F</span> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a>)<br/>
&nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "[ 'pgFun' 'of'  F ]") : <span class="id" title="var">form_scope</span>.<br/>

<br/>
<span class="id" title="keyword">Notation</span> <a name="34d675edff20d6d91e43f305650662d9"><span class="id" title="notation">&quot;</span></a>[ 'mgFun' 'by' Fmon ]" := (<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.MonoMap"><span class="id" title="constructor">MonoMap</span></a> <span class="id" title="var">Fmon</span>)<br/>
&nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "[ 'mgFun'  'by'  Fmon ]") : <span class="id" title="var">form_scope</span>.<br/>

<br/>
<span class="id" title="keyword">Notation</span> <a name="617ba6355e0c6813ccd42cf7ac127f20"><span class="id" title="notation">&quot;</span></a>[ 'mgFun' 'of' F ]" := (@<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.clone_mono"><span class="id" title="definition">clone_mono</span></a> <span class="id" title="var">F</span> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a>)<br/>
&nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "[ 'mgFun' 'of'  F ]") : <span class="id" title="var">form_scope</span>.<br/>

<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Exports"><span class="id" title="module">Exports</span></a>.<br/>

<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor"><span class="id" title="module">GFunctor</span></a>.<br/>
<span class="id" title="keyword">Export</span> <span class="id" title="var">GFunctor.Exports</span>.<br/>

<br/>

<br/>
<span class="id" title="keyword">Notation</span> <a name="5feaca9261529b1a79b9f50bc9e0bd05"><span class="id" title="notation">&quot;</span></a>F1 \o F2" := (<a class="idref" href="mathcomp.solvable.gfunctor.html#comp_head"><span class="id" title="definition">GFunctor.comp_head</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#tt"><span class="id" title="constructor">tt</span></a> <span class="id" title="var">F1</span> <span class="id" title="var">F2</span>) : <span class="id" title="var">gFun_scope</span>.<br/>
<span class="id" title="keyword">Notation</span> <a name="397612d5557f5f74747d26baf6517ab7"><span class="id" title="notation">&quot;</span></a>F1 %% F2" := (<a class="idref" href="mathcomp.solvable.gfunctor.html#modulo"><span class="id" title="definition">GFunctor.modulo</span></a> <span class="id" title="var">F1</span> <span class="id" title="var">F2</span>) : <span class="id" title="var">gFun_scope</span>.<br/>

<br/>
<span class="id" title="keyword">Section</span> <a name="FunctorGroup"><span class="id" title="section">FunctorGroup</span></a>.<br/>

<br/>
<span class="id" title="keyword">Variables</span> (<a name="FunctorGroup.F"><span class="id" title="variable">F</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#iso_map"><span class="id" title="record">GFunctor.iso_map</span></a>) (<a name="FunctorGroup.gT"><span class="id" title="variable">gT</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>) (<a name="FunctorGroup.G"><span class="id" title="variable">G</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>).<br/>
<span class="id" title="keyword">Lemma</span> <a name="gFgroupset"><span class="id" title="lemma">gFgroupset</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#group_set"><span class="id" title="definition">group_set</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#FunctorGroup.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#FunctorGroup.gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#FunctorGroup.G"><span class="id" title="variable">G</span></a>).  <br/>
<span class="id" title="keyword">Canonical</span> <span class="id" title="var">gFgroup</span> := <a class="idref" href="mathcomp.fingroup.fingroup.html#Group"><span class="id" title="constructor">Group</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gFgroupset"><span class="id" title="lemma">gFgroupset</span></a>.<br/>

<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.gfunctor.html#FunctorGroup"><span class="id" title="section">FunctorGroup</span></a>.<br/>

<br/>
<span class="id" title="keyword">Canonical</span> <span class="id" title="var">gFmod_group</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" title="var">F1</span> : <a class="idref" href="mathcomp.solvable.gfunctor.html#iso_map"><span class="id" title="record">GFunctor.iso_map</span></a>) (<span class="id" title="var">F2</span> : <a class="idref" href="mathcomp.solvable.gfunctor.html#object_map"><span class="id" title="definition">GFunctor.object_map</span></a>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" title="var">gT</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>) (<span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) :=<br/>
&nbsp;&nbsp;<a class="idref" href="mathcomp.fingroup.fingroup.html#ccb763a84253e971fd106aeeb9cd3cb0"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ccb763a84253e971fd106aeeb9cd3cb0"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#ccb763a84253e971fd106aeeb9cd3cb0"><span class="id" title="notation">of</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#F1"><span class="id" title="variable">F1</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#397612d5557f5f74747d26baf6517ab7"><span class="id" title="notation">%%</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#F2"><span class="id" title="variable">F2</span></a>)%<span class="id" title="var">gF</span> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ccb763a84253e971fd106aeeb9cd3cb0"><span class="id" title="notation">]</span></a>.<br/>

<br/>
<span class="id" title="keyword">Section</span> <a name="IsoFunctorTheory"><span class="id" title="section">IsoFunctorTheory</span></a>.<br/>

<br/>
<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> <span class="id" title="var">gT</span> <span class="id" title="var">rT</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>.<br/>
<span class="id" title="keyword">Variable</span> <a name="IsoFunctorTheory.F"><span class="id" title="variable">F</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#iso_map"><span class="id" title="record">GFunctor.iso_map</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="gFsub"><span class="id" title="lemma">gFsub</span></a> <span class="id" title="var">gT</span> (<span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) : <a class="idref" href="mathcomp.solvable.gfunctor.html#IsoFunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="gFsub_trans"><span class="id" title="lemma">gFsub_trans</span></a> <span class="id" title="var">gT</span> (<span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">A</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#pred_class"><span class="id" title="abbreviation">pred_class</span></a>) :<br/>
&nbsp;&nbsp;<a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#IsoFunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#A"><span class="id" title="variable">A</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="gF1"><span class="id" title="lemma">gF1</span></a> <span class="id" title="var">gT</span> : <a class="idref" href="mathcomp.solvable.gfunctor.html#IsoFunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> 1 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> 1.  <br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="gFiso_cont"><span class="id" title="lemma">gFiso_cont</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#iso_continuous"><span class="id" title="definition">GFunctor.iso_continuous</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#IsoFunctorTheory.F"><span class="id" title="variable">F</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="gFchar"><span class="id" title="lemma">gFchar</span></a> <span class="id" title="var">gT</span> (<span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) : <a class="idref" href="mathcomp.solvable.gfunctor.html#IsoFunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#004858100bfba9714bde1cdbce60358b"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.automorphism.html#004858100bfba9714bde1cdbce60358b"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="gFnorm"><span class="id" title="lemma">gFnorm</span></a> <span class="id" title="var">gT</span> (<span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) : <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#IsoFunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">)</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="gFnorms"><span class="id" title="lemma">gFnorms</span></a> <span class="id" title="var">gT</span> (<span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) : <a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#IsoFunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">)</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="gFnormal"><span class="id" title="lemma">gFnormal</span></a> <span class="id" title="var">gT</span> (<span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) : <a class="idref" href="mathcomp.solvable.gfunctor.html#IsoFunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#c27c638e534bbb5b7de2d4b4aa0a3e82"><span class="id" title="notation">&lt;|</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="gFchar_trans"><span class="id" title="lemma">gFchar_trans</span></a> <span class="id" title="var">gT</span> (<span class="id" title="var">G</span> <span class="id" title="var">H</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) : <a class="idref" href="mathcomp.solvable.gfunctor.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#004858100bfba9714bde1cdbce60358b"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.automorphism.html#004858100bfba9714bde1cdbce60358b"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#IsoFunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#004858100bfba9714bde1cdbce60358b"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.automorphism.html#004858100bfba9714bde1cdbce60358b"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="gFnormal_trans"><span class="id" title="lemma">gFnormal_trans</span></a> <span class="id" title="var">gT</span> (<span class="id" title="var">G</span> <span class="id" title="var">H</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) : <a class="idref" href="mathcomp.solvable.gfunctor.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#c27c638e534bbb5b7de2d4b4aa0a3e82"><span class="id" title="notation">&lt;|</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#IsoFunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#c27c638e534bbb5b7de2d4b4aa0a3e82"><span class="id" title="notation">&lt;|</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="gFnorm_trans"><span class="id" title="lemma">gFnorm_trans</span></a> <span class="id" title="var">gT</span> (<span class="id" title="var">A</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#pred_class"><span class="id" title="abbreviation">pred_class</span></a>) (<span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) :<br/>
&nbsp;&nbsp;<a class="idref" href="mathcomp.solvable.gfunctor.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#IsoFunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">)</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="injmF_sub"><span class="id" title="lemma">injmF_sub</span></a> <span class="id" title="var">gT</span> <span class="id" title="var">rT</span> (<span class="id" title="var">G</span> <span class="id" title="var">D</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">f</span> : <a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">morphism</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">&gt;-&gt;</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">}</span></a>) :<br/>
&nbsp;&nbsp;<a class="idref" href="mathcomp.fingroup.morphism.html#14bfb149f00fa839cfb11397f4fe629f"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#14bfb149f00fa839cfb11397f4fe629f"><span class="id" title="notation">injm</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#IsoFunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#IsoFunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#rT"><span class="id" title="variable">rT</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a>).<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="injmF"><span class="id" title="lemma">injmF</span></a> <span class="id" title="var">gT</span> <span class="id" title="var">rT</span> (<span class="id" title="var">G</span> <span class="id" title="var">D</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">f</span> : <a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">morphism</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">&gt;-&gt;</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">}</span></a>) :<br/>
&nbsp;&nbsp;<a class="idref" href="mathcomp.fingroup.morphism.html#14bfb149f00fa839cfb11397f4fe629f"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#14bfb149f00fa839cfb11397f4fe629f"><span class="id" title="notation">injm</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#IsoFunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#IsoFunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#rT"><span class="id" title="variable">rT</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a>).<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="gFisom"><span class="id" title="lemma">gFisom</span></a> <span class="id" title="var">gT</span> <span class="id" title="var">rT</span> (<span class="id" title="var">G</span> <span class="id" title="var">D</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) <span class="id" title="var">R</span> (<span class="id" title="var">f</span> : <a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">morphism</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">&gt;-&gt;</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">}</span></a>) :<br/>
&nbsp;&nbsp;<a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#isom"><span class="id" title="definition">isom</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> (<a class="idref" href="mathcomp.fingroup.fingroup.html#gval"><span class="id" title="projection">gval</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#R"><span class="id" title="variable">R</span></a>) <a class="idref" href="mathcomp.solvable.gfunctor.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#isom"><span class="id" title="definition">isom</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#IsoFunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a>) (<a class="idref" href="mathcomp.solvable.gfunctor.html#IsoFunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#rT"><span class="id" title="variable">rT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#R"><span class="id" title="variable">R</span></a>) <a class="idref" href="mathcomp.solvable.gfunctor.html#f"><span class="id" title="variable">f</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="gFisog"><span class="id" title="lemma">gFisog</span></a> <span class="id" title="var">gT</span> <span class="id" title="var">rT</span> (<span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">R</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) :<br/>
&nbsp;&nbsp;<a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">isog</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#R"><span class="id" title="variable">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#IsoFunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">isog</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#IsoFunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#rT"><span class="id" title="variable">rT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#R"><span class="id" title="variable">R</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.gfunctor.html#IsoFunctorTheory"><span class="id" title="section">IsoFunctorTheory</span></a>.<br/>

<br/>
<span class="id" title="keyword">Section</span> <a name="FunctorTheory"><span class="id" title="section">FunctorTheory</span></a>.<br/>

<br/>
<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> <span class="id" title="var">gT</span> <span class="id" title="var">rT</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>.<br/>
<span class="id" title="keyword">Variable</span> <a name="FunctorTheory.F"><span class="id" title="variable">F</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#map"><span class="id" title="record">GFunctor.map</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="gFcont"><span class="id" title="lemma">gFcont</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#continuous"><span class="id" title="definition">GFunctor.continuous</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#FunctorTheory.F"><span class="id" title="variable">F</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="morphimF"><span class="id" title="lemma">morphimF</span></a> <span class="id" title="var">gT</span> <span class="id" title="var">rT</span> (<span class="id" title="var">G</span> <span class="id" title="var">D</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">f</span> : <a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">morphism</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">&gt;-&gt;</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">}</span></a>) :<br/>
&nbsp;&nbsp;<a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#FunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#FunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#rT"><span class="id" title="variable">rT</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a>).<br/>

<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.gfunctor.html#FunctorTheory"><span class="id" title="section">FunctorTheory</span></a>.<br/>

<br/>
<span class="id" title="keyword">Section</span> <a name="PartialFunctorTheory"><span class="id" title="section">PartialFunctorTheory</span></a>.<br/>

<br/>
<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> <span class="id" title="var">gT</span> <span class="id" title="var">rT</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>.<br/>

<br/>
<span class="id" title="keyword">Section</span> <a name="PartialFunctorTheory.BasicTheory"><span class="id" title="section">BasicTheory</span></a>.<br/>

<br/>
<span class="id" title="keyword">Variable</span> <a name="PartialFunctorTheory.BasicTheory.F"><span class="id" title="variable">F</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#pmap"><span class="id" title="record">GFunctor.pmap</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="gFhereditary"><span class="id" title="lemma">gFhereditary</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#hereditary"><span class="id" title="definition">GFunctor.hereditary</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#PartialFunctorTheory.BasicTheory.F"><span class="id" title="variable">F</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="gFunctorI"><span class="id" title="lemma">gFunctorI</span></a> <span class="id" title="var">gT</span> (<span class="id" title="var">G</span> <span class="id" title="var">H</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) :<br/>
&nbsp;&nbsp;<a class="idref" href="mathcomp.solvable.gfunctor.html#PartialFunctorTheory.BasicTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#cb41714a5a23482f7a48a98975fa8c59"><span class="id" title="notation">:&amp;:</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#PartialFunctorTheory.BasicTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#cb41714a5a23482f7a48a98975fa8c59"><span class="id" title="notation">:&amp;:</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#PartialFunctorTheory.BasicTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#cb41714a5a23482f7a48a98975fa8c59"><span class="id" title="notation">:&amp;:</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#H"><span class="id" title="variable">H</span></a>).<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="pmorphimF"><span class="id" title="lemma">pmorphimF</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#pcontinuous"><span class="id" title="definition">GFunctor.pcontinuous</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#PartialFunctorTheory.BasicTheory.F"><span class="id" title="variable">F</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="gFid"><span class="id" title="lemma">gFid</span></a> <span class="id" title="var">gT</span> (<span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) : <a class="idref" href="mathcomp.solvable.gfunctor.html#PartialFunctorTheory.BasicTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#PartialFunctorTheory.BasicTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a>)  <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#PartialFunctorTheory.BasicTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a>.<br/>

<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.gfunctor.html#PartialFunctorTheory.BasicTheory"><span class="id" title="section">BasicTheory</span></a>.<br/>

<br/>
<span class="id" title="keyword">Section</span> <a name="PartialFunctorTheory.Modulo"><span class="id" title="section">Modulo</span></a>.<br/>

<br/>
<span class="id" title="keyword">Variables</span> (<a name="PartialFunctorTheory.Modulo.F1"><span class="id" title="variable">F1</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#pmap"><span class="id" title="record">GFunctor.pmap</span></a>) (<a name="PartialFunctorTheory.Modulo.F2"><span class="id" title="variable">F2</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#map"><span class="id" title="record">GFunctor.map</span></a>).<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="gFmod_closed"><span class="id" title="lemma">gFmod_closed</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#closed"><span class="id" title="definition">GFunctor.closed</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#PartialFunctorTheory.Modulo.F1"><span class="id" title="variable">F1</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#397612d5557f5f74747d26baf6517ab7"><span class="id" title="notation">%%</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#PartialFunctorTheory.Modulo.F2"><span class="id" title="variable">F2</span></a>).<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="gFmod_cont"><span class="id" title="lemma">gFmod_cont</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#continuous"><span class="id" title="definition">GFunctor.continuous</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#PartialFunctorTheory.Modulo.F1"><span class="id" title="variable">F1</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#397612d5557f5f74747d26baf6517ab7"><span class="id" title="notation">%%</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#PartialFunctorTheory.Modulo.F2"><span class="id" title="variable">F2</span></a>).<br/>

<br/>
<span class="id" title="keyword">Canonical</span> <span class="id" title="var">gFmod_igFun</span> := <a class="idref" href="mathcomp.solvable.gfunctor.html#a1ae11930941a680f6750f6723874923"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#a1ae11930941a680f6750f6723874923"><span class="id" title="notation">igFun</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#a1ae11930941a680f6750f6723874923"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gFmod_closed"><span class="id" title="lemma">gFmod_closed</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#a1ae11930941a680f6750f6723874923"><span class="id" title="notation">&amp;</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gFmod_cont"><span class="id" title="lemma">gFmod_cont</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#a1ae11930941a680f6750f6723874923"><span class="id" title="notation">]</span></a>.<br/>
<span class="id" title="keyword">Canonical</span> <span class="id" title="var">gFmod_gFun</span> := <a class="idref" href="mathcomp.solvable.gfunctor.html#f83b8fb103ae042d25e7034a8b11b7e7"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#f83b8fb103ae042d25e7034a8b11b7e7"><span class="id" title="notation">gFun</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#f83b8fb103ae042d25e7034a8b11b7e7"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gFmod_cont"><span class="id" title="lemma">gFmod_cont</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#f83b8fb103ae042d25e7034a8b11b7e7"><span class="id" title="notation">]</span></a>.<br/>

<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.gfunctor.html#PartialFunctorTheory.Modulo"><span class="id" title="section">Modulo</span></a>.<br/>

<br/>
<span class="id" title="keyword">Variables</span> <a name="PartialFunctorTheory.F1"><span class="id" title="variable">F1</span></a> <a name="PartialFunctorTheory.F2"><span class="id" title="variable">F2</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#pmap"><span class="id" title="record">GFunctor.pmap</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="gFmod_hereditary"><span class="id" title="lemma">gFmod_hereditary</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#hereditary"><span class="id" title="definition">GFunctor.hereditary</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#PartialFunctorTheory.F1"><span class="id" title="variable">F1</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#397612d5557f5f74747d26baf6517ab7"><span class="id" title="notation">%%</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#PartialFunctorTheory.F2"><span class="id" title="variable">F2</span></a>).<br/>

<br/>
<span class="id" title="keyword">Canonical</span> <span class="id" title="var">gFmod_pgFun</span> := <a class="idref" href="mathcomp.solvable.gfunctor.html#75f5bf98333ce9930f3fc4415f01e6a0"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#75f5bf98333ce9930f3fc4415f01e6a0"><span class="id" title="notation">pgFun</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#75f5bf98333ce9930f3fc4415f01e6a0"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gFmod_hereditary"><span class="id" title="lemma">gFmod_hereditary</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#75f5bf98333ce9930f3fc4415f01e6a0"><span class="id" title="notation">]</span></a>.<br/>

<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.gfunctor.html#PartialFunctorTheory"><span class="id" title="section">PartialFunctorTheory</span></a>.<br/>

<br/>
<span class="id" title="keyword">Section</span> <a name="MonotonicFunctorTheory"><span class="id" title="section">MonotonicFunctorTheory</span></a>.<br/>

<br/>
<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> <span class="id" title="var">gT</span> <span class="id" title="var">rT</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="gFunctorS"><span class="id" title="lemma">gFunctorS</span></a> (<span class="id" title="var">F</span> : <a class="idref" href="mathcomp.solvable.gfunctor.html#mono_map"><span class="id" title="record">GFunctor.mono_map</span></a>) : <a class="idref" href="mathcomp.solvable.gfunctor.html#monotonic"><span class="id" title="definition">GFunctor.monotonic</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#F"><span class="id" title="variable">F</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Section</span> <a name="MonotonicFunctorTheory.Composition"><span class="id" title="section">Composition</span></a>.<br/>

<br/>
<span class="id" title="keyword">Variables</span> (<a name="MonotonicFunctorTheory.Composition.F1"><span class="id" title="variable">F1</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#mono_map"><span class="id" title="record">GFunctor.mono_map</span></a>) (<a name="MonotonicFunctorTheory.Composition.F2"><span class="id" title="variable">F2</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#map"><span class="id" title="record">GFunctor.map</span></a>).<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="gFcomp_closed"><span class="id" title="lemma">gFcomp_closed</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#closed"><span class="id" title="definition">GFunctor.closed</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#MonotonicFunctorTheory.Composition.F1"><span class="id" title="variable">F1</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#5feaca9261529b1a79b9f50bc9e0bd05"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#5feaca9261529b1a79b9f50bc9e0bd05"><span class="id" title="notation">o</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#MonotonicFunctorTheory.Composition.F2"><span class="id" title="variable">F2</span></a>).<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="gFcomp_cont"><span class="id" title="lemma">gFcomp_cont</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#continuous"><span class="id" title="definition">GFunctor.continuous</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#MonotonicFunctorTheory.Composition.F1"><span class="id" title="variable">F1</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#5feaca9261529b1a79b9f50bc9e0bd05"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#5feaca9261529b1a79b9f50bc9e0bd05"><span class="id" title="notation">o</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#MonotonicFunctorTheory.Composition.F2"><span class="id" title="variable">F2</span></a>).<br/>

<br/>
<span class="id" title="keyword">Canonical</span> <span class="id" title="var">gFcomp_igFun</span> := <a class="idref" href="mathcomp.solvable.gfunctor.html#a1ae11930941a680f6750f6723874923"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#a1ae11930941a680f6750f6723874923"><span class="id" title="notation">igFun</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#a1ae11930941a680f6750f6723874923"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gFcomp_closed"><span class="id" title="lemma">gFcomp_closed</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#a1ae11930941a680f6750f6723874923"><span class="id" title="notation">&amp;</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gFcomp_cont"><span class="id" title="lemma">gFcomp_cont</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#a1ae11930941a680f6750f6723874923"><span class="id" title="notation">]</span></a>.<br/>
<span class="id" title="keyword">Canonical</span> <span class="id" title="var">gFcomp_gFun</span> :=<a class="idref" href="mathcomp.solvable.gfunctor.html#f83b8fb103ae042d25e7034a8b11b7e7"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#f83b8fb103ae042d25e7034a8b11b7e7"><span class="id" title="notation">gFun</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#f83b8fb103ae042d25e7034a8b11b7e7"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gFcomp_cont"><span class="id" title="lemma">gFcomp_cont</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#f83b8fb103ae042d25e7034a8b11b7e7"><span class="id" title="notation">]</span></a>.<br/>

<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.gfunctor.html#MonotonicFunctorTheory.Composition"><span class="id" title="section">Composition</span></a>.<br/>

<br/>
<span class="id" title="keyword">Variables</span> <a name="MonotonicFunctorTheory.F1"><span class="id" title="variable">F1</span></a> <a name="MonotonicFunctorTheory.F2"><span class="id" title="variable">F2</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#mono_map"><span class="id" title="record">GFunctor.mono_map</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="gFcompS"><span class="id" title="lemma">gFcompS</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#monotonic"><span class="id" title="definition">GFunctor.monotonic</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#MonotonicFunctorTheory.F1"><span class="id" title="variable">F1</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#5feaca9261529b1a79b9f50bc9e0bd05"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#5feaca9261529b1a79b9f50bc9e0bd05"><span class="id" title="notation">o</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#MonotonicFunctorTheory.F2"><span class="id" title="variable">F2</span></a>).<br/>
 
<br/>
<span class="id" title="keyword">Canonical</span> <span class="id" title="var">gFcomp_mgFun</span> := <a class="idref" href="mathcomp.solvable.gfunctor.html#34d675edff20d6d91e43f305650662d9"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#34d675edff20d6d91e43f305650662d9"><span class="id" title="notation">mgFun</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#34d675edff20d6d91e43f305650662d9"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gFcompS"><span class="id" title="lemma">gFcompS</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#34d675edff20d6d91e43f305650662d9"><span class="id" title="notation">]</span></a>.<br/>

<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.gfunctor.html#MonotonicFunctorTheory"><span class="id" title="section">MonotonicFunctorTheory</span></a>.<br/>

<br/>
<span class="id" title="keyword">Section</span> <a name="GFunctorExamples"><span class="id" title="section">GFunctorExamples</span></a>.<br/>

<br/>
<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> <span class="id" title="var">gT</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>.<br/>

<br/>
<span class="id" title="keyword">Definition</span> <a name="idGfun"><span class="id" title="definition">idGfun</span></a> <span class="id" title="var">gT</span> := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#18cd0ece1c60c28b29a57eea4cb098ca"><span class="id" title="notation">@</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#18cd0ece1c60c28b29a57eea4cb098ca"><span class="id" title="notation">id</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">}</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="idGfun_closed"><span class="id" title="lemma">idGfun_closed</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#closed"><span class="id" title="definition">GFunctor.closed</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#idGfun"><span class="id" title="definition">idGfun</span></a>.  <br/>
<span class="id" title="keyword">Lemma</span> <a name="idGfun_cont"><span class="id" title="lemma">idGfun_cont</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#continuous"><span class="id" title="definition">GFunctor.continuous</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#idGfun"><span class="id" title="definition">idGfun</span></a>.  <br/>
<span class="id" title="keyword">Lemma</span> <a name="idGfun_monotonic"><span class="id" title="lemma">idGfun_monotonic</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#monotonic"><span class="id" title="definition">GFunctor.monotonic</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#idGfun"><span class="id" title="definition">idGfun</span></a>.  <br/>

<br/>
<span class="id" title="keyword">Canonical</span> <span class="id" title="var">bgFunc_id</span> := <a class="idref" href="mathcomp.solvable.gfunctor.html#a1ae11930941a680f6750f6723874923"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#a1ae11930941a680f6750f6723874923"><span class="id" title="notation">igFun</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#a1ae11930941a680f6750f6723874923"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#idGfun_closed"><span class="id" title="lemma">idGfun_closed</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#a1ae11930941a680f6750f6723874923"><span class="id" title="notation">&amp;</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#idGfun_cont"><span class="id" title="lemma">idGfun_cont</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#a1ae11930941a680f6750f6723874923"><span class="id" title="notation">]</span></a>.<br/>
<span class="id" title="keyword">Canonical</span> <span class="id" title="var">gFunc_id</span> := <a class="idref" href="mathcomp.solvable.gfunctor.html#f83b8fb103ae042d25e7034a8b11b7e7"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#f83b8fb103ae042d25e7034a8b11b7e7"><span class="id" title="notation">gFun</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#f83b8fb103ae042d25e7034a8b11b7e7"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#idGfun_cont"><span class="id" title="lemma">idGfun_cont</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#f83b8fb103ae042d25e7034a8b11b7e7"><span class="id" title="notation">]</span></a>.<br/>
<span class="id" title="keyword">Canonical</span> <span class="id" title="var">mgFunc_id</span> := <a class="idref" href="mathcomp.solvable.gfunctor.html#34d675edff20d6d91e43f305650662d9"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#34d675edff20d6d91e43f305650662d9"><span class="id" title="notation">mgFun</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#34d675edff20d6d91e43f305650662d9"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#idGfun_monotonic"><span class="id" title="lemma">idGfun_monotonic</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#34d675edff20d6d91e43f305650662d9"><span class="id" title="notation">]</span></a>.<br/>

<br/>
<span class="id" title="keyword">Definition</span> <a name="trivGfun"><span class="id" title="definition">trivGfun</span></a> <span class="id" title="var">gT</span> <span class="id" title="keyword">of</span> <a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">}</span></a> := <a class="idref" href="mathcomp.fingroup.fingroup.html#26d0437a0433a7dd4f49130a7fb26acc"><span class="id" title="notation">[1</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#26d0437a0433a7dd4f49130a7fb26acc"><span class="id" title="notation">]</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="trivGfun_cont"><span class="id" title="lemma">trivGfun_cont</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#pcontinuous"><span class="id" title="definition">GFunctor.pcontinuous</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#trivGfun"><span class="id" title="definition">trivGfun</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Canonical</span> <span class="id" title="var">trivGfun_igFun</span> := <a class="idref" href="mathcomp.solvable.gfunctor.html#a1ae11930941a680f6750f6723874923"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#a1ae11930941a680f6750f6723874923"><span class="id" title="notation">igFun</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#a1ae11930941a680f6750f6723874923"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#sub1G"><span class="id" title="lemma">sub1G</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#a1ae11930941a680f6750f6723874923"><span class="id" title="notation">&amp;</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#trivGfun_cont"><span class="id" title="lemma">trivGfun_cont</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#a1ae11930941a680f6750f6723874923"><span class="id" title="notation">]</span></a>.<br/>
<span class="id" title="keyword">Canonical</span> <span class="id" title="var">trivGfun_gFun</span> := <a class="idref" href="mathcomp.solvable.gfunctor.html#f83b8fb103ae042d25e7034a8b11b7e7"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#f83b8fb103ae042d25e7034a8b11b7e7"><span class="id" title="notation">gFun</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#f83b8fb103ae042d25e7034a8b11b7e7"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#trivGfun_cont"><span class="id" title="lemma">trivGfun_cont</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#f83b8fb103ae042d25e7034a8b11b7e7"><span class="id" title="notation">]</span></a>.<br/>
<span class="id" title="keyword">Canonical</span> <span class="id" title="var">trivGfun_pgFun</span> := <a class="idref" href="mathcomp.solvable.gfunctor.html#75f5bf98333ce9930f3fc4415f01e6a0"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#75f5bf98333ce9930f3fc4415f01e6a0"><span class="id" title="notation">pgFun</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#75f5bf98333ce9930f3fc4415f01e6a0"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#trivGfun_cont"><span class="id" title="lemma">trivGfun_cont</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#75f5bf98333ce9930f3fc4415f01e6a0"><span class="id" title="notation">]</span></a>.<br/>

<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctorExamples"><span class="id" title="section">GFunctorExamples</span></a>.<br/>

<br/>
</div>
</div>

<div id="footer">
<hr/><a href="index.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a>
</div>

</div>

</body>
</html>