Skip to content

Arithmetic Frobenius in towers and restrictions

10 fully proved

Ideal

TheoremElements with the same powered congruence differ by inertia#✓fully proved

Two elements satisfying the same powered congruence differ by an element of the inertia subgroup of Q.

theorem mem_inertia_of_forall_smul_sub_pow_mem
    (hσ : ∀ x : S, σ • x - x ^ r ∈ Q) (hτ : ∀ x : S, τ • x - x ^ r ∈ Q) :
    σ * τ⁻¹ ∈ Q.inertia G
Used by 2
Used byRestriction of Frobenius equals Frobenius with trivial inertia · Uniqueness of Frobenius powers with trivial inertia

Is Arith Frob At

TheoremPowers of a Frobenius map satisfy the powered congruence#✓fully proved

Powers of an arithmetic Frobenius map satisfy the powered congruence: if φ x - x ^ q ∈ Q for all x, then (φ ^ f) x - x ^ q ^ f ∈ Q.

theorem pow_apply_sub_pow_mem (h : φ.IsArithFrobAt Q) :
    ∀ (f : ℕ) (x : S),
      (φ ^ f) x - x ^ (Nat.card (R ⧸ Q.under R)) ^ f ∈ Q

TheoremPowers of a Frobenius element satisfy the powered congruence#✓fully proved

Powers of an arithmetic Frobenius element satisfy the powered congruence: if σ • x - x ^ q ∈ Q for all x, with q = Nat.card (R ⧸ Q.under R), then (σ ^ f) • x - x ^ q ^ f ∈ Q.

theorem pow_smul_sub_pow_mem (h : IsArithFrobAt R σ Q) :
    ∀ (f : ℕ) (x : B),
      (σ ^ f) • x - x ^ (Nat.card (R ⧸ Q.under R)) ^ f ∈ Q
Used by 1
Used byUniqueness of Frobenius powers with trivial inertia

TheoremRestriction of a Frobenius element along a compatible pair#✓fully proved

A Frobenius congruence restricts along a compatible pair: if ι : C →ₐ[R] B and ρ : G →* H satisfy ι (ρ g • c) = g • ι c, and σ is a Frobenius at Q, then ρ σ is a Frobenius at Q.comap ι.

theorem comap (ι : C →ₐ[R] B) (ρ : G →* H)
    (hcompat : ∀ (g : G) (c : C), ι (ρ g • c) = g • ι c)
    (h : IsArithFrobAt R σ Q) : IsArithFrobAt R (ρ σ) (Q.comap ι)
Used by 1
Used byRestriction of Frobenius equals Frobenius with trivial inertia

TheoremUniqueness of Frobenius powers with trivial inertia#✓fully proved

If σ is a Frobenius at Q and τ satisfies the powered congruence with exponent q ^ f, then σ ^ f = τ when the inertia subgroup of Q is trivial. This is a uniqueness helper for an already supplied powered congruence. The actual tower theorem below derives that congruence from the Frobenius premise over the intermediate ring and its residue cardinality.

theorem pow_eq_of_forall_smul_sub_pow_mem_of_inertia_eq_bot
    {f : ℕ} {τ : G}
    (h : IsArithFrobAt R σ Q)
    (hτ : ∀ x : B, τ • x - x ^ (Nat.card (R ⧸ Q.under R)) ^ f ∈ Q)
    (hbot : Q.inertia G = ⊥) : σ ^ f = τ
Uses 2 · Used by 1
Proof usesElements with the same powered congruence differ by inertia · Powers of a Frobenius element satisfy the powered congruence
Used byFrobenius in a tower is a power of the base Frobenius

TheoremRestriction of Frobenius equals Frobenius with trivial inertia#✓fully proved

If σ is a Frobenius at Q and τ satisfies the Frobenius congruence at Q.comap ι, then ρ σ = τ when the inertia subgroup of Q.comap ι is trivial. This is the equality form of the restriction statement of Proposition 7.22 under its unramified hypothesis.

theorem eq_comap_of_forall_smul_sub_pow_mem_of_inertia_eq_bot
    (ι : C →ₐ[R] B) (ρ : G →* H)
    (hcompat : ∀ (g : G) (c : C), ι (ρ g • c) = g • ι c)
    (h : IsArithFrobAt R σ Q)
    {τ : H}
    (hτ : ∀ x : C, τ • x - x ^ Nat.card (R ⧸ (Q.comap ι).under R) ∈ Q.comap ι)
    (hbot : (Q.comap ι).inertia H = ⊥) : ρ σ = τ
Uses 2
Proof usesElements with the same powered congruence differ by inertia · Restriction of a Frobenius element along a compatible pair

Ideal

TheoremIntermediate residue cardinality as a power of the base residue cardinality#✓fully proved

In a finite ring tower R → T → B, the intermediate prime residue quotient has cardinality equal to the base residue cardinality raised to its canonical inertia degree. The cardinality theorem is Mathlib's cardQuot_pow_inertiaDeg.

