Inverse operator for fractional ideals

This file defines the notation I⁻¹ where I is a not necessarily invertible fractional ideal. Note that this is somewhat misleading notation in case I is not invertible. The theorem that all nonzero fractional ideals are invertible in a Dedekind domain can be found in Mathlib/RingTheory/DedekindDomain/Ideal/Basic.lean.

Main definitions

• FractionalIdeal.instInv defines I⁻¹ := 1 / I.

References

• [D. Marcus, Number Fields][marcus1977number]
• [J.W.S. Cassels, A. Fröhlich, Algebraic Number Theory][cassels1967algebraic]
• [J. Neukirch, Algebraic Number Theory][Neukirch1992]

Tags

fractional ideal, invertible ideal

@[instance_reducible]

noncomputable instance FractionalIdeal.instInvNonZeroDivisors (K : Type u_1) [Field K] {R₁ : Type u_2} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] : Inv (FractionalIdeal (nonZeroDivisors R₁) K)

Equations

• FractionalIdeal.instInvNonZeroDivisors K = { inv := fun (I : FractionalIdeal (nonZeroDivisors R₁) K) => 1 / I }

theorem FractionalIdeal.inv_eq (K : Type u_1) [Field K] {R₁ : Type u_2} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] {I : FractionalIdeal (nonZeroDivisors R₁) K} : I⁻¹ = 1 / I

theorem FractionalIdeal.inv_zero' (K : Type u_1) [Field K] {R₁ : Type u_2} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] : 0⁻¹ = 0

theorem FractionalIdeal.inv_of_ne_zero (K : Type u_1) [Field K] {R₁ : Type u_2} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] {J : FractionalIdeal (nonZeroDivisors R₁) K} (h : J ≠ 0) : J⁻¹ = ⟨↑1 / ↑J, ⋯⟩

theorem FractionalIdeal.coe_inv_of_ne_zero (K : Type u_1) [Field K] {R₁ : Type u_2} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] {J : FractionalIdeal (nonZeroDivisors R₁) K} (h : J ≠ 0) : ↑J⁻¹ = IsLocalization.coeSubmodule K ⊤ / ↑J

theorem FractionalIdeal.mem_inv_iff {K : Type u_1} [Field K] {R₁ : Type u_2} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] {I : FractionalIdeal (nonZeroDivisors R₁) K} (hI : I ≠ 0) {x : K} : x ∈ I⁻¹ ↔ ∀ y ∈ I, x * y ∈ 1

theorem FractionalIdeal.inv_anti_mono {K : Type u_1} [Field K] {R₁ : Type u_2} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] {I J : FractionalIdeal (nonZeroDivisors R₁) K} (hI : I ≠ 0) (hJ : J ≠ 0) (hIJ : I ≤ J) : J⁻¹ ≤ I⁻¹

theorem FractionalIdeal.le_self_mul_inv {K : Type u_1} [Field K] {R₁ : Type u_2} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] {I : FractionalIdeal (nonZeroDivisors R₁) K} (hI : I ≤ 1) : I ≤ I * I⁻¹

theorem FractionalIdeal.coe_ideal_le_self_mul_inv (K : Type u_1) [Field K] {R₁ : Type u_2} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] (I : Ideal R₁) : ↑I ≤ ↑I * (↑I)⁻¹

theorem FractionalIdeal.right_inverse_eq (K : Type u_1) [Field K] {R₁ : Type u_2} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] (I J : FractionalIdeal (nonZeroDivisors R₁) K) (h : I * J = 1) : J = I⁻¹

I⁻¹ is the inverse of I if I has an inverse.

theorem FractionalIdeal.mul_inv_cancel_iff (K : Type u_1) [Field K] {R₁ : Type u_2} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] {I : FractionalIdeal (nonZeroDivisors R₁) K} : I * I⁻¹ = 1 ↔ ∃ (J : FractionalIdeal (nonZeroDivisors R₁) K), I * J = 1

theorem FractionalIdeal.mul_inv_cancel_iff_isUnit (K : Type u_1) [Field K] {R₁ : Type u_2} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] {I : FractionalIdeal (nonZeroDivisors R₁) K} : I * I⁻¹ = 1 ↔ IsUnit I

@[simp]

theorem FractionalIdeal.map_inv (K : Type u_1) [Field K] {R₁ : Type u_2} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] {K' : Type u_3} [Field K'] [Algebra R₁ K'] [IsFractionRing R₁ K'] (I : FractionalIdeal (nonZeroDivisors R₁) K) (h : K ≃ₐ[R₁] K') : map (↑h) I⁻¹ = (map (↑h) I)⁻¹

@[simp]

theorem FractionalIdeal.spanSingleton_inv (K : Type u_1) [Field K] {R₁ : Type u_2} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] (x : K) : ((spanSingleton (nonZeroDivisors R₁)) x)⁻¹ = (spanSingleton (nonZeroDivisors R₁)) x⁻¹

