Third-review corrections; family corollary; autoImplicit off

- exists_companion_family: the all-lambda family, derived from exists_companion
  by choice, guarded in Axioms.lean.
- Statement is identified as the finite-extension companion-existence slice of
  Lafforgue VII.6(v), not the whole theorem; the affine model is restated as
  scope rather than shortfall.
- Corrections to Deligne numbering, Chebotarev conjugacy classes, Khare-Rajan
  and Ramakrishna scope, the Chin/Drinfeld monodromy attribution, the
  companion-matrix and Kummer paragraphs, and the etale-site inventory.
- CI attestation described accurately; instance claim in AUDIT corrected;
  known Mathlib idiom gaps recorded.
- autoImplicit = false; untrack Aristotle archive.

Author: SuvirRathore

.gitignore

@@ -1,3 +1,4 @@
 /.lake
 
 result.tar.gz
+*.tar.gz

AUDIT.md

@@ -31,9 +31,11 @@ but no tie-in to a curve. Unramifiedness predicates exist, but nothing for a
 representation.
 
 Missing: `π₁^ét(X)` for schemes. The Galois-category development is abstract,
-with finite `G`-sets as its only worked instance, and although the big étale site
-exists as a Grothendieck topology on schemes, the finite étale site is not
-instantiated as a Galois category. This decided the `G_K`-based formulation.
+with finite `G`-sets as its only worked instance. Both the big étale site and the
+small one, on the category of schemes étale over `X`, exist as Grothendieck
+topologies in `AlgebraicGeometry/Sites/Etale.lean`. What is absent is the finite
+étale subcategory, a fibre functor on it, and the Galois-category instance
+joining the two developments. This decided the `G_K`-based formulation.
 Chebotarev density is absent entirely, as is characteristic-polynomial
 coefficient descent to `E`.
 
@@ -64,13 +66,18 @@ elements at a place are conjugate, when in fact two lifts at the same prime
 differ by an element of inertia; it was deleted and replaced by the correct
 inertia argument. The companion statement was false as first written, since a
 rank-one unramified character of the constant-field quotient has Frobenius
-eigenvalues outside `E`, and irreducibility, finite-order determinant and
-`E`-rationality of the Frobenius characteristic polynomials are all required.
+eigenvalues outside `E`. Absolute irreducibility, finite-order determinant and
+`E`-rationality of the Frobenius characteristic polynomials were all added. The
+first two are Lafforgue's own hypotheses; the third is an artefact of fixing `E`
+in advance here, where Lafforgue obtains the number field as part of the theorem.
+None of the three is necessary for a compatible system to exist, since reducible
+ones do.
 Once those hypotheses were added the statement was still stronger than the
 theorem it named, in two independent ways. The conclusion placed companions over
-`E_λ` itself, where Lafforgue's theorem produces them over an algebraic closure
-and descent to `E_λ` for a fixed `E` is obstructed by the Schur index in
-`Br(E_λ)`. The irreducibility hypothesis was irreducibility over `E_λ`, which is
+`E_λ` itself, where Theorem VII.6(v) gives the companion over a finite extension
+of `E_λ` and descent to `E_λ` for a fixed `E` is obstructed by the class of a
+central simple algebra in `Br(E_λ)`. Chin's theorem is the stronger uniform
+coefficient-field descent, available after enlarging `E`. The irreducibility hypothesis was irreducibility over `E_λ`, which is
 weaker than absolute irreducibility, so using it strengthened the theorem. Both
 had been filed as limitations, which reads as having proved less when the truth
 was that it asserted more.
@@ -83,7 +90,12 @@ with the right fraction field, and fields and discrete valuation rings qualify,
 so the place set could be empty or a single point. The conclusion was then
 satisfiable cheaply, since the roots of the prescribed polynomial are `λ`-adic
 units, `GL_n(O_λ)` is profinite and `Ẑ` is procyclic, so a companion-matrix