theorem natCard_quotient_under_eq_pow_inertiaDeg
    (R T : Type*) {B : Type*} [CommRing R] [CommRing T] [CommRing B]
    [Algebra R T] [Algebra T B] [Algebra R B] [IsScalarTower R T B]
    [Module.Finite R T] (Q : Ideal B) [Q.IsPrime]
    [Finite (R ⧸ Q.under R)] [Finite (T ⧸ Q.under T)] :
    Nat.card (T ⧸ Q.under T) =
      Nat.card (R ⧸ Q.under R) ^ (Q.under T).inertiaDeg R
Used by 1
Used byFrobenius in a tower is a power of the base Frobenius

Is Arith Frob At

TheoremFrobenius in a tower is a power of the base Frobenius#✓fully proved

In a finite ring tower R → T → B, the Frobenius over T, embedded into an action over R, equals the Frobenius over R raised to the intermediate residue degree when the inertia subgroup is trivial. Only H must fix T.

theorem tower_eq_of_inertia_eq_bot
    {R T B : Type*} [CommRing R] [CommRing T] [CommRing B]
    [Algebra R T] [Algebra T B] [Algebra R B] [IsScalarTower R T B]
    [Module.Finite R T] {G H : Type*} [Group G] [Group H]
    [MulSemiringAction G B] [SMulCommClass G R B]
    [MulSemiringAction H B] [SMulCommClass H T B]
    {σ : G} {τ : H} {Q : Ideal B} [Q.IsPrime]
    (hR : IsArithFrobAt R σ Q) (ι : H →* G)
    (hcompat : ∀ (h : H) (x : B), (ι h) • x = h • x)
    (hT : IsArithFrobAt T τ Q) (hbot : Q.inertia G = ⊥) :
    ι τ = σ ^ (Q.under T).inertiaDeg R
Uses 2 · Used by 2
Proof usesIntermediate residue cardinality as a power of the base residue cardinality · Uniqueness of Frobenius powers with trivial inertia
Used byFrobenius tower equality for algebra automorphisms · Frobenius tower equality for an intermediate field

TheoremFrobenius tower equality for algebra automorphisms#✓fully proved

For algebra automorphisms in a finite ring tower, the inclusion of the intermediate Frobenius is the canonical AlgEquiv.restrictScalars.

theorem tower_eq_of_inertia_eq_bot_algEquiv
    {R T B : Type*} [CommRing R] [CommRing T] [CommRing B]
    [Algebra R T] [Algebra T B] [Algebra R B] [IsScalarTower R T B]
    [Module.Finite R T] {σ : B ≃ₐ[R] B} {τ : B ≃ₐ[T] B}
    {Q : Ideal B} [Q.IsPrime]
    (hR : IsArithFrobAt R σ Q) (hT : IsArithFrobAt T τ Q)
    (hbot : Q.inertia (B ≃ₐ[R] B) = ⊥) :
    τ.restrictScalars R = σ ^ (Q.under T).inertiaDeg R
Uses 1
Proof usesFrobenius in a tower is a power of the base Frobenius

TheoremFrobenius tower equality for an intermediate field#✓fully proved

The tower equality for the source's intermediate field E ⊂ L. Here K is the fraction field of the base ring R, T is the integral closure of R in E, and B is its integral closure in L. In the number-field application these are the three rings of integers. The intermediate action is E.fixingSubgroup; the whole Gal(L/K) need not fix T.

IsArithFrobAt.tower_eq_of_inertia_eq_bot_fixingSubgroup · 15 lines 
theorem tower_eq_of_inertia_eq_bot_fixingSubgroup
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    {R T B : Type*} [CommRing R] [CommRing T] [CommRing B]
    [Algebra R K] [IsFractionRing R K] [Algebra R L] [IsScalarTower R K L]
    (E : IntermediateField K L) [Algebra R E] [IsScalarTower R K E]
    [Algebra R T] [Algebra T E] [IsScalarTower R T E] [IsIntegralClosure T R E]
    [Algebra R B] [Algebra B L] [IsScalarTower R B L] [IsIntegralClosure B R L]
    [Algebra T B] [IsScalarTower R T B] [Algebra T L]
    [IsScalarTower T E L] [IsScalarTower T B L] [Module.Finite R T]
    [MulSemiringAction (L ≃ₐ[K] L) B] [SMulCommClass (L ≃ₐ[K] L) R B]
    [SMulCommClass (↥E.fixingSubgroup) T B]
    {σ : L ≃ₐ[K] L} {τ : E.fixingSubgroup} {Q : Ideal B} [Q.IsPrime]
    (hR : IsArithFrobAt R σ Q) (hT : IsArithFrobAt T τ Q)
    (hbot : Q.inertia (L ≃ₐ[K] L) = ⊥) :
    (τ : L ≃ₐ[K] L) = σ ^ (Q.under T).inertiaDeg R
Uses 1
Proof usesFrobenius in a tower is a power of the base Frobenius

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.