NYLL
Module

FinrankPrimePow.lean

Nyll.AlgebraicCurves.Places.FinrankPrimePow
17 declarations indexed from sourceView source ↗

Module documentation

A warning-free compatibility proof for the finrank of a prime-power quotient.

This is the filtration argument formerly bundled with the legacy NumberTheory.RamificationInertia.Basic module. It is kept in a project namespace so the remaining place trace/norm proofs can use the current split ramification imports.

Imports4
  • Mathlib.LinearAlgebra.Dimension.DivisionRing
  • Mathlib.NumberTheory.RamificationInertia.Inertia
  • Mathlib.NumberTheory.RamificationInertia.Ramification
  • Mathlib.RingTheory.Ideal.Norm.AbsNorm
Imported by5

Declarations

instance

algebraQuotientPowRamificationIdx

L48 ↗
AlgebraicCurves.Compat.FinrankPrimePow.CompatQuotient.algebraQuotientPowRamificationIdx
Documentation

R / p has a canonical map to S / (P ^ e), where e is the ramification index of P over p.

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace AlgebraicCurves.Compat.FinrankPrimePow
universe u v
variable {R : Type u} [CommRing R]
variable {S : Type v} [CommRing S] [Algebra R S]
variable (p : Ideal R) (P : Ideal S)
local notation "f" => algebraMap R S
open Module
open UniqueFactorizationMonoid
open Ideal
attribute [local instance] Ideal.Quotient.field
section FactLeComap
local notation "e" => ramificationIdx' p P
Lean source · statement
instance CompatQuotient.algebraQuotientPowRamificationIdx :
    Algebra (R ⧸ p) (S ⧸ P ^ e)
theorem

algebraMap_quotient_pow_ramificationIdx

L52 ↗
AlgebraicCurves.Compat.FinrankPrimePow.CompatQuotient.algebraMap_quotient_pow_ramificationIdx
Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace AlgebraicCurves.Compat.FinrankPrimePow
universe u v
variable {R : Type u} [CommRing R]
variable {S : Type v} [CommRing S] [Algebra R S]
variable (p : Ideal R) (P : Ideal S)
local notation "f" => algebraMap R S
open Module
open UniqueFactorizationMonoid
open Ideal
attribute [local instance] Ideal.Quotient.field
section FactLeComap
local notation "e" => ramificationIdx' p P
Lean source · statement
theorem CompatQuotient.algebraMap_quotient_pow_ramificationIdx (x : R) :
    algebraMap (R ⧸ p) (S ⧸ P ^ e) (Ideal.Quotient.mk p x) = Ideal.Quotient.mk (P ^ e) (f x)
def

algebraQuotientOfRamificationIdxNeZero

L59 ↗
AlgebraicCurves.Compat.FinrankPrimePow.CompatQuotient.algebraQuotientOfRamificationIdxNeZero
Documentation

If P lies over p, then R / p has a canonical map to S / P.

This can't be an instance since the map f : R → S is generally not inferable.

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace AlgebraicCurves.Compat.FinrankPrimePow
universe u v
variable {R : Type u} [CommRing R]
variable {S : Type v} [CommRing S] [Algebra R S]
variable (p : Ideal R) (P : Ideal S)
local notation "f" => algebraMap R S
open Module
open UniqueFactorizationMonoid
open Ideal
attribute [local instance] Ideal.Quotient.field
section FactLeComap
local notation "e" => ramificationIdx' p P
Lean source · statement
def CompatQuotient.algebraQuotientOfRamificationIdxNeZero [hfp : NeZero e] :
    Algebra (R ⧸ p) (S ⧸ P)
theorem

algebraMap_quotient_of_ramificationIdx_neZero

L66 ↗
AlgebraicCurves.Compat.FinrankPrimePow.CompatQuotient.algebraMap_quotient_of_ramificationIdx_neZero
Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace AlgebraicCurves.Compat.FinrankPrimePow
universe u v
variable {R : Type u} [CommRing R]
variable {S : Type v} [CommRing S] [Algebra R S]
variable (p : Ideal R) (P : Ideal S)
local notation "f" => algebraMap R S
open Module
open UniqueFactorizationMonoid
open Ideal
attribute [local instance] Ideal.Quotient.field
section FactLeComap
local notation "e" => ramificationIdx' p P
attribute [local instance] CompatQuotient.algebraQuotientOfRamificationIdxNeZero
Lean source · statement
theorem CompatQuotient.algebraMap_quotient_of_ramificationIdx_neZero
    [NeZero e] (x : R) :
    algebraMap (R ⧸ p) (S ⧸ P) (Ideal.Quotient.mk p x) = Ideal.Quotient.mk P (f x)
