Documentation

TauCeti.RingTheory.ClassGroup.RelNorm

The relative norm on ideal class groups #

For a finite extension S / R of Dedekind domains, Mathlib's relative ideal norm Ideal.relNorm R : Ideal S →*₀ Ideal R is multiplicative and sends principal ideals to principal ideals (Ideal.relNorm_singleton), so it descends to a group homomorphism ClassGroup.relNorm : ClassGroup S →* ClassGroup R on ideal class groups.

The descent is along ClassGroup.mk0 : (Ideal S)⁰ →* ClassGroup S, which is surjective. Since (Ideal S)⁰ is a monoid rather than a group, MonoidHom.liftOfSurjective does not apply; the descent instead goes through the monoid congruence Con.ker and Con.quotientKerEquivOfSurjective.

Main definitions #

Main results #

Provenance #

Ported from the AINTLIB HasseWeil project (Apache-2.0), revision 513e83879e2f, file HasseWeil/Pic0/ClassGroupNorm.lean, declarations relNorm0, mk0CompRelNorm0, mk0CompRelNorm0_apply, mk0CompRelNorm0_eq_of_mk0_eq, ClassGroup.relNorm, ClassGroup.relNorm_mk0, ClassGroup.relNorm_mk0', ClassGroup.relNorm_comp_map and ClassGroup.relNorm_comp_map_eq.

Deviations from the source. It descends by Function.surjInv on ClassGroup.mk0_surjective, with Function.surjInv_eq rewrites discharging map_one' and map_mul'; the congruence route used here needs no choice plumbing in the proofs. It assumes IsDomain and IsIntegrallyClosed alongside IsDedekindDomain for both rings, which are implied. Its intermediate mk0CompRelNorm0 and that lemma's _apply are inlined, the well-definedness fact being stated directly about mk0 ∘ relNorm0. Finally its relNorm_mk0', a restatement of relNorm_mk0 with the membership proof spelled out inline, is not ported.

The source's extension direction is not ported at all. Its map0, mk0CompMap0, ClassGroup.map, ClassGroup.map_mk0, ClassGroup.map_one and ClassGroup.map_mul are Mathlib's ClassGroup.extendedIdeal, ClassGroup.extendedHom and ClassGroup.extendedHom_mk0 (Mathlib/RingTheory/ClassGroup/ExtendedHom.lean), which the pinned Mathlib already carries; the first version of this file duplicated them under the source's names and reuse blocked it. Its Ideal.relNorm_map_algebraMap is likewise not ported: it converts Ideal.relNorm_algebraMap's exponent from Module.finrank (FractionRing R) (FractionRing S) to Module.finrank R S, and the pinned Ideal.relNorm_algebraMap already concludes in the latter form, with the converting lemma finrank_of_isFractionRing now deprecated.

The composite is ported, not original. relNorm_extendedHom and relNorm_comp_extendedHom are the source's ClassGroup.relNorm_comp_map and ClassGroup.relNorm_comp_map_eq, respelt so that the extension direction is Mathlib's ClassGroup.extendedHom rather than the source's own ClassGroup.map. What is new here is only that respelling and the shape of the proof: the source reaches the ideal level inline, by congrArg ClassGroup.mk0, Subtype.ext and a change, landing on its own Ideal.relNorm_map_algebraMap; this file names that step as Ideal.relNorm0_extendedIdeal and lands on Mathlib's Ideal.relNorm_algebraMap directly, no exponent conversion being needed. The composite is nonetheless new relative to Mathlib, since it needs ClassGroup.relNorm, which Mathlib does not carry.

source
noncomputable def Ideal.relNorm0 (R : Type u_1) {S : Type u_2} [CommRing R] [CommRing S] [IsDedekindDomain R] [IsDedekindDomain S] [Algebra R S] [Module.Finite R S] [Module.IsTorsionFree R S] :
↥(nonZeroDivisors (Ideal S)) →* ↥(nonZeroDivisors (Ideal R))

The relative ideal norm restricted to nonzero ideals, using that it reflects ⊥ (Ideal.relNorm_eq_bot_iff).

Equations
Instances For
    source
    @[simp]
    theorem Ideal.coe_relNorm0 {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDedekindDomain R] [IsDedekindDomain S] [Algebra R S] [Module.Finite R S] [Module.IsTorsionFree R S] (I : ↥(nonZeroDivisors (Ideal S))) :
    ↑((relNorm0 R) I) = (relNorm R) ↑I
    source
    @[simp]
    theorem Ideal.relNorm0_extendedIdeal {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDedekindDomain R] [IsDedekindDomain S] [Algebra R S] [Module.Finite R S] [Module.IsTorsionFree R S] (I : ↥(nonZeroDivisors (Ideal R))) :
    (relNorm0 R) (ClassGroup.extendedIdeal R S I) = I ^ Module.finrank R S

    Norm of an extended ideal is the finrank-th power, on nonzero ideals: the (Ideal R)⁰-level form of Mathlib's Ideal.relNorm_algebraMap, against Mathlib's ClassGroup.extendedIdeal.

    source
    noncomputable def ClassGroup.relNorm {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDedekindDomain R] [IsDedekindDomain S] [Algebra R S] [Module.Finite R S] [Module.IsTorsionFree R S] :
    ClassGroup S →* ClassGroup R

    The relative norm on class groups, induced by Ideal.relNorm.

    Every class has an integral representative, since ClassGroup.mk0 is surjective, and the class of the norm does not depend on the representative; ClassGroup.relNorm_mk0 is the resulting computation.

    Equations
    Instances For
      source
      @[simp]
      theorem ClassGroup.relNorm_mk0 {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDedekindDomain R] [IsDedekindDomain S] [Algebra R S] [Module.Finite R S] [Module.IsTorsionFree R S] (I : ↥(nonZeroDivisors (Ideal S))) :
      relNorm (mk0 I) = mk0 ((Ideal.relNorm0 R) I)

      The relative norm of the class represented by a nonzero ideal I is the class represented by I's relative norm. This is the computation rule for ClassGroup.relNorm.

      source
      @[simp]
      theorem ClassGroup.relNorm_extendedHom {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDedekindDomain R] [IsDedekindDomain S] [Algebra R S] [Module.Finite R S] [Module.IsTorsionFree R S] (c : ClassGroup R) :
      relNorm ((extendedHom R S) c) = c ^ Module.finrank R S

      Extending a class and taking its relative norm raises it to the finrank-th power.

      The extension direction is Mathlib's ClassGroup.extendedHom; the arithmetic is Mathlib's Ideal.relNorm_algebraMap, which needs no separability, Galois or perfect-field hypothesis, so neither does this. The composite is the source's ClassGroup.relNorm_comp_map; see the module's Provenance.

      source
      theorem ClassGroup.relNorm_comp_extendedHom {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDedekindDomain R] [IsDedekindDomain S] [Algebra R S] [Module.Finite R S] [Module.IsTorsionFree R S] :
      relNorm.comp (extendedHom R S) = powMonoidHom (Module.finrank R S)

      ClassGroup.relNorm_extendedHom as an identity of monoid homomorphisms: the composite relNorm ∘ extendedHom is the finrank-th power map on ClassGroup R.