Galois group acts on ideals

Stream: Is there code for X?

[Kevin Buzzard]

In a proof, I need this:

import Mathlib.RingTheory.Ideal.Maps

variable (A : Type*) [CommRing A] (B : Type*) [CommRing B] [Algebra A B]

instance foo : MulDistribMulAction (B ≃ₐ[A] B) (Ideal B) where
  smul σ I := Ideal.comap σ.symm I
  one_smul I := I.comap_id
  smul_one σ := by simp only [Ideal.one_eq_top]; rfl
  mul_smul _ _ _ := rfl
  smul_mul σ I J := by
    refine le_antisymm (fun x ↦ ?_ : Ideal.comap _ _ ≤ _) (Ideal.le_comap_mul _)
    obtain ⟨y, rfl⟩ : ∃ y, σ y = x := ⟨σ.symm x, σ.apply_symm_apply x⟩
    rw [Ideal.mem_comap, AlgEquiv.symm_apply_apply, ← Ideal.mem_comap]
    revert y
    refine Ideal.mul_le.mpr (fun r hr s hs ↦ ?_)
    simp only [Ideal.mem_comap, map_mul]
    exact Ideal.mul_mem_mul (Ideal.mem_comap.2 (by simp [hr])) (Ideal.mem_comap.2 <| by simp [hs])

Do we have it already? If not, is this instance suitable for mathlib, or should I just make it a local instance?

[Eric Wieser]

This feels like it ought to follow from docs#Submodule.pointwiseDistribMulAction, but the SMulCommClass requirement doesn't work

[Adam Topaz]

This makes me wonder... what's the general abstraction here? If we have some object X with an action of G, and some other object Y "constructed out of X" (whatever that means...), we get an action of G on Y. Is there something general we can do here?

It's possible to do this with category theory ("constructed out of" means "functor"), but I wonder if anyone has any other ideas.

[Eric Wieser]

I think the missing piece is

instance Ideal.pointwiseMulSemiringAction
    [Monoid α] [MulSemiringAction α B] : MulSemiringAction α (Ideal B) where
  smul a I := Ideal.map (MulSemiringAction.toRingHom _ _ a) I
  one_smul I :=
    congr_arg (I.map ·) (RingHom.ext <| one_smul α) |>.trans I.map_id
  mul_smul _a₁ _a₂ I :=
    congr_arg (I.map ·) (RingHom.ext <| mul_smul _ _) |>.trans (I.map_map _ _).symm
  smul_one a := by simp only [Ideal.one_eq_top]; exact Ideal.map_top _
  smul_mul a I J := Ideal.map_mul _ I J
  smul_add a I J := Ideal.map_sup _ I J
  smul_zero a := Ideal.map_bot

edit: #13294

[Adam Topaz]

Yeah that would works in this case, but again that’s special to Ideal.

[Eric Wieser]

I think every time you "construct Y out of X" you have to specify what that means, which is one of the things this instance captures

[Adam Topaz]

I wish we could do better :-/

[Eric Wieser]

I think this treads into "generalizing SubFoo.map and FooHom.comp" territory

[Antoine Chambert-Loir]

There is an analogous stuff for modules / submodules if one compatible actions on the ring and the module. (This is important, eg, to formulate Galois descent.)

[Antoine Chambert-Loir]

The action on ideals is a particular case, when the module is the ring, with the same action.

[Eric Wieser]

I don't think the two actions are the same, since Ideal.map and Submodule.map are different

[Kevin Buzzard]

docs#Ideal.map and docs#Submodule.map to save people from going to random websites.

[Eric Wieser]

I guess this tension exists in general: should actions /images only exist when they coincide with the set action/image, or should they always exist and take the appropriate closure?

[Antoine Chambert-Loir]

(For a surjective morphism of rings, the ideal map coincides with the submodule map )

[Eric Wieser]

Do we have that result in mathlib?

[Junyan Xu]

(deleted)

[Junyan Xu]

@loogle Ideal.map, RingHomSurjective

[loogle]

:search: Ideal.map_eq_submodule_map