Theorems · Definition · commutative algebra
Algebra.SubmersivePresentation.basisKaehler
{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 ι σ) → Module.Basis (↑(Set.range P.map)ᶜ) S Ω[S⁄R]Given a submersive presentation of S as R-algebra, the images of dxᵢ
for i in the complement of σ in ι form a basis of Ω[S⁄R].
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 147 from the axioms · uses propext, Classical.choice, Quot.sound
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.
- Setstatement · cited by 53,352
- CommRingstatement and proof · cited by 17,173
- Algebrastatement and proof · cited by 11,388
- Set.Elemstatement · cited by 7,166
- Set.rangestatement · cited by 4,705
- Finitestatement and proof · cited by 3,029
- Compl.complstatement · cited by 2,925
- Module.Basisstatement · cited by 1,477
- KaehlerDifferentialstatement · cited by 204
- Algebra.SubmersivePresentationstatement and proof · cited by 52
- Algebra.SubmersivePresentation.toPreSubmersivePresentationstatement · cited by 47
- Algebra.PreSubmersivePresentation.mapstatement · cited by 34
Cited by4
Results whose statement or proof uses this declaration.
- Algebra.SubmersivePresentation.rank_kaehlerDifferentialproof · cited by 2
- Algebra.IsStandardSmooth.iff_exists_basis_kaehlerDifferentialproof · cited by 1
- Algebra.SubmersivePresentation.basisKaehler_applystatement · cited by 1
- Algebra.SubmersivePresentation.free_kaehlerDifferentialproof · cited by 0