EtaleFundamentalGroups.Inertia.integralAutomorphism_localized_principal_order
The original intrinsic normalization automorphism has p-power order, or is trivial in residue characteristic zero, when its actual prime localization acts by principal units. Every field/action comparison comes from the actual fraction lift and canonical localization equivalence.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups.Inertia
open TameAbhyankar.SGA1
universe u vLean source · statement
theorem integralAutomorphism_localized_principal_order
(A : Type u) (B : Type v)
[rA : CommRing A] [dA : IsDomain A]
[rB : CommRing B] [dB : IsDedekindDomain B]
[aAB : Algebra A B] [finAB : Module.Finite A B] [tfAB : Module.IsTorsionFree A B]
(σ : B ≃ₐ[A] B) :
∀ (Q : Ideal B) [Q.IsPrime], Q ≠ ⊥ →
∀ (hσ : Q = Q.comap σ.toRingEquiv.toRingHom),
(∀ (p : ℕ) [Fact p.Prime]
[CharP (IsLocalRing.ResidueField (Localization.AtPrime Q)) p],
(∀ x : Localization.AtPrime Q, ∃ a : (Localization.AtPrime Q)ˣ,
Localization.localRingEquiv Q Q σ.toRingEquiv hσ x =
x * (a : Localization.AtPrime Q) ∧
(a : Localization.AtPrime Q) - 1 ∈
IsLocalRing.maximalIdeal (Localization.AtPrime Q)) →
∃ n : ℕ, σ.toRingEquiv ^ (p ^ n) = 1) ∧
(∀ [CharZero (IsLocalRing.ResidueField (Localization.AtPrime Q))],
(∀ x : Localization.AtPrime Q, ∃ a : (Localization.AtPrime Q)ˣ,
Localization.localRingEquiv Q Q σ.toRingEquiv hσ x =
x * (a : Localization.AtPrime Q) ∧
(a : Localization.AtPrime Q) - 1 ∈
IsLocalRing.maximalIdeal (Localization.AtPrime Q)) →
σ.toRingEquiv = 1)