Atlas.NumberTheoryI.code.FractionalIdeals

source

theorem isFractional_iff_fg (A : Type u_1) [CommRing A] [IsDomain A] [IsNoetherianRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (I : Submodule A K) :

IsFractional (nonZeroDivisors A) I ↔ I.FG

source

theorem submodule_fg_iff_isFractional (A : Type u_1) [CommRing A] [IsDomain A] [IsNoetherianRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (I : Submodule A K) :

I.FG ↔ IsFractional (nonZeroDivisors A) I

source

theorem ideal_coe_fractionalIdeal (A : Type u_1) [CommRing A] [IsDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (I : Ideal A) :

∃ (J : FractionalIdeal (nonZeroDivisors A) K), ↑J = IsLocalization.coeSubmodule K I

source

theorem fractionalIdeal_exists_eq_spanSingleton_mul (A : Type u_1) [CommRing A] [IsDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (J : FractionalIdeal (nonZeroDivisors A) K) :

∃ (a : A) (I : Ideal A), a ≠ 0 ∧ J = FractionalIdeal.spanSingleton (nonZeroDivisors A) ((algebraMap A K) a)⁻¹ * ↑I

source

@[deprecated isFractional_iff_fg (since := "2025-05-04")]

theorem Definition_2_13 (A : Type u_1) [CommRing A] [IsDomain A] [IsNoetherianRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (I : Submodule A K) :

IsFractional (nonZeroDivisors A) I ↔ I.FG

source

@[deprecated submodule_fg_iff_isFractional (since := "2025-05-04")]

theorem Lemma_2_14 (A : Type u_1) [CommRing A] [IsDomain A] [IsNoetherianRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (I : Submodule A K) :

I.FG ↔ IsFractional (nonZeroDivisors A) I

source

@[deprecated fractionalIdeal_exists_eq_spanSingleton_mul (since := "2025-05-04")]

theorem Corollary_2_16 (A : Type u_1) [CommRing A] [IsDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (J : FractionalIdeal (nonZeroDivisors A) K) :

∃ (a : A) (I : Ideal A), a ≠ 0 ∧ J = FractionalIdeal.spanSingleton (nonZeroDivisors A) ((algebraMap A K) a)⁻¹ * ↑I

source

@[reducible, inline]

noncomputable abbrev principalFractionalIdeal (A : Type u_1) [CommRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (x : K) :

FractionalIdeal (nonZeroDivisors A) K

Instances For

source

theorem fractionalIdeal_isPrincipal_iff (A : Type u_1) [CommRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (I : FractionalIdeal (nonZeroDivisors A) K) :

(↑I).IsPrincipal ↔ ∃ (x : K), I = FractionalIdeal.spanSingleton (nonZeroDivisors A) x

source

@[deprecated fractionalIdeal_isPrincipal_iff (since := "2025-05-04")]

theorem Definition_2_17 (A : Type u_1) [CommRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (I : FractionalIdeal (nonZeroDivisors A) K) :

(↑I).IsPrincipal ↔ ∃ (x : K), I = FractionalIdeal.spanSingleton (nonZeroDivisors A) x

source

theorem mem_principalFractionalIdeal (A : Type u_1) [CommRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (x y : K) :

y ∈ principalFractionalIdeal A K x ↔ ∃ (a : A), a • x = y

source

theorem colonIdeal_isFractional (A : Type u_1) [CommRing A] [IsDomain A] [IsNoetherianRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (I J : FractionalIdeal (nonZeroDivisors A) K) (hJ : J ≠ 0) :

IsFractional (nonZeroDivisors A) (↑I / ↑J)

source

@[deprecated colonIdeal_isFractional (since := "2025-05-04")]

theorem Lemma_2_18_isFractional (A : Type u_1) [CommRing A] [IsDomain A] [IsNoetherianRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (I J : FractionalIdeal (nonZeroDivisors A) K) (hJ : J ≠ 0) :

IsFractional (nonZeroDivisors A) (↑I / ↑J)

source

theorem colonIdeal_isFractionalIdeal (A : Type u_1) [CommRing A] [IsDomain A] [IsNoetherianRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (I J : FractionalIdeal (nonZeroDivisors A) K) (hJ : J ≠ 0) :

∃ (Q : FractionalIdeal (nonZeroDivisors A) K), ∀ (x : K), x ∈ ↑Q ↔ ∀ y ∈ ↑J, x * y ∈ ↑I

source

@[deprecated colonIdeal_isFractionalIdeal (since := "2025-05-04")]

theorem Lemma_2_18 (A : Type u_1) [CommRing A] [IsDomain A] [IsNoetherianRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (I J : FractionalIdeal (nonZeroDivisors A) K) (hJ : J ≠ 0) :

∃ (Q : FractionalIdeal (nonZeroDivisors A) K), ∀ (x : K), x ∈ ↑Q ↔ ∀ y ∈ ↑J, x * y ∈ ↑I

source

def FractionalIdeal.IsInvertible {A : Type u_1} [CommRing A] {K : Type u_2} [Field K] [Algebra A K] (I : FractionalIdeal (nonZeroDivisors A) K) :

Prop

Instances For

source

theorem FractionalIdeal.isInvertible_iff_exists_mul_eq_one {A : Type u_1} [CommRing A] {K : Type u_2} [Field K] [Algebra A K] (I : FractionalIdeal (nonZeroDivisors A) K) :

I.IsInvertible ↔ ∃ (J : FractionalIdeal (nonZeroDivisors A) K), I * J = 1

source

@[deprecated FractionalIdeal.isInvertible_iff_exists_mul_eq_one (since := "2025-05-04")]

theorem FractionalIdeal.Definition_2_19 {A : Type u_1} [CommRing A] {K : Type u_2} [Field K] [Algebra A K] (I : FractionalIdeal (nonZeroDivisors A) K) :

I.IsInvertible ↔ ∃ (J : FractionalIdeal (nonZeroDivisors A) K), I * J = 1

source

theorem FractionalIdeal.isInvertible_iff_mul_inv_cancel {A : Type u_1} [CommRing A] [IsDomain A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] (I : FractionalIdeal (nonZeroDivisors A) K) :

I.IsInvertible ↔ I * I⁻¹ = 1

source

theorem FractionalIdeal.IsInvertible.inv_eq {A : Type u_1} [CommRing A] [IsDomain A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] (I J : FractionalIdeal (nonZeroDivisors A) K) (h : I * J = 1) :

J = I⁻¹

source

theorem FractionalIdeal.isInvertible_iff_isUnit {A : Type u_1} [CommRing A] {K : Type u_2} [Field K] [Algebra A K] (I : FractionalIdeal (nonZeroDivisors A) K) :

I.IsInvertible ↔ IsUnit I

source

theorem FractionalIdeal.IsInvertible.inv_unique {A : Type u_1} [CommRing A] {K : Type u_2} [Field K] [Algebra A K] (I J J' : FractionalIdeal (nonZeroDivisors A) K) (hJ : I * J = 1) (hJ' : I * J' = 1) :

J = J'

source

theorem FractionalIdeal.isInvertible_iff_mul_inv_eq_one {A : Type u_1} [CommRing A] [IsDomain A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] (I : FractionalIdeal (nonZeroDivisors A) K) :

I.IsInvertible ↔ I * I⁻¹ = 1

source

@[deprecated FractionalIdeal.isInvertible_iff_mul_inv_eq_one (since := "2025-05-04")]

theorem FractionalIdeal.Lemma_2_20 {A : Type u_1} [CommRing A] [IsDomain A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] (I : FractionalIdeal (nonZeroDivisors A) K) :

I.IsInvertible ↔ I * I⁻¹ = 1

source

@[reducible, inline]

noncomputable abbrev IdealGroup (A : Type u_1) [CommRing A] (K : Type u_2) [Field K] [Algebra A K] :

Type u_2

Instances For

source

@[implicit_reducible]

instance IdealGroup.commGroup (A : Type u_1) [CommRing A] (K : Type u_2) [Field K] [Algebra A K] :

CommGroup (IdealGroup A K)

source

theorem mem_idealGroup_iff (A : Type u_1) [CommRing A] (K : Type u_2) [Field K] [Algebra A K] (I : FractionalIdeal (nonZeroDivisors A) K) :

IsUnit I ↔ I.IsInvertible

source

@[reducible, inline]

noncomputable abbrev IdealClassGroup (A : Type u_1) [CommRing A] [IsDomain A] :

Type u_1

Instances For

source

@[implicit_reducible]

noncomputable instance IdealClassGroup.commGroup (A : Type u_1) [CommRing A] [IsDomain A] :

CommGroup (IdealClassGroup A)

source

@[reducible, inline]

noncomputable abbrev PicardGroup (A : Type u_1) [CommRing A] [IsDomain A] :

Type u_1

Instances For

source

noncomputable def IdealClassGroup.mk (A : Type u_1) [CommRing A] [IsDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] :

(FractionalIdeal (nonZeroDivisors A) K)ˣ →* IdealClassGroup A

Instances For

source

theorem IdealClassGroup.eq_classGroup (A : Type u_1) [CommRing A] [IsDomain A] :

IdealClassGroup A = ClassGroup A