EtaleFundamentalGroups.Inertia.commAlgInertiaHomOfDifference
The proved literal coefficient difference condition constructs the actual map into the existing native intrinsic ideal-inertia group.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u vLean source · full declaration
def commAlgInertiaHomOfDifference
(A : Type u) [CommRing A] (B : CommAlgCat.{v} A) (G : GrpCat.{v})
(Q : Ideal B) (f : GrpCat.Hom G (commAlgAutomorphismGroup A B))
(hf : ∀ g : G, ∀ b : B,
Q.carrier ((commAlgAutomorphismRingHom A B (f.hom'.toFun g)).toFun b - b)) :
GrpCat.Hom G (commAlgIdealInertiaGroup A B Q) where
hom' :=
{ toFun := fun g => ⟨f.hom'.toFun g, hf g⟩
map_one' := Subtype.ext f.hom'.map_one
map_mul' := fun g h => Subtype.ext (f.hom'.map_mul g h) }