-representation of the constant-field quotient satisfies everything. Requiring the
+representation of the constant-field quotient satisfies everything. What made
+that sufficient is that the conclusion of the version in question imposed no
+irreducibility on the members of the family. It would not satisfy the present
+conclusion: a representation factoring through a procyclic group has image
+generated by a single matrix `C`, so its span lies in `M[C]` and has dimension at
+most `n`, short of the `n²` that `SpanFull` demands once `n > 1`. Requiring the
 base ring to be a finite-type algebra over the constant field makes its spectrum
 a smooth affine curve carrying cofinitely many of the places, and closes this.
 
@@ -92,8 +104,8 @@ Three claims were described as doing more than they do.
 compatibility condition, which needs inertia rather than conjugacy, and a
 docstring continued to assert that claim, and to cite the deleted axiom, after
 the code had been corrected. Unit-ness of the Frobenius roots was attributed to
-purity, when it is part (c) of Deligne's Conjecture 1.2.10, proved for curves by
-Lafforgue, and a conclusion separate from the weight condition; `(3 + 4i)/5` has
+purity, when it is part (iii) of Deligne's Conjecture 1.2.10, labelled (c) in
+Drinfeld's abbreviated restatement, proved for curves by Lafforgue, and a conclusion separate from the weight condition; `(3 + 4i)/5` has
 absolute value `1` at every archimedean place and is not a `5`-adic unit. The
 equivalence between the span condition and absolute irreducibility was stated
 without its scope, which is a field and `n ≥ 1`.
@@ -110,31 +122,59 @@ hand-written versions were shadowing them. The claim came from an early survey
 and was repeated without reading the source. It survived every review, because a
 claim that something is missing from a library is not a mathematical claim and
 nothing in the reviews was aimed at that kind of claim. The instances are deleted
-and the file builds on Mathlib's.
+and the file builds on Mathlib's. A related inventory error in the same area, an
+undercount of what the étale-site file contains, was corrected at the same time;
+the conclusion it supported, that no `π₁^ét(X)` is available, survives.
 
 ## Why the unramifiedness hypothesis is not redundant
 
 It is tempting to drop it. Continuity forces the image into a compact subgroup of
 `GL_n(E_λ)`, which stabilises a lattice, so the representation modulo each power
 of the maximal ideal factors through a finite extension ramified at finitely many
 places. That gives a finite ramification set at every finite level, but the
-level-wise sets need not stabilise, and for `n ≥ 2` they need not. A Kummer class
-built from `b_m = ∏_{i ≤ m} π_i^{ℓ^i}` gives a continuous upper-triangular
+level-wise sets need not stabilise, and for `n ≥ 2` they need not. For
+`ℓ ≠ char K`, a Kummer class built from `b_m = ∏_{i ≤ m} π_i^{ℓ^i}`, with places
+`v_i` and elements `π_i` chosen so that `v_i(π_i) = 1` and each later `π_j` is a
+unit at the earlier `v_i`, gives a continuous upper-triangular
 `ρ = (χ_ℓ, c; 0, 1) : G_K → GL₂(ℤ_ℓ)` ramified at every `v_i`. Ramakrishna,
 *Infinitely ramified Galois representations*, Ann. of Math. 151 (2000), 793–815,
