Arithmetic Pic0 Galois trace vanishes over a rational quotient

Proved

MazurTransfer.RationalQuotientPicardGaloisTrace.pic0_galois_trace_eq_zero

by Vas · Oct 17, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-geometryarithmetic-geometrymazur-theorem

With the original field and scalar-tower structures, let E/F be finite Galois and assume HasPrincipalDivisors K E. A specified K-algebra equivalence K(t) to F makes the sum of the F-Galois conjugates of any arithmetic Pic0(K,E) class equal to zero. Every original hypothesis and universe is retained.

Preamble

/-
Copyright (c) 2026 Vas and contributors. Released under Apache-2.0.
Original Pic0 Galois-trace proof retained, using its public principal-divisor input.
Design boundary: the sum of Galois conjugates of any arithmetic degree-zero
Picard class vanishes over a specified rational quotient field.
Named downstream consumer: finite-subgroup and cyclic Pic0 trace.
Official Anthropic FLT divisor interfaces at
6e837e75355538c7f80bab5b956861e86c4eacc2, Apache-2.0.
-/
import Theorems.Thm_MazurTransfer_RationalQuotientPicardGaloisTrace_degree_zero_galois_trace_principal
noncomputable section
universe u v w
open AlgebraicCurve MazurTransfer.RationalQuotientPicardGaloisTrace

Formal statement

theorem MazurTransfer.RationalQuotientPicardGaloisTrace.pic0_galois_trace_eq_zero
    {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
    {E : Type w} [Field E] [Algebra K E] [Algebra F E]
    [IsScalarTower K F E] [FiniteDimensional F E] [IsGalois F E]
    [HasPrincipalDivisors K E] (e : RatFunc K ≃ₐ[K] F) (c : Pic0 K E) :
    ∑ σ : E ≃ₐ[F] E, (σ.restrictScalars K) • c = 0 := by sorry

Source

Unchanged complete original MazurTheorem RationalQuotientPicardGaloisTrace.pic0_galois_trace_eq_zero proof and statement; official Anthropic FLT divisor and quotient interfaces at 6e837e75355538c7f80bab5b956861e86c4eacc2, Apache-2.0.

View graph