ArithmeticLifts.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Uniform lifts of a nonzero line modulo a prime square

The reduction map has exactly p lifts over every residue. A line with a unit coefficient has exactly p zero lifts among the p² pairs over a fixed solution modulo p. This is the relative 1/p loss in §8.

def OAI.Ostmann.additiveFiberEquiv line 18

Source documentation

Translate an additive fiber to the zero fiber.

def additiveFiberEquiv {G H : Type*} [AddGroup G] [AddGroup H]
    (φ : G →+ H) (x : G) : {y : G // φ y = φ x} ≃ {y : G // φ y = 0} where
…

theorem OAI.Ostmann.card_additiveFiber line 27

Source documentation

Every fiber of a surjective homomorphism between finite additive groups has the same size.

theorem card_additiveFiber {G H : Type*} [AddGroup G] [AddGroup H]
    [Fintype G] [Fintype H] [DecidableEq H]
    (φ : G →+ H) (hφ : Function.Surjective φ) (a : H) :
    Fintype.card G = Fintype.card H * Fintype.card {y : G // φ y = a} := by
…

def OAI.Ostmann.squareReduction line 43
Source documentation
The actual reduction map modulo a prime.
```
def squareReduction (p : ℕ) : ZMod (p ^ 2) →+* ZMod p :=
…
```
theorem OAI.Ostmann.squareReduction_natCast line 46
theorem OAI.Ostmann.card_squareReduction_fiber line 49
theorem OAI.Ostmann.isUnit_square_iff line 57
Source documentation
A prime-square residue is a unit exactly when its reduction is nonzero.
```
theorem isUnit_square_iff {p : ℕ} [Fact p.Prime] (x : ZMod (p ^ 2)) :
    IsUnit x ↔ squareReduction p x ≠ 0 := by
…
```
Mentions: OAI.Ostmann.squareReduction
def OAI.Ostmann.squareUnitLiftEquiv line 74
Source documentation
Above a nonzero residue every lift is a unit; passing to Haar-unit coordinates leaves the same p uniformly weighted lifts.
```
noncomputable def squareUnitLiftEquiv {p : ℕ} [Fact p.Prime]
    (a : ZMod p) (ha : a ≠ 0) :
    {u : (ZMod (p ^ 2))ˣ // squareReduction p u = a} ≃
      {x : ZMod (p ^ 2) // squareReduction p x = a} where
…
```
Mentions: OAI.Ostmann.squareReduction
theorem OAI.Ostmann.card_squareUnitLift line 95

theorem OAI.Ostmann.square_line_first_isUnit line 101

Source documentation

In both giant environments the second residue is a unit. A nonzero row vanishing there must have a unit first coefficient.

theorem square_line_first_isUnit {p : ℕ} [Fact p.Prime]
    (a b : ZMod (p ^ 2)) (x₀ y₀ : ZMod p) (hy : y₀ ≠ 0)
    (hrow : squareReduction p a ≠ 0 ∨ squareReduction p b ≠ 0)
    (hbase : squareReduction p a * x₀ + squareReduction p b * y₀ = 0) :
    IsUnit a := by
…

Mentions: OAI.Ostmann.squareReduction

theorem OAI.Ostmann.unit_linear_solution line 111

def OAI.Ostmann.liftedLineEquiv line 120

Source documentation

A line with a unit first coefficient has one zero lift for each lift of the second coordinate, over any fixed solution in the quotient.

def liftedLineEquiv {R K : Type*} [CommRing R] [CommRing K]
    (φ : R →+* K) (a : Rˣ) (b : R) (x₀ y₀ : K)
    (hbase : φ a * x₀ + φ b * y₀ = 0) :
    {xy : R × R // φ xy.1 = x₀ ∧ φ xy.2 = y₀ ∧ (a : R) * xy.1 + b * xy.2 = 0} ≃
      {y : R // φ y = y₀} where
…

theorem OAI.Ostmann.square_line_lift_probability line 141

Source documentation

Exactly one out of p uniform pairs of lifts makes the line vanish modulo p², conditional on its vanishing modulo p.

theorem square_line_lift_probability {p : ℕ} [Fact p.Prime]
    (a : (ZMod (p ^ 2))ˣ) (b : ZMod (p ^ 2)) (x₀ y₀ : ZMod p)
    (hbase : squareReduction p a * x₀ + squareReduction p b * y₀ = 0) :
    (Fintype.card {xy : ZMod (p ^ 2) × ZMod (p ^ 2) //
      squareReduction p xy.1 = x₀ ∧ squareReduction p xy.2 = y₀ ∧
        (a : ZMod (p ^ 2)) * xy.1 + b * xy.2 = 0} : ℝ) /
    ((Fintype.card {x : ZMod (p ^ 2) // squareReduction p x = x₀} : ℝ) *
      (Fintype.card {y : ZMod (p ^ 2) // squareReduction p y = y₀} : ℝ)) =
      (p : ℝ)⁻¹ := by
…

Mentions: OAI.Ostmann.squareReduction