-shows that even full image is compatible with infinite ramification;
-Khare–Rajan, Int. Math. Res. Not. 2001, no. 12, 601–607, show the ramified set
-has density zero but can still be infinite. For `n = 1` the claim is true, since
-the torsion of `1 + 𝔪` is finite and class field theory closes the argument. This
-is why finite ramification is an explicit condition in the Fontaine–Mazur
-conjecture rather than a consequence of continuity, and it is why the hypothesis
-is stated here.
+constructs over `ℚ` surjective `GL₂(ℤ_ℓ)`-valued representations ramified at
+infinitely many primes, so even full image is compatible with infinite
+ramification;
+Khare–Rajan, Int. Math. Res. Not. 2001, no. 12, 601–607, show that for continuous
+semisimple representations of the absolute Galois group of a number field the
+ramified set has density zero while remaining possibly infinite, and remark that
+the same holds over function fields when the coefficient residue characteristic
+differs from the field characteristic. Semisimplicity is essential there; the
+Kummer representations above are not semisimple. For `n = 1` the claim is true,
+since the torsion of `1 + 𝔪` is finite and class field theory closes the
+argument.
+
+The example settles continuity alone. It does not show the hypothesis independent
+of the others: the representation displayed is reducible, so it fails `SpanFull`,
+and its determinant `χ_ℓ` has infinite order. Whether continuity together with
+absolute irreducibility and finite-order determinant forces finite ramification is
+not settled here. The hypothesis is stated because nothing available establishes
+that it can be dropped, which is also why finite ramification is an explicit
+condition in the Fontaine–Mazur conjecture rather than a consequence of
+continuity.
 
 ## What is not machine-checked
 
 Compile status and the axiom profile are checked in CI; see `Axioms.lean` and
-`.github/workflows/build.yml`. No instances are declared here, so the instance
-diamond an earlier version created no longer arises.
+`.github/workflows/build.yml`. The axiom check covers the declarations named
+there and their dependency closures; a `sorry` in a declaration outside those
+would not be caught, since `lake build` exits successfully on the warning it
+emits. No instances are declared on types Mathlib owns, so the diamond an earlier
+version created no longer arises; the five instances declared here are the
+projections of `CompanionRep`, whose carrier is defined here.
+
+Three notions defined here have close Mathlib counterparts that are not used.
+`LambdaAdicRep` is a `ContinuousMonoidHom`; the recurring conjunction
+`Q.IsPrime ∧ Q.under A = v.asIdeal` restates `Ideal.LiesOver`, the idiom
+`RingTheory/Frobenius.lean` itself uses; and `Field.absoluteGaloisGroup` is the
+fixed-closure form of `AbsGal`. Each is equivalent to what is written, and each
+would be the better choice in a version aimed at upstreaming.
 
 Lafforgue's Theorem VII.6 and Deligne's Conjecture 1.2.10 were verified through
 Drinfeld's verbatim quotations and bibliography rather than the originals. The

Axioms.lean

@@ -1,7 +1,7 @@
 /-
 Machine-checked attestation of the axiom profile. `lake env lean Axioms.lean`
 fails if any proved lemma acquires an axiom dependency, or if the companion
-theorem stops depending on `sorryAx` — that is, if the single deliberate `sorry`
+theorems stop depending on `sorryAx` — that is, if the single deliberate `sorry`
 silently moves or multiplies. Run in CI.
 -/
 import LambdaAdicSlice.Companions
@@ -35,3 +35,8 @@ import LambdaAdicSlice.Companions
 [propext, sorryAx, Classical.choice, Quot.sound] -/
 #guard_msgs (whitespace := lax) in
 #print axioms LambdaAdicSlice.exists_companion
+
+/-- info: 'LambdaAdicSlice.exists_companion_family' depends on axioms:
+[propext, sorryAx, Classical.choice, Quot.sound] -/
+#guard_msgs (whitespace := lax) in
+#print axioms LambdaAdicSlice.exists_companion_family

LambdaAdicSlice/Companions.lean

@@ -21,9 +21,14 @@ namespace LambdaAdicSlice
 
 section Setup
 
--- `A` is a Dedekind domain with fraction field `K`; the finite places of `K`
--- are the height-one primes of `A`. This covers number fields (`A = 𝓞 K`) and
--- function fields of curves over finite fields alike.
+-- `A` is a Dedekind domain with fraction field `K`. Its height-one primes are the
+-- places carried by the chosen model: for `A = 𝓞 K` they are the finite places of
+-- a number field, and for a finite-type Dedekind model of a function field they
+-- are the closed points of the corresponding affine curve, hence all but finitely
+-- many places of the proper curve. For an arbitrary Dedekind subring they are
+-- neither, since Mathlib's `IsDedekindDomain` admits localisations, discrete
+-- valuation rings and fields. `exists_companion` imposes the finite-type
+-- hypothesis that pins this down.
 variable (A K : Type*) [CommRing A] [IsDedekindDomain A] [Field K]
   [Algebra A K] [IsFractionRing A K]
 
