Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Merged by Bors] - chore(Analysis/Normed/Ring/WithAbs): make equiv a ring equiv #20713

Closed
wants to merge 4 commits into from
Closed

[Merged by Bors] - chore(Analysis/Normed/Ring/WithAbs): make equiv a ring equiv #20713

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
77fd5db
chore(Analysis/Normed/Ring/WithAbs): make equiv a ring equiv
MichaelStollBayreuth Jan 13, 2025
97ef8d3
fix NumberTheory.NumberField.InfinitePlace
MichaelStollBayreuth Jan 13, 2025
8be87f7
put def etc. in separate section
MichaelStollBayreuth Jan 13, 2025
1127cf4
typo, docstring
MichaelStollBayreuth Jan 13, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
65 changes: 35 additions & 30 deletions Mathlib/Analysis/Normed/Ring/WithAbs.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,9 @@ open Topology

noncomputable section

variable {R S K : Type*} [Semiring R] [OrderedSemiring S] [Field K]
section definition

variable {R R' S K : Type*} [Semiring R] [Ring R'] [OrderedSemiring S] [Field K]

/-- Type synonym for a semiring which depends on an absolute value. This is a function that takes
an absolute value on a semiring and returns the semiring. We use this to assign and infer instances
Expand All @@ -40,67 +42,68 @@ def WithAbs : AbsoluteValue R S → Type _ := fun _ => R

namespace WithAbs

variable (v : AbsoluteValue R ℝ)

/-- Canonical equivalence between `WithAbs v` and `R`. -/
def equiv : WithAbs v ≃ R := Equiv.refl (WithAbs v)
variable (v : AbsoluteValue R ℝ) (v' : AbsoluteValue R' ℝ)

instance instNonTrivial [Nontrivial R] : Nontrivial (WithAbs v) := inferInstanceAs (Nontrivial R)

instance instUnique [Unique R] : Unique (WithAbs v) := inferInstanceAs (Unique R)

instance instSemiring : Semiring (WithAbs v) := inferInstanceAs (Semiring R)

instance instRing [Ring R] : Ring (WithAbs v) := inferInstanceAs (Ring R)
instance instRing : Ring (WithAbs v') := inferInstanceAs (Ring R')

instance instInhabited : Inhabited (WithAbs v) := ⟨0⟩

instance normedRing {R : Type*} [Ring R] (v : AbsoluteValue R ℝ) : NormedRing (WithAbs v) :=
v.toNormedRing
/-- The canonical (semiring) equivalence between `WithAbs v` and `R`. -/
def equiv : WithAbs v ≃+* R := RingEquiv.refl _

instance normedRing : NormedRing (WithAbs v') :=
v'.toNormedRing

instance normedField (v : AbsoluteValue K ℝ) : NormedField (WithAbs v) :=
v.toNormedField

/-! `WithAbs.equiv` preserves the ring structure. -/
variable (x y : WithAbs v) (r s : R) (x' y' : WithAbs v') (r' s' : R')

variable (x y : WithAbs v) (r s : R)
@[simp]
theorem equiv_zero : WithAbs.equiv v 0 = 0 := rfl
@[deprecated "Use map_zero" (since := "2025-01-13"), simp]
theorem equiv_zero : equiv v 0 = 0 := rfl

@[simp]
theorem equiv_symm_zero : (WithAbs.equiv v).symm 0 = 0 := rfl
@[deprecated "Use map_zero" (since := "2025-01-13"), simp]
theorem equiv_symm_zero : (equiv v).symm 0 = 0 := rfl

@[simp]
theorem equiv_add : WithAbs.equiv v (x + y) = WithAbs.equiv v x + WithAbs.equiv v y := rfl
@[deprecated "Use map_add" (since := "2025-01-13"), simp]
theorem equiv_add : equiv v (x + y) = equiv v x + equiv v y := rfl

@[simp]
@[deprecated "Use map_add" (since := "2025-01-13"), simp]
theorem equiv_symm_add :
(WithAbs.equiv v).symm (r + s) = (WithAbs.equiv v).symm r + (WithAbs.equiv v).symm s :=
(equiv v).symm (r + s) = (equiv v).symm r + (equiv v).symm s :=
rfl

@[simp]
theorem equiv_sub [Ring R] : WithAbs.equiv v (x - y) = WithAbs.equiv v x - WithAbs.equiv v y := rfl
@[deprecated "Use map_sub" (since := "2025-01-13"), simp]
theorem equiv_sub : equiv v' (x' - y') = equiv v' x' - equiv v' y' := rfl

@[simp]
theorem equiv_symm_sub [Ring R] :
(WithAbs.equiv v).symm (r - s) = (WithAbs.equiv v).symm r - (WithAbs.equiv v).symm s :=
@[deprecated "Use map_sub" (since := "2025-01-13"), simp]
theorem equiv_symm_sub :
(equiv v').symm (r' - s') = (equiv v').symm r' - (equiv v').symm s' :=
rfl

@[simp]
theorem equiv_neg [Ring R] : WithAbs.equiv v (-x) = - WithAbs.equiv v x := rfl
@[deprecated "Use map_neg" (since := "2025-01-13"), simp]
theorem equiv_neg : equiv v' (-x') = - equiv v' x' := rfl

@[simp]
theorem equiv_symm_neg [Ring R] : (WithAbs.equiv v).symm (-r) = - (WithAbs.equiv v).symm r := rfl
@[deprecated "Use map_neg" (since := "2025-01-13"), simp]
theorem equiv_symm_neg : (equiv v').symm (-r') = - (equiv v').symm r' := rfl

@[simp]
theorem equiv_mul : WithAbs.equiv v (x * y) = WithAbs.equiv v x * WithAbs.equiv v y := rfl
@[deprecated "Use map_mul" (since := "2025-01-13"), simp]
theorem equiv_mul : equiv v (x * y) = equiv v x * equiv v y := rfl

@[simp]
@[deprecated "Use map_mul" (since := "2025-01-13"), simp]
theorem equiv_symm_mul :
(WithAbs.equiv v).symm (x * y) = (WithAbs.equiv v).symm x * (WithAbs.equiv v).symm y :=
(equiv v).symm (x * y) = (equiv v).symm x * (equiv v).symm y :=
rfl

/-- `WithAbs.equiv` as a ring equivalence. -/
@[deprecated equiv (since := "2025-01-13")]
def ringEquiv : WithAbs v ≃+* R := RingEquiv.refl _

/-! The completion of a field at an absolute value. -/
Expand Down Expand Up @@ -134,6 +137,8 @@ theorem isUniformInducing_of_comp (h : ∀ x, ‖f x‖ = v x) : IsUniformInduci

end WithAbs

end definition

namespace AbsoluteValue

open WithAbs
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/NumberTheory/NumberField/Completion.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -83,7 +83,7 @@ instance : Algebra K v.Completion :=
lemma WithAbs.ratCast_equiv (v : InfinitePlace ℚ) (x : WithAbs v.1) :
Rat.cast (WithAbs.equiv _ x) = (x : v.Completion) :=
(eq_ratCast (UniformSpace.Completion.coeRingHom.comp
(WithAbs.ringEquiv v.1).symm.toRingHom) x).symm
(WithAbs.equiv v.1).symm.toRingHom) x).symm

lemma Rat.norm_infinitePlace_completion (v : InfinitePlace ℚ) (x : ℚ) :
‖(x : v.Completion)‖ = |x| := by
Expand Down
Loading