rw

Stream: maths

[Ashvni Narayanan]

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]

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

[Adam Topaz]

(it's sorryabove)

[Reid Barton]

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

[Reid Barton]

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]

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]

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

[Adam Topaz]

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

[Reid Barton]

what about the zero ideal?

[Adam Topaz]

Ok yeah, for nonzero fractional ideals

[Adam Topaz]

Or define a group_with_zero

[Adam Topaz]

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

[Adam Topaz]

Unfortunately, I don't think subgroup_with_zero is a thing.

[Ashvni Narayanan]

I finally figured out the issue. Thank you!