@@ -80,8 +85,9 @@ omit [IsAlgClosure K Kbar] in
 of `g`.
 
 This is not the well-definedness fact behind the compatible-family
-condition. Two Frobenius elements at the same place need not be conjugate: they
-differ by an element of inertia. The correct argument is
+condition. Two Frobenius elements at the same prime `Q` above a place need not be
+conjugate: they differ by an element of the inertia at `Q`. Across different
+primes above one place, a conjugation moves the prime first. The correct argument is
 `toHom_eq_of_isArithFrobAt` below, which runs through `Ideal.inertia`. An
 earlier version of this file asserted the conjugacy statement as an axiom and
 described this lemma as establishing well-definedness; both were wrong. -/
@@ -319,10 +325,10 @@ into `GL_n(M)` for some finite extension `M` of `E_λ`, carrying the `E_λ`-modu
 topology.
 
 The coefficient field is bundled because Lafforgue's theorem does not produce
-companions over `E_λ` itself — it produces them over an algebraic closure, and
-descent to `E_λ` for a *fixed* `E` is false in general (a Schur-index obstruction
-in `Br(E_λ)`). Descent to a finite extension is elementary; descent to `E_λ`
-after enlarging `E` is Chin's theorem and is not formalised here.
+companions over `E_λ` itself. Theorem VII.6(v) states the companion over a finite
+extension of `E_λ`, and the obstruction to descending further for a fixed `E` is
+the class of a central simple algebra, which Lafforgue's own proof works with.
+Removing it by enlarging `E` is Chin's theorem, and is not formalised here.
 
 The topology is pinned by `IsModuleTopology`, not left arbitrary: an unspecified
 topology would make `Continuous` meaningless. -/
@@ -353,7 +359,15 @@ variable (A K Kbar : Type*) [CommRing A] [IsDedekindDomain A] [Field K]
   [Algebra A Kbar] [IsScalarTower A K Kbar]
 variable (E : Type*) [Field E] [NumberField E] (n : ℕ)
 
-/-- **Lafforgue's companion theorem for curves**, stated one place `λ` at a time.
+/-- The finite-extension companion-existence consequence of Lafforgue's Theorem
+VII.6(v), after fixing the coefficient field `E` and an `E_{λ₀}`-model, stated one
+place `λ` at a time.
+
+This is a slice of VII.6, not the whole of it. VII.6 begins from an irreducible
+lisse sheaf of finite-order determinant and constructs `E` and the polynomials
+`P_v`; here both are supplied as data. VII.6 also proves purity, integrality of
+the Frobenius roots, and a further descent statement, none of which is
+formalised.
 
 `A` is a finite-type Dedekind `𝔽_q`-algebra with fraction field the function
 field `K`, so `Spec A` is a smooth affine curve over `𝔽_q` and its closed points
@@ -373,9 +387,11 @@ varies).
 Conclusion: a companion over a finite extension of `E_λ`, unramified outside `S`,
 with the same `P v`, itself absolutely irreducible with finite-order determinant.
 
-Deliberately not formalised: `HeightOneSpectrum A` omits the places of the proper
-curve outside `Spec A`, so "unramified outside `S`" does not constrain those; and
-there is no claim that the coefficient field can be taken to be `E_λ`.
+The curve here is the smooth affine `U = Spec A` with `S` removed, to which
+VII.6 applies directly. The places of a proper model lying outside `Spec A` are
+not points of `U`, so nothing is claimed about them; that is a statement of scope,
+not a shortfall. What is deliberately not formalised is any descent of the
+coefficient field to `E_λ`.
 
 Statement only: the proof is `sorry`. -/
 theorem exists_companion
