EtaleFundamentalGroups.Inertia.coefficientInertia_exists_preimage
A coefficient-automorphism lift with the same actual ring action preserves the literal inertia condition.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u vLean source · full declaration
theorem coefficientInertia_exists_preimage
(A : Type u) [CommRing A] (B : CommAlgCat.{v} A) (G : GrpCat.{v})
(Q : Ideal B.carrier) (a : MulSemiringAction G.carrier B.carrier)
(f : GrpCat.Hom G (commAlgAutomorphismGroup A B))
(hsurj : Function.Surjective f.hom'.toFun)
(hcompare :
let : MulSemiringAction G.carrier B.carrier := a
∀ g : G.carrier, MulSemiringAction.toRingHom G.carrier B.carrier g =
commAlgAutomorphismRingHom A B (f.hom'.toFun g)) :
let : MulSemiringAction G.carrier B.carrier := a
∀ τ : (commAlgIdealInertiaGroup A B Q).carrier,
∃ g : G.carrier, (Q.inertia G.carrier).carrier g ∧ f.hom'.toFun g = τ.val := by
intro ringAction τ
obtain ⟨g, hg⟩ := hsurj τ.val
refine ⟨g, ?_, hg⟩
intro b
change Q.carrier ((MulSemiringAction.toRingHom G.carrier B.carrier g).toFun b - b)
rw [hcompare g, hg]
exact τ.property b