Documentation

Mathlib.RingTheory.FractionalIdeal.Inverse

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/DedekindDomain/Ideal/Basic.lean.

Main definitions #

References #

Tags #

fractional ideal, invertible ideal

noncomputable instance FractionalIdeal.instInvNonZeroDivisors (K : Type u_3) [Field K] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] :
Equations
theorem FractionalIdeal.inv_eq (K : Type u_3) [Field K] {R₁ : Type u_4} [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_3) [Field K] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] :
0⁻¹ = 0
theorem FractionalIdeal.inv_nonzero (K : Type u_3) [Field K] {R₁ : Type u_4} [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_nonzero (K : Type u_3) [Field K] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] {J : FractionalIdeal (nonZeroDivisors R₁) K} (h : J 0) :
theorem FractionalIdeal.mem_inv_iff {K : Type u_3} [Field K] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] {I : FractionalIdeal (nonZeroDivisors R₁) K} (hI : I 0) {x : K} :
x I⁻¹ yI, x * y 1
theorem FractionalIdeal.inv_anti_mono {K : Type u_3} [Field K] {R₁ : Type u_4} [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) :
theorem FractionalIdeal.le_self_mul_inv {K : Type u_3} [Field K] {R₁ : Type u_4} [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_3) [Field K] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] (I : Ideal R₁) :
I I * (↑I)⁻¹
theorem FractionalIdeal.right_inverse_eq (K : Type u_3) [Field K] {R₁ : Type u_4} [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_3) [Field K] {R₁ : Type u_4} [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_3) [Field K] {R₁ : Type u_4} [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_3) [Field K] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] {K' : Type u_5} [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_3) [Field K] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] (x : K) :
theorem FractionalIdeal.spanSingleton_div_self (K : Type u_3) [Field K] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] {x : K} (hx : x 0) :
theorem FractionalIdeal.coe_ideal_span_singleton_div_self (K : Type u_3) [Field K] {R₁ : Type u_4} [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_3) [Field K] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] {x : K} (hx : x 0) :
theorem FractionalIdeal.coe_ideal_span_singleton_mul_inv (K : Type u_3) [Field K] {R₁ : Type u_4} [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_3) [Field K] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] {x : K} (hx : x 0) :
theorem FractionalIdeal.coe_ideal_span_singleton_inv_mul (K : Type u_3) [Field K] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] {x : R₁} (hx : x 0) :
(↑(Ideal.span {x}))⁻¹ * (Ideal.span {x}) = 1
theorem FractionalIdeal.invertible_of_principal (K : Type u_3) [Field K] {R₁ : Type u_4} [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.isPrincipal_inv (K : Type u_3) [Field K] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] (I : FractionalIdeal (nonZeroDivisors R₁) K) [(↑I).IsPrincipal] (h : I 0) :
theorem FractionalIdeal.den_mem_inv {K : Type u_3} [Field K] {R₁ : Type u_4} [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_3} [Field K] {R₁ : Type u_4} [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_3} [Field K] {R₁ : Type u_4} [CommRing R₁] [IsDomain R₁] [Algebra R₁ K] [IsFractionRing R₁ K] {I : FractionalIdeal (nonZeroDivisors R₁) K} (hI : I ) :