Theorems · Definition · commutative algebra

FractionalIdeal.equivNumOfIsLocalization

{R : Type u_1} →
  [inst : CommRing R] →
    {S : Submonoid R} →
      {P : Type u_2} →
        [inst_1 : CommRing P] →
          [inst_2 : Algebra R P] →
            [FaithfulSMul R P] → [IsLocalization S P] → (I : FractionalIdeal S P) → ↥↑I ≃ₗ[R] ↥I.num

The linear equivalence between the fractional ideal I in a faithful localization and the integral ideal I.num.

Defined in: Mathlib.RingTheory.FractionalIdeal.Basic
Cited by: 2 results in Mathlib
Foundations: Depth 75 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing CommRing Algebra FaithfulSMul IsLocalization

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites13

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

RingHom.idstatement · cited by 18,349
CommRingstatement and proof · cited by 17,173
Algebrastatement and proof · cited by 11,388
Submodulestatement · cited by 7,192
Idealstatement · cited by 4,748
LinearEquivstatement · cited by 3,317
Submonoidstatement and proof · cited by 3,086
IsLocalizationstatement and proof · cited by 636
FractionalIdealstatement and proof · cited by 423
FaithfulSMulstatement and proof · cited by 340
FractionalIdeal.coeToSubmodulestatement · cited by 130
FractionalIdeal.numstatement · cited by 22

Cited by2

Results whose statement or proof uses this declaration.

FractionalIdeal.isPrincipal_of_isPrincipal_numproof · cited by 0
Module.Invertible.exists_linearEquiv_idealproof · cited by 0