Theorems · Theorem · commutative algebra

Algebra.SubmersivePresentation.sectionCotangent_eq_iff

∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : Finite σ] (P : Algebra.SubmersivePresentation R S ι σ)
  (x : P.toExtension.CotangentSpace) (y : P.toExtension.Cotangent),
  P.sectionCotangent x = y ↔ ∀ (i : σ), (P.cotangentSpaceBasis.repr x) (P.map i) = P.cotangentComplexAux y i

Defined in: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Cited by: 2 results in Mathlib
Foundations: Depth 143 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing CommRing Algebra Finite

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites31

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

DFunLike.coestatement and proof · cited by 62,936
RingHom.idstatement · cited by 18,349
CommRingstatement and proof · cited by 17,173
Algebrastatement and proof · cited by 11,388
LinearMapstatement · cited by 10,215
Finsuppstatement · cited by 5,255
LinearEquivstatement · cited by 3,317
Finitestatement and proof · cited by 3,029
Module.Basis.reprstatement and proof · cited by 498
KaehlerDifferentialstatement · cited by 204
Algebra.Extension.Ringstatement · cited by 179
LinearEquiv.injectiveproof · cited by 162

Cited by2

Results whose statement or proof uses this declaration.

Algebra.SubmersivePresentation.sectionCotangent_compproof · cited by 1
Algebra.SubmersivePresentation.sectionCotangent_zero_of_notMem_rangeproof · cited by 0