EtaleFundamentalGroups.Inertia.commAlgIdealInertiaGroup
The actual ideal inertia for the native coefficient automorphisms.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u vLean source · statement
def commAlgIdealInertiaGroup (A : Type u) [CommRing A] (B : CommAlgCat.{v} A)
(Q : Ideal B.carrier) : GrpCat.{v}