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 #
FractionalIdeal.instInv
definesI⁻¹ := 1 / I
.
References #
- D. Marcus, Number Fields
- J.W.S. Cassels, A. Fröhlich, Algebraic Number Theory
- J. Neukirch, Algebraic Number Theory
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]
:
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_3)
[Field K]
{R₁ : Type u_4}
[CommRing R₁]
[IsDomain R₁]
[Algebra R₁ K]
[IsFractionRing R₁ K]
{I : FractionalIdeal (nonZeroDivisors R₁) K}
:
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)
:
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}
:
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)
:
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)
:
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}
:
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}
:
@[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')
:
@[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_spanSingleton
(K : Type u_3)
[Field K]
{R₁ : Type u_4}
[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_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)
:
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)
:
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)
:
theorem
FractionalIdeal.mul_generator_self_inv
(K : Type u_3)
[Field K]
{R₁ : Type u_6}
[CommRing R₁]
[Algebra R₁ K]
[IsLocalization (nonZeroDivisors R₁) K]
(I : FractionalIdeal (nonZeroDivisors R₁) K)
[(↑I).IsPrincipal]
(h : I ≠ 0)
:
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)
:
theorem
FractionalIdeal.invertible_iff_generator_nonzero
(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]
:
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)
:
(↑I⁻¹).IsPrincipal
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 ≠ ⊥)
:
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)
:
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 ≠ ⊥)
:
noncomputable instance
FractionalIdeal.instInvOneClassNonZeroDivisors
{K : Type u_3}
[Field K]
{R₁ : Type u_4}
[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 := ⋯ }