NYLL
Module

PlaceEquiv.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.NumberField.PlaceEquiv
2 declarations indexed from sourceView source ↗

Module documentation

Places under a number-field equivalence

A field equivalence bijects both the finite and infinite places. These equivalences reindex placewise products without changing their mathematics.

Imports3
  • Mathlib.NumberTheory.NumberField.Basic
  • Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
  • Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Imported by3

Declarations

def

finitePlaceEquivOfRingEquiv

L28 ↗
ClassFieldTheory.finitePlaceEquivOfRingEquiv
Documentation

Finite places correspond via the induced equivalence of rings of integers.

Source context 5 commands

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

noncomputable section
open scoped NumberField
open NumberField IsDedekindDomain
namespace ClassFieldTheory
universe u v
Lean source · statement
def finitePlaceEquivOfRingEquiv
    {F : Type u} {G : Type v} [Field F] [Field G]
    [NumberField F] [NumberField G] (e : F ≃+* G) :
    HeightOneSpectrum (𝓞 F) ≃ HeightOneSpectrum (𝓞 G)
def

infinitePlaceEquivOfRingEquiv

L37 ↗
ClassFieldTheory.infinitePlaceEquivOfRingEquiv
Documentation

Infinite places correspond by pulling embeddings back along the inverse field equivalence.

Source context 5 commands

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

noncomputable section
open scoped NumberField
open NumberField IsDedekindDomain
namespace ClassFieldTheory
universe u v
Lean source · full declaration
def infinitePlaceEquivOfRingEquiv
    {F : Type u} {G : Type v} [Field F] [Field G]
    (e : F ≃+* G) :
    NumberField.InfinitePlace F ≃ NumberField.InfinitePlace G where
  toFun w := w.comap e.symm.toRingHom
  invFun w := w.comap e.toRingHom
  left_inv w := by
    change (w.comap e.symm.toRingHom).comap e.toRingHom = w
    rw [← NumberField.InfinitePlace.comap_comp]
    have hcomp : e.symm.toRingHom.comp e.toRingHom = RingHom.id F := by
      ext x
      simp
    rw [hcomp, NumberField.InfinitePlace.comap_id]
  right_inv w := by
    change (w.comap e.toRingHom).comap e.symm.toRingHom = w
    rw [← NumberField.InfinitePlace.comap_comp]
    have hcomp : e.toRingHom.comp e.symm.toRingHom = RingHom.id G := by
      ext x
      simp
    rw [hcomp, NumberField.InfinitePlace.comap_id]

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