EtaleFundamentalGroups.Inertia.commAlgIdealInertia_eq_one_iff_coefficient
An intrinsic inertia element is the identity exactly when its actual coefficient ring map is the identity.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u vLean source · statement
theorem commAlgIdealInertia_eq_one_iff_coefficient
(A : Type u) [CommRing A] (B : CommAlgCat.{v} A) (Q : Ideal B.carrier)
(τ : (commAlgIdealInertiaGroup A B Q).carrier) :
τ = 1 ↔ commAlgAutomorphismRingHom A B τ.val = RingHom.id B.carrier