Mathlib Map

Theorems · Theorem · commutative algebra

Algebra.Extension.h1CotangentExtendScalarsEquiv_symm_toLinearMap

∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Extension R S),
  ↑P.h1CotangentExtendScalarsEquiv.symm =
    Algebra.Extension.H1Cotangent.map (Algebra.Extension.defaultHom P.Ring S P.extendScalars)
Defined in
Mathlib.RingTheory.Extension.ExtendScalars
Cited by
1 results in Mathlib
Foundations
Depth 121 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
CommRingCommRingAlgebra
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Algebra.Extension.h1CotangentEquivCotangent_comp_map · cited by 1Extension.h1CotangentEqui…RingHom.id · cited by 18349RingHom.idCommRing · cited by 17173CommRingAlgebra · cited by 11388AlgebraLinearMap · cited by 10215LinearMapLinearEquiv.symm · cited by 1461LinearEquiv.symmLinearEquiv.toLinearMap · cited by 1171LinearEquiv.toLinearMapAlgebra.Extension.Ring · cited by 179Extension.RingAlgebra.Extension · cited by 138Algebra.ExtensionAlgebra.Generators.toExtension · cited by 103Generators.toExtensionAlgebra.Extension.H1Cotangent · cited by 49Extension.H1CotangentAlgebra.H1Cotangent · cited by 27Algebra.H1CotangentAlgebra.Extension.H1Cotangent.map · cited by 25H1Cotangent.mapAlgebra.Generators.self · cited by 22Generators.selfAlgebra.Extension.extendScalars · cited by 12Extension.extendScalarsAlgebra.Extension.defaultHom · cited by 4Extension.defaultHomExtension.h1CotangentExtendSc…CITED BYCITES

Cites16

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

Cited by1

Results whose statement or proof uses this declaration.