Theorems · Definition · commutative algebra

Module.Invertible.linearEquiv

(R : Type u) →
  (M : Type v) →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] → [Module.Invertible R M] → TensorProduct R (Module.Dual R M) M ≃ₗ[R] R

Promote the canonical map Mᵛ ⊗[R] M → R to a linear equivalence for invertible M.

Defined in: Mathlib.RingTheory.PicardGroup
Cited by: 8 results in Mathlib
Foundations: Depth 66 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommSemiring AddCommMonoid Module Module.Invertible

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites11

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

Modulestatement and proof · cited by 20,661
RingHom.idstatement · cited by 18,349
AddCommMonoidstatement and proof · cited by 12,281
CommSemiringstatement and proof · cited by 10,911
LinearEquivstatement · cited by 3,317
TensorProductstatement · cited by 2,545
Module.Dualstatement · cited by 583
LinearEquiv.ofBijectiveproof · cited by 60
Module.Invertiblestatement and proof · cited by 41
contractLeftproof · cited by 11
Module.Invertible.bijectiveproof · cited by 1

Cited by9

Results whose statement or proof uses this declaration.

Module.Invertible.free_iff_linearEquivproof · cited by 3
Module.Invertible.bijective_of_surjectiveproof · cited by 3
Module.Invertible.congrproof · cited by 1
Module.Invertible.lTensor_injective_iffproof · cited by 1
Module.Invertible.lTensor_surjective_iffproof · cited by 1
Module.Invertible.algEquivOfRingproof · cited by 1
Module.Invertible.exists_finset_free_localizationproof · cited by 0
Module.Invertible.toModuleEnd_bijectiveproof · cited by 0
Module.Invertible.linearEquiv.congr_simpstatement and proof · cited by 0