Theorems · Theorem · commutative algebra

IsFractional.mapEquiv

∀ {R : Type u_5} {S : Type u_6} (K : Type u_7) (L : Type u_8) [inst : CommRing R] [IsDomain R] [inst_2 : CommRing S]
  [IsDomain S] [inst_4 : CommRing K] [inst_5 : CommRing L] [inst_6 : Algebra R K] [inst_7 : Algebra S L]
  [inst_8 : IsFractionRing R K] [inst_9 : IsFractionRing S L] (f : R ≃+* S) {I : Submodule R K},
  IsFractional (nonZeroDivisors R) I →
    IsFractional (nonZeroDivisors S) (Submodule.map (↑(IsFractionRing.semilinearEquivOfRingEquiv K L f)) I)

If f : R ≃+* S is a ring isomorphism and I : Submodule R K is fractional with respect to R⁰, then I.map (IsFractionRing.semilinearEquivOfRingEquiv K L f).toLinearMap is fractional with respect to S⁰. Do not confuse with IsFractional.map.

Defined in

Mathlib.RingTheory.FractionalIdeal.Operations

Cited by

2 results in Mathlib

Foundations

Depth 63 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingIsDomainCommRingIsDomainCommRingCommRingAlgebraAlgebraIsFractionRingIsFractionRing