EtaleFundamentalGroups.Inertia.commAlgCanonicalTameMorphism
Native categorical packaging of the already constructed finite character. The local ring and stabilizer action are closed inside its existing owner.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory
universe u vLean source · statement
def commAlgCanonicalTameMorphism (A : Type u) [CommRing A] (B : CommAlgCat.{v} A)
[IsDedekindDomain B] [Finite (B ≃ₐ[A] B)]
(Q : Ideal B) [Q.IsPrime] (hQ : Q ≠ ⊥) :
commAlgIdealInertiaGroup A B Q ⟶ commAlgIdealTameRootsGroup A B Q hQ