@@ -412,6 +428,62 @@ theorem exists_companion
 
 end Companions
 
+section CompanionFamily
+
+variable (A K Kbar : Type*) [CommRing A] [IsDedekindDomain A] [Field K]
+  [Algebra A K] [IsFractionRing A K]
+  [Field Kbar] [Algebra K Kbar] [IsAlgClosure K Kbar]
+  [Algebra A Kbar] [IsScalarTower A K Kbar]
+variable (E : Type*) [Field E] [NumberField E] (n : ℕ)
+
+/-- The whole family of companions, one for each finite place of `E` away from
+the characteristic, obtained from `exists_companion` by choice.
+
+Same hypotheses as `exists_companion` with the target place removed. The choice
+function assigns to each `λ` with `ℓ(λ) ≠ char K` a companion over its own finite
+extension of `E_λ`, all of them matching the one family of polynomials `P`. This
+is the Lean form of the statement that a family indexed by all `λ` follows from
+the one-place-at-a-time version; it is proved, not assumed, but inherits the
+`sorry` of `exists_companion`. -/
+theorem exists_companion_family
+    {Fq : Type*} [Field Fq] [Finite Fq]
+    [Algebra Fq A] [Algebra Fq K] [IsScalarTower Fq A K] [Algebra.FiniteType Fq A]
+    [Algebra (RatFunc Fq) K] [IsScalarTower Fq (RatFunc Fq) K]
+    (hK : FunctionField Fq K)
+    (hn : 0 < n)
+    (Frob : FrobeniusChoice A K Kbar)
+    (S : Finset (HeightOneSpectrum A))
+    (P : HeightOneSpectrum A → E[X])
+    {lam₀ : CoeffPlace E} (hchar₀ : resChar E lam₀ ≠ ringChar K)
+    (rho₀ : LambdaAdicRep K Kbar E n lam₀)
+    (hspan : SpanFull rho₀.toHom)
+    (hdet : DetFiniteOrderHom rho₀.toHom)
+    (hunram : ∀ v : HeightOneSpectrum A, v ∉ S →
+      IsUnramifiedAt A K Kbar E n rho₀ v)
+    (hrat : ∀ v : HeightOneSpectrum A, v ∉ S →
+      (rho₀.toHom (Frob.frob v) :
+          Matrix (Fin n) (Fin n) (Completion E lam₀)).charpoly
+        = (P v).map (algebraMap E (Completion E lam₀))) :
+    ∃ F : ∀ lam : CoeffPlace E, resChar E lam ≠ ringChar K →
+        CompanionRep K Kbar E n lam,
+      ∀ (lam : CoeffPlace E) (h : resChar E lam ≠ ringChar K),
+        (∀ v : HeightOneSpectrum A, v ∉ S →
+            ∀ Q : Ideal (IntClosure A Kbar), Q.IsPrime → Q.under A = v.asIdeal →
+              ∀ g : AbsGal K Kbar, g ∈ Q.inertia (AbsGal K Kbar) →
+                (F lam h).toHom g = 1) ∧
+        (∀ v : HeightOneSpectrum A, v ∉ S →
+            ((F lam h).toHom (Frob.frob v) :
+                Matrix (Fin n) (Fin n) (F lam h).M).charpoly
+              = (P v).map ((algebraMap (Completion E lam) (F lam h).M).comp
+                  (algebraMap E (Completion E lam)))) ∧
+        SpanFull (F lam h).toHom ∧ DetFiniteOrderHom (F lam h).toHom := by
+  choose F hF using fun (lam : CoeffPlace E) (h : resChar E lam ≠ ringChar K) =>
+    exists_companion A K Kbar E n hK hn Frob S P hchar₀ rho₀ hspan hdet hunram
+      hrat lam h
+  exact ⟨F, hF⟩
+
+end CompanionFamily
+
 section InertiaCorrect
 
 variable (A K Kbar : Type*) [CommRing A] [IsDedekindDomain A] [Field K]