Ring automorphisms acting on ideals

DefinitionRing automorphisms act on fractional ideals#✓fully proved

Let \(R\) be a commutative domain and \(K\) a field of fractions of \(R\). For a ring automorphism \(\sigma\) of \(R\), let \(\tilde\sigma\) be the automorphism of \(K\) extending \(\sigma\). Sending \(\sigma\) to the map \(I \mapsto \tilde\sigma(I)\) on fractional ideals of \(R\) in \(K\) defines a group homomorphism from the group of ring automorphisms of \(R\) to the group of ring automorphisms of the semiring of fractional ideals of \(R\) in \(K\).

noncomputable def ringEquivOfRingEquivHom :
    RingAut R →* RingAut (FractionalIdeal R⁰ K) where
  toFun σ := FractionalIdeal.ringEquivOfRingEquiv K K σ
  map_one' := FractionalIdeal.ringEquivOfRingEquiv_refl K
  map_mul' σ τ := FractionalIdeal.ringEquivOfRingEquiv_trans K K K τ σ

Used by 7

Used byMembership in a translated fractional ideal · Elements of a translated fractional ideal are images · Viewing prime ideals as fractional ideals commutes with the group action · Translating an integral ideal · The action on fractional ideals is by images · Action on invertible fractional ideals · Translating an invertible fractional ideal

AbbreviationAction on invertible fractional ideals#✓fully proved

Let a group \(G\) act on a commutative domain \(R\) by ring automorphisms, let \(K\) be a field of fractions of \(R\), and let \(G\) act on fractional ideals of \(R\) in \(K\) by \(g \cdot I = \tilde\sigma_g(I)\), where \(\tilde\sigma_g\) is the automorphism of \(K\) extending \(r \mapsto g \cdot r\). This induces an action of \(G\) on the group of invertible fractional ideals: \(g\) sends an invertible fractional ideal \(I\) to \(g \cdot I\), whose inverse is \(g \cdot I^{-1}\). This action respects products and fixes the unit fractional ideal \(R\).

noncomputable abbrev unitsMulDistribMulAction :
    MulDistribMulAction G (FractionalIdeal R⁰ K)ˣ :=
  Units.mulDistribMulActionRight

Uses 1 · Used by 1

Statement usesRing automorphisms act on fractional ideals

Used byTranslating an invertible fractional ideal

TheoremTranslating an invertible fractional ideal#✓fully proved

Let a group \(G\) act on a commutative domain \(R\) by ring automorphisms, let \(K\) be a field of fractions of \(R\), and let \(G\) act on fractional ideals of \(R\) in \(K\) by \(g \cdot I = \tilde\sigma_g(I)\), where \(\tilde\sigma_g\) is the automorphism of \(K\) extending \(r \mapsto g \cdot r\). For every \(g \in G\) and every invertible fractional ideal \(I\), the translate of \(I\) under the induced action on invertible fractional ideals has underlying fractional ideal \(g \cdot I\).

@[simp]
theorem units_smul_val (g : G) (I : (FractionalIdeal R⁰ K)ˣ) :
    ((g • I : (FractionalIdeal R⁰ K)ˣ) : FractionalIdeal R⁰ K) =
      g • (I : FractionalIdeal R⁰ K)

Uses 2

Statement usesRing automorphisms act on fractional ideals · Action on invertible fractional ideals

TheoremThe action on fractional ideals is by images#✓fully proved

Let a group \(G\) act on a commutative domain \(R\) by ring automorphisms and let \(K\) be a field of fractions of \(R\). For \(g \in G\) let \(\tilde\sigma_g\) be the automorphism of \(K\) extending the automorphism \(r \mapsto g \cdot r\) of \(R\). Then for every \(g \in G\) and every fractional ideal \(I\) of \(R\) in \(K\), the induced action satisfies \(g \cdot I = \tilde\sigma_g(I)\), the image of \(I\) under \(\tilde\sigma_g\).

@[simp]
theorem smul_def (g : G) (I : FractionalIdeal R⁰ K) :
    g • I =
      FractionalIdeal.ringEquivOfRingEquiv K K
        (MulSemiringAction.toRingAut G R g) I

Uses 1 · Used by 1

Statement usesRing automorphisms act on fractional ideals

Used byElements of a translated fractional ideal are images

TheoremElements of a translated fractional ideal are images#✓fully proved

Let a group \(G\) act on a commutative domain \(R\) by ring automorphisms, let \(K\) be a field of fractions of \(R\), and let \(G\) act on fractional ideals of \(R\) in \(K\) by \(g \cdot I = \tilde\sigma_g(I)\), where \(\tilde\sigma_g\) is the automorphism of \(K\) extending \(r \mapsto g \cdot r\). For every \(g \in G\), every fractional ideal \(I\) and every \(x \in K\), we have \(x \in g \cdot I\) if and only if \(\tilde\sigma_g(y) = x\) for some \(y \in I\).