def

powQuotSuccInclusion

L71 ↗
AlgebraicCurves.Compat.FinrankPrimePow.powQuotSuccInclusion
Documentation

The inclusion (P^(i + 1) / P^e) ⊂ (P^i / P^e).

Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace AlgebraicCurves.Compat.FinrankPrimePow
universe u v
variable {R : Type u} [CommRing R]
variable {S : Type v} [CommRing S] [Algebra R S]
variable (p : Ideal R) (P : Ideal S)
local notation "f" => algebraMap R S
open Module
open UniqueFactorizationMonoid
open Ideal
attribute [local instance] Ideal.Quotient.field
section FactLeComap
local notation "e" => ramificationIdx' p P
attribute [local instance] CompatQuotient.algebraQuotientOfRamificationIdxNeZero
Lean source · full declaration
def powQuotSuccInclusion (i : ℕ) :
    Ideal.map (Ideal.Quotient.mk (P ^ e)) (P ^ (i + 1)) →ₗ[R ⧸ p]
    Ideal.map (Ideal.Quotient.mk (P ^ e)) (P ^ i) where
  toFun x := ⟨x, Ideal.map_mono (Ideal.pow_le_pow_right i.le_succ) x.2⟩
  map_add' _ _ := rfl
  map_smul' _ _ := rfl
theorem

powQuotSuccInclusion_injective

L78 ↗
AlgebraicCurves.Compat.FinrankPrimePow.powQuotSuccInclusion_injective
Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace AlgebraicCurves.Compat.FinrankPrimePow
universe u v
variable {R : Type u} [CommRing R]
variable {S : Type v} [CommRing S] [Algebra R S]
variable (p : Ideal R) (P : Ideal S)
local notation "f" => algebraMap R S
open Module
open UniqueFactorizationMonoid
open Ideal
attribute [local instance] Ideal.Quotient.field
section FactLeComap
local notation "e" => ramificationIdx' p P
attribute [local instance] CompatQuotient.algebraQuotientOfRamificationIdxNeZero
Lean source · statement
theorem powQuotSuccInclusion_injective (i : ℕ) :
    Function.Injective (powQuotSuccInclusion p P i)
def

quotientToQuotientRangePowQuotSuccAux

L87 ↗
AlgebraicCurves.Compat.FinrankPrimePow.quotientToQuotientRangePowQuotSuccAux
Documentation

S ⧸ P embeds into the quotient by P^(i+1) ⧸ P^e as a subspace of P^i ⧸ P^e. See quotientToQuotientRangePowQuotSucc for this as a linear map, and quotientRangePowQuotSuccInclusionEquiv for this as a linear equivalence.

Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace AlgebraicCurves.Compat.FinrankPrimePow
universe u v
variable {R : Type u} [CommRing R]
variable {S : Type v} [CommRing S] [Algebra R S]
variable (p : Ideal R) (P : Ideal S)
local notation "f" => algebraMap R S
open Module
open UniqueFactorizationMonoid
open Ideal
attribute [local instance] Ideal.Quotient.field
section FactLeComap
local notation "e" => ramificationIdx' p P
attribute [local instance] CompatQuotient.algebraQuotientOfRamificationIdxNeZero
Lean source · statement
def quotientToQuotientRangePowQuotSuccAux {i : ℕ} {a : S} (a_mem : a ∈ P ^ i) :
    S ⧸ P →
      (P ^ i).map (Ideal.Quotient.mk (P ^ e)) ⧸ LinearMap.range (powQuotSuccInclusion p P i)
theorem

quotientToQuotientRangePowQuotSuccAux_mk

L99 ↗
AlgebraicCurves.Compat.FinrankPrimePow.quotientToQuotientRangePowQuotSuccAux_mk
Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace AlgebraicCurves.Compat.FinrankPrimePow
universe u v
variable {R : Type u} [CommRing R]
variable {S : Type v} [CommRing S] [Algebra R S]
variable (p : Ideal R) (P : Ideal S)
local notation "f" => algebraMap R S
open Module
open UniqueFactorizationMonoid
open Ideal
attribute [local instance] Ideal.Quotient.field
section FactLeComap
local notation "e" => ramificationIdx' p P
attribute [local instance] CompatQuotient.algebraQuotientOfRamificationIdxNeZero
Lean source · statement
theorem quotientToQuotientRangePowQuotSuccAux_mk {i : ℕ} {a : S} (a_mem : a ∈ P ^ i) (x : S) :
    quotientToQuotientRangePowQuotSuccAux p P a_mem (Submodule.Quotient.mk x) =
      Submodule.Quotient.mk ⟨_, Ideal.mem_map_of_mem _ (Ideal.mul_mem_right x _ a_mem)⟩
