Theorems · Theorem · commutative algebra

Submodule.unitsQuotEquivRelPic_apply_coe

∀ (R : Type u) (A : Type u_4) [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  [inst_3 : FaithfulSMul R A] (a : (Submodule R A)ˣ ⧸ (Units.map ↑(Submodule.spanSingleton R)).range),
  ↑((Submodule.unitsQuotEquivRelPic R A) a) =
    ↑((QuotientGroup.quotientKerEquivRange (Submodule.unitsToPic R A))
        ((QuotientGroup.congr (Units.map ↑(Submodule.spanSingleton R)).range (Submodule.unitsToPic R A).ker
            (MulEquiv.refl (Submodule R A)ˣ) ⋯)
          a))

Defined in

Mathlib.RingTheory.PicardGroup

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiringAlgebraFaithfulSMul