NYLL
Module

Compat_Mathlib430.lean

Nyll.AlgebraicCurves.Foundations.Compatibility.Compat_Mathlib430
45 declarations indexed from sourceView source ↗

Module documentation

Block A — Mathlib v4.30.0 Mathlib/RepresentationTheory/Basic.lean:391-419 (section

MulAction), names suffixed Finsupp

Block B — Mathlib v4.30.0 Mathlib/RepresentationTheory/Basic.lean:472-483 (section Group)

Block C — Mathlib v4.30.0 Mathlib/RepresentationTheory/Rep/Basic.lean:336-346 and

404-412, names suffixed Finsupp

Block D — AddAut: Mathlib v4.30.0 Mathlib/Algebra/Group/End.lean:746-801 (+

GroupWithZero/Action/Basic.lean:89-92 and :104-112, Ring/AddAut.lean:32), lemma names primed

Block D (continued) — Mathlib v4.30.0

Mathlib/Algebra/GroupWithZero/Action/Basic.lean:104-112: the tautological DistribMulAction (AddAut A) A (AddAut.applyDistribMulAction, its smul_def and apply_faithfulSMul), dropped in v4.33.0 together with the multiplicative structure; vendored with primed names on top of the Group instance above.

Block E — elliptic (divisibility) sequence predicates: Mathlib v4.30.0

Mathlib/NumberTheory/EllipticDivisibilitySequence.lean:78-110 (verbatim; names primed). Vendored because Mathlib v4.33.0 (db584cd6, same file :286-295) RENAMED AND REDEFINED them (IsEllipticSequence W := ∀ p q r, IsEllipticNet.rel W p q r 0 = 0, IsDvdSequence over ℤ instead of ℕ) and kept the 4.30 names only as deprecated aliases of the NEW predicates.

Block F — notation α ^+ M for FixedPoints.addSubgroup M α: Mathlib v4.30.0

Mathlib/Algebra/Ring/Action/Submonoid.lean:43 (verbatim). Mathlib v4.33.0 removed the notation line; the definition itself is unchanged, so re-declaring the notation keeps every tree statement that uses it textually and semantically identical.

Block G — ramification/inertia cardinality lemmas under the separability hypothesis

(adapted from Mathlib v4.30.0, Mathlib/NumberTheory/RamificationInertia/Galois.lean; v4.33.0 restates them assuming PerfectField of the residue field). Theorems only, primed names; no definitions involved.

Imports10
  • Mathlib.RepresentationTheory.Rep.Basic
  • Mathlib.Algebra.Group.End
  • Mathlib.Algebra.GroupWithZero.Action.Basic
  • Mathlib.Algebra.Ring.AddAut
  • Mathlib.Algebra.Ring.Action.Submonoid
  • Mathlib.NumberTheory.RamificationInertia.Galois
  • Mathlib.RingTheory.Invariant.Galois
  • Mathlib.FieldTheory.Galois.Basic
  • Mathlib.Tactic.LinearCombination
  • Mathlib.Tactic.Ring
Imported by1

Declarations

def

ofMulActionFinsupp

L71 ↗
Representation.ofMulActionFinsupp
Documentation

The representation on finitely supported functions induced by the given action on their indices.

Source context 3 commands

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

namespace Representation
section MulAction
variable (k : Type*) [Semiring k] (G : Type*) [Monoid G] (H : Type*) [MulAction G H]
Lean source · full declaration
def ofMulActionFinsupp : Representation k G (H →₀ k) where
  toFun g := Finsupp.lmapDomain k k (g • ·)
  map_one' := by
    ext x y
    simp
  map_mul' x y := by
    ext z w
    simp [mul_smul]
abbrev

leftRegularFinsupp

L81 ↗
Representation.leftRegularFinsupp
Documentation

The left regular representation on finitely supported functions on the group.

Source context 3 commands

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

namespace Representation
section MulAction
variable (k : Type*) [Semiring k] (G : Type*) [Monoid G] (H : Type*) [MulAction G H]
Lean source · statement
abbrev leftRegularFinsupp
abbrev

diagonalFinsupp

L85 ↗
Representation.diagonalFinsupp
Documentation

The representation on finitely supported functions on tuples under the diagonal group action.

Source context 3 commands

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

namespace Representation
section MulAction
variable (k : Type*) [Semiring k] (G : Type*) [Monoid G] (H : Type*) [MulAction G H]
Lean source · statement
abbrev diagonalFinsupp (n : ℕ)
theorem

ofMulActionFinsupp_def

L89 ↗
Representation.ofMulActionFinsupp_def
Source context 4 commands

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

namespace Representation
section MulAction
variable (k : Type*) [Semiring k] (G : Type*) [Monoid G] (H : Type*) [MulAction G H]
variable {k G H}
Lean source · statement
theorem ofMulActionFinsupp_def (g : G) : ofMulActionFinsupp k G H g = Finsupp.lmapDomain k k (g •
  ·)
theorem

ofMulActionFinsupp_single

L93 ↗
Representation.ofMulActionFinsupp_single
Source context 4 commands

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

namespace Representation
section MulAction
variable (k : Type*) [Semiring k] (G : Type*) [Monoid G] (H : Type*) [MulAction G H]
variable {k G H}
Lean source · statement
theorem ofMulActionFinsupp_single (g : G) (x : H) (r : k) :
    ofMulActionFinsupp k G H g (Finsupp.single x r) = Finsupp.single (g • x) r
theorem

ofMulActionFinsupp_apply

L106 ↗
Representation.ofMulActionFinsupp_apply
Source context 3 commands

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

namespace Representation
section Group
variable {k G V : Type*} [Semiring k] [Group G] [AddCommMonoid V] [Module k V]
  (ρ : Representation k G V)
Lean source · statement
theorem ofMulActionFinsupp_apply {H : Type*} [MulAction G H] (g : G) (f : H →₀ k) (h : H) :
    ofMulActionFinsupp k G H g f h = f (g⁻¹ • h)
def

ofMulActionFinsuppEquiv

L125 ↗
Representation.ofMulActionFinsuppEquiv
Documentation

The equivalence between the finitely supported-function model and the monoid-algebra model of the action.

Source context 3 commands

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

namespace Representation
section Bridge
variable (k : Type*) [Semiring k] (G : Type*) [Monoid G] (H : Type*) [MulAction G H]
Lean source · statement
def ofMulActionFinsuppEquiv : (ofMulActionFinsupp k G H).Equiv (ofMulAction k G H)
abbrev

ofMulActionFinsupp

L152 ↗
Rep.ofMulActionFinsupp
Documentation

The representation object on finitely supported functions induced by the given action on their indices.

Source context 6 commands

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

namespace Rep
open CategoryTheory
universe w' u v
variable {k : Type u} {G : Type v} [Ring k] [Monoid G]
section
variable (k G)
Lean source · statement
abbrev ofMulActionFinsupp (H : Type w') [MulAction G H] : Rep k G
abbrev

leftRegularFinsupp

L157 ↗
Rep.leftRegularFinsupp
Documentation

The left regular representation object on finitely supported functions on the group.

Source context 6 commands

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

namespace Rep
open CategoryTheory
universe w' u v
variable {k : Type u} {G : Type v} [Ring k] [Monoid G]
section
variable (k G)
Lean source · statement
abbrev leftRegularFinsupp : Rep k G
abbrev

diagonalFinsupp

L163 ↗
Rep.diagonalFinsupp
Documentation

The representation object on finitely supported functions on tuples under the diagonal group action.

Source context 6 commands

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

namespace Rep
open CategoryTheory
universe w' u v
variable {k : Type u} {G : Type v} [Ring k] [Monoid G]
section
variable (k G)
Lean source · statement
abbrev diagonalFinsupp (n : ℕ) : Rep k G
def

ofMulActionFinsuppIso

L169 ↗
Rep.ofMulActionFinsuppIso
Documentation

The isomorphism between the finitely supported-function and monoid-algebra action representations.

Source context 6 commands

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

namespace Rep
open CategoryTheory
universe w' u v
variable {k : Type u} {G : Type v} [Ring k] [Monoid G]
section
variable (k G)
Lean source · statement
def ofMulActionFinsuppIso (H : Type w') [MulAction G H] :
    ofMulActionFinsupp k G H ≅ ofMulAction k G H
abbrev

leftRegularHomFinsupp

L177 ↗
Rep.leftRegularHomFinsupp
Documentation

The map from the left regular representation sending its identity basis vector to the chosen vector.

Source context 4 commands

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

namespace Rep
open CategoryTheory
universe w' u v
variable {k : Type u} {G : Type v} [Ring k] [Monoid G]
Lean source · statement
abbrev leftRegularHomFinsupp (A : Rep k G) (x : A) : leftRegularFinsupp k G ⟶ A
theorem

leftRegularHomFinsupp_hom_single

L181 ↗
Rep.leftRegularHomFinsupp_hom_single
Source context 4 commands

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

namespace Rep
open CategoryTheory
universe w' u v
variable {k : Type u} {G : Type v} [Ring k] [Monoid G]
Lean source · statement
theorem leftRegularHomFinsupp_hom_single {A : Rep k G} (g : G) (x : A) (r : k) :
    (leftRegularHomFinsupp A x).hom (.single g r) = r • A.ρ g x
instance

(anonymous instance)

L196 ↗
Source context 3 commands

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

namespace AddAut
section Compat430
variable (A : Type*) [Add A]
Lean source · full declaration
instance : Group (AddAut A) where
  mul g h := AddEquiv.trans h g
  one := AddEquiv.refl _
  inv := AddEquiv.symm
  mul_assoc _ _ _ := rfl
  one_mul _ := rfl
  mul_one _ := rfl
  inv_mul_cancel := AddEquiv.self_trans_symm
theorem

coe_mul'

L207 ↗
AddAut.coe_mul'
Source context 3 commands

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

namespace AddAut
section Compat430
variable (A : Type*) [Add A]
Lean source · statement
theorem coe_mul' (e₁ e₂ : AddAut A) : ⇑(e₁ * e₂) = e₁ ∘ e₂
theorem

coe_one'

L210 ↗
AddAut.coe_one'
Source context 3 commands

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

namespace AddAut
section Compat430
variable (A : Type*) [Add A]
Lean source · statement
theorem coe_one' : ⇑(1 : AddAut A) = id
theorem

coe_inv'

L213 ↗
AddAut.coe_inv'
Source context 3 commands

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

namespace AddAut
section Compat430
variable (A : Type*) [Add A]
Lean source · statement
theorem coe_inv' (e : AddAut A) : ⇑e⁻¹ = e.symm
theorem

mul_def'

L215 ↗
AddAut.mul_def'
Source context 3 commands

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

namespace AddAut
section Compat430
variable (A : Type*) [Add A]
Lean source · statement
theorem mul_def' (e₁ e₂ : AddAut A) : e₁ * e₂ = e₂.trans e₁
theorem

one_def'

L218 ↗
AddAut.one_def'
Source context 3 commands

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

namespace AddAut
section Compat430
variable (A : Type*) [Add A]
Lean source · statement
theorem one_def' : (1 : AddAut A) = AddEquiv.refl _
theorem

inv_def'

L221 ↗
AddAut.inv_def'
Source context 3 commands

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

namespace AddAut
section Compat430
variable (A : Type*) [Add A]
Lean source · statement
theorem inv_def' (e₁ : AddAut A) : e₁⁻¹ = e₁.symm
theorem

mul_apply'

L224 ↗
AddAut.mul_apply'
Source context 3 commands

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

namespace AddAut
section Compat430
variable (A : Type*) [Add A]
Lean source · statement
theorem mul_apply' (e₁ e₂ : AddAut A) (a : A) : (e₁ * e₂) a = e₁ (e₂ a)
theorem

one_apply'

L227 ↗
AddAut.one_apply'
Source context 3 commands

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

namespace AddAut
section Compat430
variable (A : Type*) [Add A]
Lean source · statement
theorem one_apply' (a : A) : (1 : AddAut A) a = a
theorem

inv_symm'

L230 ↗
AddAut.inv_symm'
Source context 3 commands

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

namespace AddAut
section Compat430
variable (A : Type*) [Add A]
Lean source · statement
theorem inv_symm' (e : AddAut A) : e⁻¹.symm = e
theorem

symm_inv'

L232 ↗
AddAut.symm_inv'
Source context 3 commands

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

namespace AddAut
section Compat430
variable (A : Type*) [Add A]
Lean source · statement
theorem symm_inv' (e : AddAut A) : e.symm⁻¹ = e
theorem

inv_apply'

L234 ↗
AddAut.inv_apply'
Source context 3 commands

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

namespace AddAut
section Compat430
variable (A : Type*) [Add A]
Lean source · statement
theorem inv_apply' (e : AddAut A) (a : A) : e⁻¹ a = e.symm a
theorem

inv_apply_self'

L236 ↗
AddAut.inv_apply_self'
Source context 3 commands

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

namespace AddAut
section Compat430
variable (A : Type*) [Add A]
Lean source · statement
theorem inv_apply_self' (e : AddAut A) (a : A) : e⁻¹ (e a) = a
theorem

apply_inv_self'

L239 ↗
AddAut.apply_inv_self'
Source context 3 commands

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

namespace AddAut
section Compat430
variable (A : Type*) [Add A]
Lean source · statement
theorem apply_inv_self' (e : AddAut A) (a : A) : e (e⁻¹ a) = a
def

toAddAut'

L252 ↗
DistribMulAction.toAddAut'
Documentation

The homomorphism to additive automorphisms induced by a distributive group action.

Lean source · full declaration
def DistribMulAction.toAddAut' (G A : Type*) [Group G] [AddMonoid A] [DistribMulAction G A] :
    G →* AddAut A where
  toFun := DistribMulAction.toAddEquiv A
  map_one' := AddEquiv.ext (one_smul _)
  map_mul' _ _ := AddEquiv.ext (mul_smul _ _)
def

mulLeft'

L259 ↗
AddAut.mulLeft'
Documentation

The homomorphism sending a unit to the additive automorphism given by left multiplication.

Lean source · statement
def AddAut.mulLeft' {R : Type*} [Semiring R] : Rˣ →* AddAut R
instance

applyDistribMulAction'

L270 ↗
AddAut.applyDistribMulAction'
Source context 1 command

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

namespace AddAut
Lean source · full declaration
instance applyDistribMulAction' {A : Type*} [AddMonoid A] : DistribMulAction (AddAut A) A where
  smul := (· <| ·)
  one_smul _ := rfl
  mul_smul _ _ _ := rfl
  smul_zero := AddEquiv.map_zero
  smul_add := AddEquiv.map_add
theorem

smul_def'

L277 ↗
AddAut.smul_def'
Source context 1 command

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

namespace AddAut
Lean source · statement
theorem smul_def' {A : Type*} [AddMonoid A] (f : AddAut A) (a : A) : f • a = f a
instance

apply_faithfulSMul'

L280 ↗
AddAut.apply_faithfulSMul'
Source context 1 command

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

namespace AddAut
Lean source · statement
instance apply_faithfulSMul' {A : Type*} [AddMonoid A] : FaithfulSMul (AddAut A) A
def

IsEllSequence'

L301 ↗
Documentation

The elliptic-sequence identity for an integer-indexed sequence.

Source context 4 commands

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

section IsEllDivSequence430
universe u
variable {R : Type u} [CommRing R]
variable (W : ℤ → R)
Lean source · statement
def IsEllSequence' : Prop
def

IsDivSequence'

L306 ↗
Documentation

The divisibility condition on sequence values at divisible natural-number indices.

Source context 4 commands

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

section IsEllDivSequence430
universe u
variable {R : Type u} [CommRing R]
variable (W : ℤ → R)
Lean source · statement
def IsDivSequence' : Prop
def

IsEllDivSequence'

L310 ↗
Documentation

The conjunction of the elliptic-sequence and divisibility identities.

Source context 4 commands

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

section IsEllDivSequence430
universe u
variable {R : Type u} [CommRing R]
variable (W : ℤ → R)
Lean source · statement
def IsEllDivSequence' : Prop
lemma

isEllSequence'_id

L313 ↗
Source context 4 commands

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

section IsEllDivSequence430
universe u
variable {R : Type u} [CommRing R]
variable (W : ℤ → R)
Lean source · statement
lemma isEllSequence'_id : IsEllSequence' id
lemma

isDivSequence'_id

L316 ↗
Source context 4 commands

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

section IsEllDivSequence430
universe u
variable {R : Type u} [CommRing R]
variable (W : ℤ → R)
Lean source · statement
lemma isDivSequence'_id : IsDivSequence' id
theorem

isEllDivSequence'_id

L319 ↗
Source context 4 commands

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

section IsEllDivSequence430
universe u
variable {R : Type u} [CommRing R]
variable (W : ℤ → R)
Lean source · statement
theorem isEllDivSequence'_id : IsEllDivSequence' id
lemma

smul

L324 ↗
IsEllSequence'.smul
Source context 5 commands

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

section IsEllDivSequence430
universe u
variable {R : Type u} [CommRing R]
variable (W : ℤ → R)
variable {W}
Lean source · statement
lemma IsEllSequence'.smul (h : IsEllSequence' W) (x : R) : IsEllSequence' (x • W)
lemma

smul

L328 ↗
IsDivSequence'.smul
Source context 5 commands

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

section IsEllDivSequence430
universe u
variable {R : Type u} [CommRing R]
variable (W : ℤ → R)
variable {W}
Lean source · statement
lemma IsDivSequence'.smul (h : IsDivSequence' W) (x : R) : IsDivSequence' (x • W)
lemma

smul

L331 ↗
IsEllDivSequence'.smul
Source context 5 commands

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

section IsEllDivSequence430
universe u
variable {R : Type u} [CommRing R]
variable (W : ℤ → R)
variable {W}
Lean source · statement
lemma IsEllDivSequence'.smul (h : IsEllDivSequence' W) (x : R) : IsEllDivSequence' (x • W)
theorem

card_stabilizer_eq_card_inertia_mul_finrank'

L363 ↗
Ideal.card_stabilizer_eq_card_inertia_mul_finrank'
Source context 6 commands

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

/-- The additive subgroup fixed by the action of the monoid. -/
notation α "^+" M:51 => FixedPoints.addSubgroup M α
namespace Ideal
section inertia430
variable {R S G : Type*} [CommRing R] [CommRing S] [Algebra R S] [Group G]
  [MulSemiringAction G S] [IsGaloisGroup G R S] [Finite G]
open scoped Pointwise
attribute [local instance] Ideal.Quotient.field in
Lean source · statement
theorem card_stabilizer_eq_card_inertia_mul_finrank' (p : Ideal R) [p.IsMaximal]
    (P : Ideal S) [P.LiesOver p] [P.IsMaximal] [Algebra.IsSeparable (R ⧸ p) (S ⧸ P)] :
    Nat.card (MulAction.stabilizer G P) = Nat.card (inertia G P) *
      Module.finrank (R ⧸ p) (S ⧸ P)
lemma

ncard_primesOver_mul_card_inertia_mul_finrank'

L376 ↗
Ideal.ncard_primesOver_mul_card_inertia_mul_finrank'
Source context 5 commands

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

/-- The additive subgroup fixed by the action of the monoid. -/
notation α "^+" M:51 => FixedPoints.addSubgroup M α
namespace Ideal
section inertia430
variable {R S G : Type*} [CommRing R] [CommRing S] [Algebra R S] [Group G]
  [MulSemiringAction G S] [IsGaloisGroup G R S] [Finite G]
open scoped Pointwise
Lean source · statement
lemma ncard_primesOver_mul_card_inertia_mul_finrank' (p : Ideal R) [p.IsMaximal]
    (P : Ideal S) [P.LiesOver p] [P.IsMaximal] [Algebra.IsSeparable (R ⧸ p) (S ⧸ P)] :
    (p.primesOver S).ncard * Nat.card (P.inertia G) *
      Module.finrank (R ⧸ p) (S ⧸ P) = Nat.card G
lemma

card_inertia_eq_ramificationIdxIn'

L385 ↗
Ideal.card_inertia_eq_ramificationIdxIn'
Source context 6 commands

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

/-- The additive subgroup fixed by the action of the monoid. -/
notation α "^+" M:51 => FixedPoints.addSubgroup M α
namespace Ideal
section inertia430
variable {R S G : Type*} [CommRing R] [CommRing S] [Algebra R S] [Group G]
  [MulSemiringAction G S] [IsGaloisGroup G R S] [Finite G]
open scoped Pointwise
attribute [local instance] Ideal.Quotient.field in
Lean source · statement
lemma card_inertia_eq_ramificationIdxIn'
    [IsDedekindDomain R] [IsDedekindDomain S] [Module.Finite R S]
    [Module.IsTorsionFree R S]
    (p : Ideal R) (hp : p ≠ ⊥)
    (P : Ideal S) [P.LiesOver p] [P.IsMaximal] [Algebra.IsSeparable (R ⧸ p) (S ⧸ P)] :
    Nat.card (P.inertia G) = Ideal.ramificationIdxIn p S
lemma

card_stabilizer_eq'

L401 ↗
Ideal.card_stabilizer_eq'
Source context 6 commands

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

/-- The additive subgroup fixed by the action of the monoid. -/
notation α "^+" M:51 => FixedPoints.addSubgroup M α
namespace Ideal
section inertia430
variable {R S G : Type*} [CommRing R] [CommRing S] [Algebra R S] [Group G]
  [MulSemiringAction G S] [IsGaloisGroup G R S] [Finite G]
open scoped Pointwise
attribute [local instance] Ideal.Quotient.field in
Lean source · statement
lemma card_stabilizer_eq' [IsDedekindDomain R] [IsDedekindDomain S] [Module.Finite R S]
    [Module.IsTorsionFree R S] (p : Ideal R) (hp : p ≠ ⊥) (P : Ideal S) [P.LiesOver p] [P.IsMaximal]
    [Algebra.IsSeparable (R ⧸ p) (S ⧸ P)] :
    Nat.card (MulAction.stabilizer G P) = p.ramificationIdxIn S * p.inertiaDegIn S

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