theorem mem_smul_iff_exists (g : G) (I : FractionalIdeal R⁰ K) (x : K) :
    x ∈ g • I ↔ ∃ y ∈ I,
      IsFractionRing.ringEquivOfRingEquiv
        (MulSemiringAction.toRingAut G R g) y = x

Uses 2 · Used by 2

Statement usesRing automorphisms act on fractional ideals

Proof usesThe action on fractional ideals is by images

Used byMembership in a translated fractional ideal · Translating an integral ideal

TheoremMembership in a translated fractional ideal#✓fully proved

Let a group \(G\) act on a commutative domain \(R\) by ring automorphisms, let \(K\) be a field of fractions of \(R\), and let \(G\) act on fractional ideals of \(R\) in \(K\) by \(g \cdot I = \tilde\sigma_g(I)\), where \(\tilde\sigma_g\) is the automorphism of \(K\) extending \(r \mapsto g \cdot r\). For every \(g \in G\), every fractional ideal \(I\) and every \(x \in K\), we have \(x \in g \cdot I\) if and only if \(\tilde\sigma_g^{-1}(x) \in I\).

theorem mem_smul_iff (g : G) (I : FractionalIdeal R⁰ K) (x : K) :
    x ∈ g • I ↔
      (IsFractionRing.ringEquivOfRingEquiv
        (MulSemiringAction.toRingAut G R g)).symm x ∈ I

Uses 2

Statement usesRing automorphisms act on fractional ideals

Proof usesElements of a translated fractional ideal are images

TheoremTranslating an integral ideal#✓fully proved

Let a group \(G\) act on a commutative domain \(R\) by ring automorphisms, let \(K\) be a field of fractions of \(R\), and let \(G\) act on fractional ideals of \(R\) in \(K\) by \(g \cdot J = \tilde\sigma_g(J)\), where \(\tilde\sigma_g\) is the automorphism of \(K\) extending \(r \mapsto g \cdot r\). For every \(g \in G\) and every ideal \(I\) of \(R\), the translate \(g \cdot I\) of \(I\) viewed as a fractional ideal is the ideal \(\{g \cdot a : a \in I\}\) of \(R\) viewed as a fractional ideal.

@[simp]
theorem smul_coeIdeal (g : G) (I : Ideal R) :
    g • (I : FractionalIdeal R⁰ K) =
      ((g • I : Ideal R) : FractionalIdeal R⁰ K)

Uses 2 · Used by 1

Statement usesRing automorphisms act on fractional ideals

Proof usesElements of a translated fractional ideal are images

Used byViewing prime ideals as fractional ideals commutes with the group action

TheoremTranslating a prime ideal by a group element#✓fully proved

Let a group \(G\) act on a commutative semiring \(R\) by semiring automorphisms, and let \(G\) act on the prime spectrum of \(R\) by the induced action. For every \(g \in G\) and every point \(\mathfrak p\) of the prime spectrum of \(R\), the prime ideal underlying the translated point \(g \cdot \mathfrak p\) is the image of the ideal \(\mathfrak p\) under the automorphism of \(R\) given by \(g\).

@[simp]
theorem smul_asIdeal (g : G) (p : PrimeSpectrum R) :
    (g • p).asIdeal = g • p.asIdeal

Used by 1

Used byViewing prime ideals as fractional ideals commutes with the group action

TheoremViewing prime ideals as fractional ideals commutes with the group action#✓fully proved

Let a group \(G\) act on an integral domain \(R\) by ring automorphisms, let \(K\) be a fraction field of \(R\), and let \(G\) act on the fractional ideals of \(R\) in \(K\) through the extension of each automorphism of \(R\) to \(K\). For \(g \in G\) and a prime ideal \(\mathfrak p\) of \(R\), write \(g \cdot \mathfrak p = \{g \cdot x : x \in \mathfrak p\}\) for the image of \(\mathfrak p\) under \(g\), again a prime ideal of \(R\). Then for every \(g \in G\) and every prime ideal \(\mathfrak p\) of \(R\), the ideal \(g \cdot \mathfrak p\) viewed as a fractional ideal in \(K\) equals \(g\) applied to \(\mathfrak p\) viewed as a fractional ideal in \(K\).

@[simp]
theorem smul_asIdeal_coe (g : G) (p : PrimeSpectrum R) :
    FractionalIdeal.coeIdeal (S := R⁰) (P := K) (g • p).asIdeal =
      g • FractionalIdeal.coeIdeal (S := R⁰) (P := K) p.asIdeal

Uses 3

Statement usesRing automorphisms act on fractional ideals

Proof usesTranslating an integral ideal · Translating a prime ideal by a group element

9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.