def

quotientToQuotientRangePowQuotSucc

L108 ↗
AlgebraicCurves.Compat.FinrankPrimePow.quotientToQuotientRangePowQuotSucc
Documentation

S ⧸ P embeds into the quotient by P^(i+1) ⧸ P^e as a subspace of P^i ⧸ P^e.

Source context 15 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace AlgebraicCurves.Compat.FinrankPrimePow
universe u v
variable {R : Type u} [CommRing R]
variable {S : Type v} [CommRing S] [Algebra R S]
variable (p : Ideal R) (P : Ideal S)
local notation "f" => algebraMap R S
open Module
open UniqueFactorizationMonoid
open Ideal
attribute [local instance] Ideal.Quotient.field
section FactLeComap
local notation "e" => ramificationIdx' p P
attribute [local instance] CompatQuotient.algebraQuotientOfRamificationIdxNeZero
section
variable [hfp : NeZero (ramificationIdx' p P)]
Lean source · full declaration
def quotientToQuotientRangePowQuotSucc
    {i : ℕ} {a : S} (a_mem : a ∈ P ^ i) :
    S ⧸ P →ₗ[R ⧸ p]
      (P ^ i).map (Ideal.Quotient.mk (P ^ e)) ⧸ LinearMap.range (powQuotSuccInclusion p P i) where
  toFun := quotientToQuotientRangePowQuotSuccAux p P a_mem
  map_add' x y := by
    induction x, y using Quotient.inductionOn₂' with | _ x y
    simp only [Submodule.Quotient.mk''_eq_mk, ← Submodule.Quotient.mk_add,
      quotientToQuotientRangePowQuotSuccAux_mk, mul_add, map_add, map_mul, AddMemClass.mk_add_mk]
  map_smul' x y := by
    induction x, y using Quotient.inductionOn₂' with | _ x y
    simp only [Submodule.Quotient.mk''_eq_mk, RingHom.id_apply,
      quotientToQuotientRangePowQuotSuccAux_mk]
    refine congr_arg Submodule.Quotient.mk ?_
    ext
    simp only [map_mul, Quotient.mk_eq_mk, Submodule.coe_smul_of_tower,
      Algebra.smul_def, CompatQuotient.algebraMap_quotient_pow_ramificationIdx]
    ring
theorem

quotientToQuotientRangePowQuotSucc_mk

L127 ↗
AlgebraicCurves.Compat.FinrankPrimePow.quotientToQuotientRangePowQuotSucc_mk
Source context 15 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace AlgebraicCurves.Compat.FinrankPrimePow
universe u v
variable {R : Type u} [CommRing R]
variable {S : Type v} [CommRing S] [Algebra R S]
variable (p : Ideal R) (P : Ideal S)
local notation "f" => algebraMap R S
open Module
open UniqueFactorizationMonoid
open Ideal
attribute [local instance] Ideal.Quotient.field
section FactLeComap
local notation "e" => ramificationIdx' p P
attribute [local instance] CompatQuotient.algebraQuotientOfRamificationIdxNeZero
section
variable [hfp : NeZero (ramificationIdx' p P)]
Lean source · statement
theorem quotientToQuotientRangePowQuotSucc_mk {i : ℕ} {a : S} (a_mem : a ∈ P ^ i) (x : S) :
    quotientToQuotientRangePowQuotSucc p P a_mem (Submodule.Quotient.mk x) =
      Submodule.Quotient.mk ⟨_, Ideal.mem_map_of_mem _ (Ideal.mul_mem_right x _ a_mem)⟩
theorem

quotientToQuotientRangePowQuotSucc_injective

L132 ↗
AlgebraicCurves.Compat.FinrankPrimePow.quotientToQuotientRangePowQuotSucc_injective
Source context 15 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace AlgebraicCurves.Compat.FinrankPrimePow
universe u v
variable {R : Type u} [CommRing R]
variable {S : Type v} [CommRing S] [Algebra R S]
variable (p : Ideal R) (P : Ideal S)
local notation "f" => algebraMap R S
open Module
open UniqueFactorizationMonoid
open Ideal
attribute [local instance] Ideal.Quotient.field
section FactLeComap
local notation "e" => ramificationIdx' p P
attribute [local instance] CompatQuotient.algebraQuotientOfRamificationIdxNeZero
section
variable [hfp : NeZero (ramificationIdx' p P)]
Lean source · statement
theorem quotientToQuotientRangePowQuotSucc_injective [IsDedekindDomain S] [P.IsPrime]
    {i : ℕ} (hi : i < e) {a : S} (a_mem : a ∈ P ^ i) (a_notMem : a ∉ P ^ (i + 1)) :
    Function.Injective (quotientToQuotientRangePowQuotSucc p P a_mem)
theorem

quotientToQuotientRangePowQuotSucc_surjective

L151 ↗
AlgebraicCurves.Compat.FinrankPrimePow.quotientToQuotientRangePowQuotSucc_surjective
Source context 15 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace AlgebraicCurves.Compat.FinrankPrimePow
universe u v
variable {R : Type u} [CommRing R]
variable {S : Type v} [CommRing S] [Algebra R S]
variable (p : Ideal R) (P : Ideal S)
local notation "f" => algebraMap R S
open Module
open UniqueFactorizationMonoid
open Ideal
attribute [local instance] Ideal.Quotient.field
section FactLeComap
local notation "e" => ramificationIdx' p P
attribute [local instance] CompatQuotient.algebraQuotientOfRamificationIdxNeZero
section
variable [hfp : NeZero (ramificationIdx' p P)]
Lean source · statement
theorem quotientToQuotientRangePowQuotSucc_surjective [IsDedekindDomain S]
    (hP0 : P ≠ ⊥) [hP : P.IsPrime] {i : ℕ} (hi : i < e) {a : S} (a_mem : a ∈ P ^ i)
    (a_notMem : a ∉ P ^ (i + 1)) :
    Function.Surjective (quotientToQuotientRangePowQuotSucc p P a_mem)
def

quotientRangePowQuotSuccInclusionEquiv

L176 ↗
AlgebraicCurves.Compat.FinrankPrimePow.quotientRangePowQuotSuccInclusionEquiv
Documentation

Quotienting P^i / P^e by its subspace P^(i+1) ⧸ P^e is R ⧸ p-linearly isomorphic to S ⧸ P.

Source context 15 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace AlgebraicCurves.Compat.FinrankPrimePow
universe u v
variable {R : Type u} [CommRing R]
variable {S : Type v} [CommRing S] [Algebra R S]
variable (p : Ideal R) (P : Ideal S)
local notation "f" => algebraMap R S
open Module
open UniqueFactorizationMonoid
open Ideal
attribute [local instance] Ideal.Quotient.field
section FactLeComap
local notation "e" => ramificationIdx' p P
attribute [local instance] CompatQuotient.algebraQuotientOfRamificationIdxNeZero
section
variable [hfp : NeZero (ramificationIdx' p P)]
Lean source · statement
def quotientRangePowQuotSuccInclusionEquiv [IsDedekindDomain S]
    [P.IsPrime] (hP : P ≠ ⊥) {i : ℕ} (hi : i < e) :
    ((P ^ i).map (Ideal.Quotient.mk (P ^ e)) ⧸ LinearMap.range (powQuotSuccInclusion p P i))
      ≃ₗ[R ⧸ p] S ⧸ P
theorem

rank_pow_quot_aux

L190 ↗
AlgebraicCurves.Compat.FinrankPrimePow.rank_pow_quot_aux
Documentation

Since the inclusion (P^(i + 1) / P^e) ⊂ (P^i / P^e) has a kernel isomorphic to P / S, [P^i / P^e : R / p] = [P^(i+1) / P^e : R / p] + [P / S : R / p]

Source context 15 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace AlgebraicCurves.Compat.FinrankPrimePow
universe u v
variable {R : Type u} [CommRing R]
variable {S : Type v} [CommRing S] [Algebra R S]
variable (p : Ideal R) (P : Ideal S)
local notation "f" => algebraMap R S
open Module
open UniqueFactorizationMonoid
open Ideal
attribute [local instance] Ideal.Quotient.field
section FactLeComap
local notation "e" => ramificationIdx' p P
attribute [local instance] CompatQuotient.algebraQuotientOfRamificationIdxNeZero
section
variable [hfp : NeZero (ramificationIdx' p P)]
Lean source · statement
theorem rank_pow_quot_aux [IsDedekindDomain S] [p.IsMaximal] [P.IsPrime] (hP0 : P ≠ ⊥)
    {i : ℕ} (hi : i < e) :
    Module.rank (R ⧸ p) (Ideal.map (Ideal.Quotient.mk (P ^ e)) (P ^ i)) =
      Module.rank (R ⧸ p) (S ⧸ P) +
        Module.rank (R ⧸ p) (Ideal.map (Ideal.Quotient.mk (P ^ e)) (P ^ (i + 1)))
theorem

rank_pow_quot

L199 ↗
AlgebraicCurves.Compat.FinrankPrimePow.rank_pow_quot
Source context 15 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace AlgebraicCurves.Compat.FinrankPrimePow
universe u v
variable {R : Type u} [CommRing R]
variable {S : Type v} [CommRing S] [Algebra R S]
variable (p : Ideal R) (P : Ideal S)
local notation "f" => algebraMap R S
open Module
open UniqueFactorizationMonoid
open Ideal
attribute [local instance] Ideal.Quotient.field
section FactLeComap
local notation "e" => ramificationIdx' p P
attribute [local instance] CompatQuotient.algebraQuotientOfRamificationIdxNeZero
section
variable [hfp : NeZero (ramificationIdx' p P)]
Lean source · statement
theorem rank_pow_quot [IsDedekindDomain S] [p.IsMaximal] [P.IsPrime] (hP0 : P ≠ ⊥)
    (i : ℕ) (hi : i ≤ e) :
    Module.rank (R ⧸ p) (Ideal.map (Ideal.Quotient.mk (P ^ e)) (P ^ i)) =
      (e - i) • Module.rank (R ⧸ p) (S ⧸ P)
theorem

rank_prime_pow_ramificationIdx

L219 ↗
AlgebraicCurves.Compat.FinrankPrimePow.rank_prime_pow_ramificationIdx
Documentation

If p is a maximal ideal of R, S extends R and P^e lies over p, then the dimension [S/(P^e) : R/p] is equal to e * [S/P : R/p].

Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace AlgebraicCurves.Compat.FinrankPrimePow
universe u v
variable {R : Type u} [CommRing R]
variable {S : Type v} [CommRing S] [Algebra R S]
variable (p : Ideal R) (P : Ideal S)
local notation "f" => algebraMap R S
open Module
open UniqueFactorizationMonoid
open Ideal
attribute [local instance] Ideal.Quotient.field
section FactLeComap
local notation "e" => ramificationIdx' p P
attribute [local instance] CompatQuotient.algebraQuotientOfRamificationIdxNeZero
Lean source · statement
theorem rank_prime_pow_ramificationIdx [IsDedekindDomain S] [p.IsMaximal] [P.IsPrime]
    (hP0 : P ≠ ⊥) (he : e ≠ 0) :
    Module.rank (R ⧸ p) (S ⧸ P ^ e) =
      e •
        @Module.rank (R ⧸ p) (S ⧸ P) _ _
          (@Algebra.toModule _ _ _ _ <|
            @CompatQuotient.algebraQuotientOfRamificationIdxNeZero _ _ _ _ _ _ _ ⟨he⟩)
theorem

finrank_prime_pow_ramificationIdx

L233 ↗
AlgebraicCurves.Compat.FinrankPrimePow.finrank_prime_pow_ramificationIdx
Documentation

If p is a maximal ideal of R, S extends R and P^e lies over p, then the dimension [S/(P^e) : R/p], as a natural number, is equal to e * [S/P : R/p].

Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace AlgebraicCurves.Compat.FinrankPrimePow
universe u v
variable {R : Type u} [CommRing R]
variable {S : Type v} [CommRing S] [Algebra R S]
variable (p : Ideal R) (P : Ideal S)
local notation "f" => algebraMap R S
open Module
open UniqueFactorizationMonoid
open Ideal
attribute [local instance] Ideal.Quotient.field
section FactLeComap
local notation "e" => ramificationIdx' p P
attribute [local instance] CompatQuotient.algebraQuotientOfRamificationIdxNeZero
Lean source · statement
theorem finrank_prime_pow_ramificationIdx [IsDedekindDomain S] (hP0 : P ≠ ⊥)
    [p.IsMaximal] [P.IsPrime] (he : e ≠ 0) :
    finrank (R ⧸ p) (S ⧸ P ^ e) =
      e *
        @finrank (R ⧸ p) (S ⧸ P) _ _
          (@Algebra.toModule _ _ _ _ <|
            @CompatQuotient.algebraQuotientOfRamificationIdxNeZero _ _ _ _ _ _ _ ⟨he⟩)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.