theorem FractionalIdeal.spanSingleton_div_spanSingleton (K : Type u_1) [Field K] {R₁ : Type u_2} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] (x y : K) : (spanSingleton (nonZeroDivisors R₁)) x / (spanSingleton (nonZeroDivisors R₁)) y = (spanSingleton (nonZeroDivisors R₁)) (x / y)

theorem FractionalIdeal.spanSingleton_div_self (K : Type u_1) [Field K] {R₁ : Type u_2} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] {x : K} (hx : x ≠ 0) : (spanSingleton (nonZeroDivisors R₁)) x / (spanSingleton (nonZeroDivisors R₁)) x = 1

theorem FractionalIdeal.coe_ideal_span_singleton_div_self (K : Type u_1) [Field K] {R₁ : Type u_2} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] {x : R₁} (hx : x ≠ 0) : ↑(Ideal.span {x}) / ↑(Ideal.span {x}) = 1

theorem FractionalIdeal.spanSingleton_mul_inv (K : Type u_1) [Field K] {R₁ : Type u_2} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] {x : K} (hx : x ≠ 0) : (spanSingleton (nonZeroDivisors R₁)) x * ((spanSingleton (nonZeroDivisors R₁)) x)⁻¹ = 1

theorem FractionalIdeal.coe_ideal_span_singleton_mul_inv (K : Type u_1) [Field K] {R₁ : Type u_2} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] {x : R₁} (hx : x ≠ 0) : ↑(Ideal.span {x}) * (↑(Ideal.span {x}))⁻¹ = 1

theorem FractionalIdeal.spanSingleton_inv_mul (K : Type u_1) [Field K] {R₁ : Type u_2} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] {x : K} (hx : x ≠ 0) : ((spanSingleton (nonZeroDivisors R₁)) x)⁻¹ * (spanSingleton (nonZeroDivisors R₁)) x = 1

theorem FractionalIdeal.coe_ideal_span_singleton_inv_mul (K : Type u_1) [Field K] {R₁ : Type u_2} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] {x : R₁} (hx : x ≠ 0) : (↑(Ideal.span {x}))⁻¹ * ↑(Ideal.span {x}) = 1

theorem FractionalIdeal.mul_generator_self_inv (K : Type u_1) [Field K] {R₁ : Type u_4} [CommRing R₁] [Algebra R₁ K] [IsLocalization (nonZeroDivisors R₁) K] (I : FractionalIdeal (nonZeroDivisors R₁) K) [(↑I).IsPrincipal] (h : I ≠ 0) : I * (spanSingleton (nonZeroDivisors R₁)) (Submodule.IsPrincipal.generator ↑I)⁻¹ = 1

theorem FractionalIdeal.invertible_of_principal (K : Type u_1) [Field K] {R₁ : Type u_2} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] (I : FractionalIdeal (nonZeroDivisors R₁) K) [(↑I).IsPrincipal] (h : I ≠ 0) : I * I⁻¹ = 1

theorem FractionalIdeal.invertible_iff_generator_nonzero (K : Type u_1) [Field K] {R₁ : Type u_2} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] (I : FractionalIdeal (nonZeroDivisors R₁) K) [(↑I).IsPrincipal] : I * I⁻¹ = 1 ↔ Submodule.IsPrincipal.generator ↑I ≠ 0

theorem FractionalIdeal.isPrincipal_inv (K : Type u_1) [Field K] {R₁ : Type u_2} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] (I : FractionalIdeal (nonZeroDivisors R₁) K) [(↑I).IsPrincipal] (h : I ≠ 0) : (↑I⁻¹).IsPrincipal

theorem FractionalIdeal.den_mem_inv {K : Type u_1} [Field K] {R₁ : Type u_2} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] {I : FractionalIdeal (nonZeroDivisors R₁) K} (hI : I ≠ ⊥) : (algebraMap R₁ K) ↑I.den ∈ I⁻¹

theorem FractionalIdeal.num_le_mul_inv {K : Type u_1} [Field K] {R₁ : Type u_2} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] (I : FractionalIdeal (nonZeroDivisors R₁) K) : ↑I.num ≤ I * I⁻¹

theorem FractionalIdeal.bot_lt_mul_inv {K : Type u_1} [Field K] {R₁ : Type u_2} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] {I : FractionalIdeal (nonZeroDivisors R₁) K} (hI : I ≠ ⊥) : ⊥ < I * I⁻¹

@[instance_reducible]

noncomputable instance FractionalIdeal.instInvOneClassNonZeroDivisors {K : Type u_1} [Field K] {R₁ : Type u_2} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] : InvOneClass (FractionalIdeal (nonZeroDivisors R₁) K)

Equations

• FractionalIdeal.instInvOneClassNonZeroDivisors = { toOne := FractionalIdeal.instOne, toInv := FractionalIdeal.instInvNonZeroDivisors K, inv_one := ⋯ }