# Zulip Chat Archive

## Stream: maths

### Topic: rw

#### Ashvni Narayanan (Sep 03 2020 at 12:49):

I am trying to prove that the set of principal fractional ideals of a number ring is a subgroup of the group of fractional ideals.

```
import linear_algebra.finite_dimensional
import ring_theory.ideal.basic
import algebra.field
import ring_theory.subring
import ring_theory.integral_closure
import ring_theory.fractional_ideal
import data.rat.basic
import ring_theory.algebra
import ring_theory.algebraic
class number_field (K : Type*) :=
(fld : field K)
(alg : algebra ℚ K)
(fd : finite_dimensional ℚ K)
instance field_of_number_field (K : Type*) [number_field K] : field K := _inst_1.fld
instance algebra_of_number_field (K : Type*) [number_field K] : algebra ℚ K := _inst_1.alg
def number_ring (K : Type*) [number_field K] := @integral_closure ℤ K _ (@field.to_comm_ring K _inst_1.fld) _
theorem integral_domain_of_number_ring (K : Type*) [number_field K] : integral_domain (number_ring K) :=
(number_ring K).integral_domain
noncomputable theory
open_locale classical
open finite_dimensional
open ring.fractional_ideal
namespace number_field
variables (K : Type*) [number_field K]
variables (g : fraction_map (number_ring K) K)
def principal_fractional_ideal := { P : ring.fractional_ideal g | submodule.is_principal P.1 }
instance is_group : group (ring.fractional_ideal g) := sorry,
instance is_subgroup : subgroup (ring.fractional_ideal g) :=
begin
use (principal_fractional_ideal K g),
{
sorry,
},
{
unfold principal_fractional_ideal,
simp only [set.mem_set_of_eq],
rintros a b ha hb,
rw ring.fractional_ideal.is_principal_iff at *,
cases ha with c ha,
cases hb with d hb,
use c*d,
rw [ha, hb],
rw ring.fractional_ideal.span_singleton_mul_span_singleton c d,
sorry,
},
{ sorry, },
end
```

In showing that it is closed under multiplication, it gives me an error :

```
rewrite tactic failed, did not find instance of the pattern in the target expression
span_singleton c * span_singleton d
state:
K : Type u_1,
_inst_1 : number_field K,
g : fraction_map ↥(number_ring K) K,
a b : ring.fractional_ideal g,
c : localization_map.codomain g,
ha : a = span_singleton c,
d : localization_map.codomain g,
hb : b = span_singleton d
⊢ span_singleton c * span_singleton d = span_singleton (c * d)
```

I can get it down to a reflectivity statement, but `refl`

does not solve it. Any help is appreciated, thank you!

#### Adam Topaz (Sep 03 2020 at 13:11):

Did you already define the group structure on fractional ideals in your code?

#### Adam Topaz (Sep 03 2020 at 13:12):

(it's `sorry`

above)

#### Reid Barton (Sep 03 2020 at 13:17):

If you want a group, don't you need to be talking about invertible fractional ideals?

#### Reid Barton (Sep 03 2020 at 13:18):

The library already has a `monoid (ring.fractional_ideal g)`

, but you re"defined" it as `sorry`

by writing

```
instance is_group : group (ring.fractional_ideal g) := sorry,
```

(which probably doesn't compile because of the comma), and so the multiplication in `span_singleton c * span_singleton d`

doesn't mean anything and the lemma from the library doesn't apply.

#### Reid Barton (Sep 03 2020 at 13:20):

So I'm guessing this isn't your real code but I'm also a bit confused about what your real code would be, because of the "invertible" issue (I guess you can just use `units (fractional_ideal g)`

).

#### Reid Barton (Sep 03 2020 at 13:21):

Or you could replace "group" by "monoid" throughout as well

#### Adam Topaz (Sep 03 2020 at 13:21):

(for Dedekind domains, invertibility is automatic :smile:)

#### Reid Barton (Sep 03 2020 at 13:22):

what about the zero ideal?

#### Adam Topaz (Sep 03 2020 at 13:23):

Ok yeah, for nonzero fractional ideals

#### Adam Topaz (Sep 03 2020 at 13:24):

Or define a `group_with_zero`

#### Adam Topaz (Sep 03 2020 at 13:38):

I guess even the monoid instance from mathlib should really be a `monoid_with_zero`

#### Adam Topaz (Sep 03 2020 at 13:44):

Unfortunately, I don't think `subgroup_with_zero`

is a thing.

#### Ashvni Narayanan (Sep 03 2020 at 16:53):

I finally figured out the issue. Thank you!

Last updated: May 18 2021 at 06:15 UTC