multiplier subring

Stream: Is there code for X?

[Edward van de Meent]

does mathlib already have the following concept?

def multiplierRing
    (K : Type*) [Ring K]
    (SK : Type*) [SetLike SK K] [AddSubgroupClass SK K] (I : SK) :
    Subring K where
  carrier := {x:K | ∀ i ∈ I, (x * i) ∈ I}
  add_mem' := fun {a b} ha hb i hi=> by
    simp only [Set.mem_setOf_eq] at ha hb ⊢
    rw [right_distrib]
    exact add_mem (ha i hi) (hb i hi)
  zero_mem' := by
    simp only [Set.mem_setOf_eq, zero_mul]
    intros
    exact zero_mem I
  one_mem' := by
    simp only [Set.mem_setOf_eq, one_mul, imp_self, forall_const]
  neg_mem' {a} := by
    simp only [Set.mem_setOf_eq, neg_mul]
    intro ha i hi
    exact neg_mem (ha i hi)
  mul_mem' {a b} := by
    simp only [Set.mem_setOf_eq]
    intro ha hb i hi
    rw [mul_assoc]
    exact ha (b * i) (hb i hi)

i'm asking because i'd like to prove that for fractional ideals, if the ideal is invertible, it is proper, (i.e. its multiplier subring is exactly the embedding of R in its field of fractions)

[Edward van de Meent]

as a side note, to make this work for fractional ideals i also need the AddSubgroupClass instance for FractionalIdeal, which afaict doesn't exist either?

[Yaël Dillies]

Is this not docs#Submodule.colon ?

[Edward van de Meent]

it looks like it...

[Edward van de Meent]

by the way, is there a reason why FractionalIdeal is a def using Subtype rather than this:

structure FractionalIdeal extends Submodule R P where
  isFractional : IsFractional S toSubmodule

[Edward van de Meent]

because i think the above works much nicer, exposing I.add_mem and the like...

[Kevin Buzzard]

Yaël Dillies said:

Is this not docs#Submodule.colon ?

That produces an ideal from an ideal. This produces a subring from a subgroup.