diff options
Diffstat (limited to 'docs/htmldoc/mathcomp.solvable.gfunctor.html')
| -rw-r--r-- | docs/htmldoc/mathcomp.solvable.gfunctor.html | 585 |
1 files changed, 585 insertions, 0 deletions
diff --git a/docs/htmldoc/mathcomp.solvable.gfunctor.html b/docs/htmldoc/mathcomp.solvable.gfunctor.html new file mode 100644 index 0000000..871ba2b --- /dev/null +++ b/docs/htmldoc/mathcomp.solvable.gfunctor.html @@ -0,0 +1,585 @@ +<!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">(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. <br/> + Distributed under the terms of CeCILL-B. *)</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} -> {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 <-> F G is a group when G is a group + closed F <-> F G is a subgroup o fG when G is a group + continuous F <-> F is continuous with respect to morphism image: + for any f : {morphism G >-> ..}, 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 <-> 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 <-> 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 <-> 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 <-> 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 & !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 & 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/> + <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">>-></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/> + <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/> + <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">>-></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/> + <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/> + <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">>-></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/> + <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/> + <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">:&:</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/> + <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/> + <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/> + <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/> + <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/> + <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/> + <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/> + <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/> + <span class="id" title="keyword">fun</span> <span class="id" title="var">isoF0</span> & <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> & <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/> + <span class="id" title="keyword">fun</span> <span class="id" title="var">isoF</span> & <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/> + <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>) & <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/> + <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>) & <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/> + <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>) & <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/> + <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>) & <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/> + <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>) & <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/> + <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>) & <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/> + <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>) & <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/> + <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>) & <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> >-> <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">>-></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">>-></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">>-></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">>-></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">>-></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">>-></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">>-></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">"</span></a>[ 'igFun' 'by' Fsub & Fcont ]" :=<br/> + (<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/> + (<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 & 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">"</span></a>[ 'igFun' 'by' Fsub & ! Fcont ]" :=<br/> + (<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/> + (<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 & ! 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">"</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/> + (<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">"</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/> + (<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">"</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/> + (<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">"</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/> + (<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">"</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/> + (<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">"</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/> + (<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">"</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/> + (<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">"</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">"</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/> + (<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/> + (<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/> + <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/> + <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"><|</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"><|</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"><|</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/> + <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">>-></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/> + <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">>-></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/> + <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">>-></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/> + <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/> + <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">>-></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/> + <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/> + <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">:&:</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">:&:</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">:&:</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">&</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">&</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">&</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">&</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>
\ No newline at end of file |