## 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 sorryabove)

#### 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:)

#### 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