Submersive

📁 Source: Mathlib/RingTheory/Extension/Presentation/Submersive.lean

Statistics

Metric	Count
Definitions PreSubmersivePresentation, aevalDifferential, baseChange, basis, comp, differential, jacobiMatrix, jacobian, localizationAway, map, naive, ofAlgEquiv, ofBijectiveAlgebraMap, reindex, toPresentation, SubmersivePresentation, aevalDifferentialEquiv, baseChange, basisDeriv, comp, id, localizationAway, ofAlgEquiv, ofBijectiveAlgebraMap, ofSubsingleton, reindex, toPreSubmersivePresentation	27
Theorems aevalDifferential_single, aevalDifferential_toMatrix'_eq_mapMatrix_jacobiMatrix, baseChange_jacobian, baseChange_ring, baseChange_toPresentation, card_relations_le_card_vars_of_isFinite, comp_jacobian_eq_jacobian_smul_jacobian, comp_map, dimension_comp_eq_dimension_add_dimension, isUnit_jacobian_iff_aevalDifferential_bijective, isUnit_jacobian_of_linearIndependent_of_span_eq_top, jacobiMatrix_apply, jacobiMatrix_naive, jacobiMatrix_ofAlgEquiv, jacobiMatrix_reindex, jacobian_eq_det_aevalDifferential, jacobian_eq_jacobiMatrix_det, jacobian_ofAlgEquiv, jacobian_reindex, localizationAway_jacobiMatrix, localizationAway_jacobian, localizationAway_map, map_inj, naive_toPresentation, ofAlgEquiv_map, ofAlgEquiv_toPresentation, ofBijectiveAlgebraMap_jacobian, reindex_map, reindex_toPresentation, toGenerators_comp, toPresentation_comp, aevalDifferentialEquiv_apply, basisDeriv_apply, jacobian_isUnit, linearIndependent_aeval_val_pderiv_relation, ofAlgEquiv_toPreSubmersivePresentation, ofSubsingleton_algebra_algebraMap, ofSubsingleton_algebra_smul, ofSubsingleton_map, ofSubsingleton_relation, ofSubsingleton_val, ofSubsingleton_σ', reindex_toPreSubmersivePresentation	43
Total	70

Algebra

Definitions

Name	Category	Theorems
PreSubmersivePresentation 📖	CompData	—
SubmersivePresentation 📖	CompData	1 math math: IsStandardSmooth.out

Algebra.PreSubmersivePresentation

Definitions

Name	Category	Theorems
aevalDifferential 📖	CompOp	5 math math: isUnit_jacobian_iff_aevalDifferential_bijective, aevalDifferential_toMatrix'_eq_mapMatrix_jacobiMatrix, jacobian_eq_det_aevalDifferential, aevalDifferential_single, Algebra.SubmersivePresentation.aevalDifferentialEquiv_apply
baseChange 📖	CompOp	3 math math: baseChange_jacobian, baseChange_toPresentation, baseChange_ring
basis 📖	CompOp	—
comp 📖	CompOp	5 math math: comp_jacobian_eq_jacobian_smul_jacobian, dimension_comp_eq_dimension_add_dimension, comp_map, toPresentation_comp, toGenerators_comp
differential 📖	CompOp	—
jacobiMatrix 📖	CompOp	11 math math: jacobiMatrix_naive, jacobiMatrix_ofAlgEquiv, jacobiMatrix_reindex, Algebra.SubmersivePresentation.map_jacobianOfHasCoeffs, Algebra.SubmersivePresentation.jacobianRelations_spec, aevalDifferential_toMatrix'_eq_mapMatrix_jacobiMatrix, jacobiMatrix_apply, Algebra.SubmersivePresentation.exists_sum_eq_σ_jacobian_mul_σ_jacobian_inv_sub_one, localizationAway_jacobiMatrix, MvPolynomial.universalFactorizationMapPresentation_jacobiMatrix, jacobian_eq_jacobiMatrix_det
jacobian 📖	CompOp	26 math math: jacobian_ofAlgEquiv, jacobian_reindex, Polynomial.UniversalCoprimeFactorizationRing.exists_liesOver_residueFieldMap_bijective, baseChange_jacobian, isUnit_jacobian_iff_aevalDifferential_bijective, Polynomial.UniversalCoprimeFactorizationRing.homEquiv_comp_snd, Polynomial.UniversalFactorizationRing.jacobian_resentation, Algebra.SubmersivePresentation.jacobianRelations_spec, comp_jacobian_eq_jacobian_smul_jacobian, Polynomial.UniversalCoprimeFactorizationRing.homEquiv_comp_fst, Algebra.SubmersivePresentation.map_invJacobianOfHasCoeffs, jacobian_eq_det_aevalDifferential, isUnit_jacobian_of_cotangentRestrict_bijective, StandardEtalePresentation.toSubmersivePresentation_jacobian, isUnit_jacobian_of_linearIndependent_of_span_eq_top, ofBijectiveAlgebraMap_jacobian, Algebra.SubmersivePresentation.aeval_jacobianOfHasCoeffs, Algebra.SubmersivePresentation.aeval_invJacobianOfHasCoeffs, Algebra.SubmersivePresentation.exists_sum_eq_σ_jacobian_mul_σ_jacobian_inv_sub_one, Polynomial.UniversalCoprimeFactorizationRing.factor₁_mul_factor₂, Algebra.SubmersivePresentation.jacobian_isUnit, Polynomial.UniversalCoprimeFactorizationRing.isCoprime_factor₁_factor₂, jacobian_eq_jacobiMatrix_det, Polynomial.instEtaleUniversalCoprimeFactorizationRing, MvPolynomial.universalFactorizationMapPresentation_jacobian, localizationAway_jacobian
localizationAway 📖	CompOp	3 math math: localizationAway_map, localizationAway_jacobiMatrix, localizationAway_jacobian
map 📖	CompOp	17 math math: cotangentComplexAux_apply, ofHasCoeffs_map, cotangentComplexAux_zero_iff, localizationAway_map, jacobiMatrix_apply, Algebra.SubmersivePresentation.linearIndependent_aeval_val_pderiv_relation, Algebra.SubmersivePresentation.sectionCotangent_eq_iff, StandardEtalePresentation.toSubmersivePresentation_map, map_inj, MvPolynomial.universalFactorizationMapPresentation_map, aevalDifferential_single, ofAlgEquiv_map, comp_map, Algebra.SubmersivePresentation.basisKaehler_apply, reindex_map, Algebra.SubmersivePresentation.basisDeriv_apply, Algebra.SubmersivePresentation.ofSubsingleton_map
naive 📖	CompOp	2 math math: jacobiMatrix_naive, naive_toPresentation
ofAlgEquiv 📖	CompOp	5 math math: jacobian_ofAlgEquiv, jacobiMatrix_ofAlgEquiv, Algebra.SubmersivePresentation.ofAlgEquiv_toPreSubmersivePresentation, ofAlgEquiv_map, ofAlgEquiv_toPresentation
ofBijectiveAlgebraMap 📖	CompOp	1 math math: ofBijectiveAlgebraMap_jacobian
reindex 📖	CompOp	5 math math: jacobian_reindex, Algebra.SubmersivePresentation.reindex_toPreSubmersivePresentation, jacobiMatrix_reindex, reindex_toPresentation, reindex_map
toPresentation 📖	CompOp	59 math math: Algebra.SubmersivePresentation.cotangentComplexAux_injective, cotangentComplexAux_apply, ofHasCoeffs_map, cotangentComplexAux_zero_iff, jacobiMatrix_reindex, Algebra.SubmersivePresentation.ofSubsingleton_algebra_algebraMap, Algebra.SubmersivePresentation.map_jacobianOfHasCoeffs, ofHasCoeffs_relation, StandardEtalePresentation.toSubmersivePresentation_toPreSubmersivePresentation_toPresentation, Algebra.SubmersivePresentation.basisKaehlerOfIsCompl_apply, Algebra.SubmersivePresentation.instHasCoeffs, ofHasCoeffs_σ', Algebra.SubmersivePresentation.ofSubsingleton_relation, baseChange_toPresentation, Algebra.SubmersivePresentation.jacobianRelations_spec, aevalDifferential_toMatrix'_eq_mapMatrix_jacobiMatrix, jacobiMatrix_apply, ofHasCoeffs_algebra_algebraMap_apply, Algebra.SubmersivePresentation.map_invJacobianOfHasCoeffs, Algebra.SubmersivePresentation.linearIndependent_aeval_val_pderiv_relation, Algebra.SubmersivePresentation.sectionCotangent_eq_iff, naive_toPresentation, Algebra.SubmersivePresentation.coeffs_toPresentation_subset_coeffs, Algebra.SubmersivePresentation.subsingleton_h1Cotangent, MvPolynomial.universalFactorizationMapPresentation_relation, dimension_comp_eq_dimension_add_dimension, aevalDifferential_single, Algebra.SubmersivePresentation.ofSubsingleton_val, MvPolynomial.universalFactorizationMapPresentation_algebra_algebraMap, Algebra.SubmersivePresentation.sum_jacobianRelationsOfHasCoeffs_mul_relationOfHasCoeffs, Algebra.SubmersivePresentation.aeval_jacobianOfHasCoeffs, Algebra.SubmersivePresentation.aeval_invJacobianOfHasCoeffs, Algebra.SubmersivePresentation.basisCotangent_localizationAway_apply, Algebra.SubmersivePresentation.cotangentComplexAux_surjective, ofAlgEquiv_toPresentation, Algebra.SubmersivePresentation.basisKaehler_apply, Algebra.SubmersivePresentation.exists_sum_eq_σ_jacobian_mul_σ_jacobian_inv_sub_one, toPresentation_comp, Algebra.SubmersivePresentation.ofSubsingleton_algebra_smul, Algebra.SubmersivePresentation.ofSubsingleton_σ', Algebra.SubmersivePresentation.rank_kaehlerDifferential, MvPolynomial.universalFactorizationMapPresentation_algebra_smul, Algebra.SubmersivePresentation.sectionCotangent_comp, MvPolynomial.universalFactorizationMapPresentation_val, MvPolynomial.universalFactorizationMapPresentation_σ', Algebra.SubmersivePresentation.sectionCotangent_zero_of_notMem_range, localizationAway_jacobiMatrix, Algebra.SubmersivePresentation.free_cotangent, ofHasCoeffs_val, ofHasCoeffs_algebra_smul, Algebra.SubmersivePresentation.cotangentComplex_injective, Algebra.SubmersivePresentation.basisCotangent_apply, reindex_toPresentation, Algebra.IsStandardSmoothOfRelativeDimension.out, jacobian_eq_jacobiMatrix_det, Algebra.SubmersivePresentation.cotangentEquiv_apply, baseChange_ring, Algebra.SubmersivePresentation.basisDeriv_apply, toGenerators_comp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aevalDifferential_single 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Pi.Function.module Semiring.toModule LinearMap.instFunLike aevalDifferential Pi.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing AlgHom MvPolynomial MvPolynomial.commSemiring MvPolynomial.algebra Algebra.id AlgHom.funLike MvPolynomial.aeval Algebra.Generators.val Algebra.Presentation.toGenerators toPresentation Derivation NonAssocSemiring.toNonUnitalNonAssocSemiring MvPolynomial.module Derivation.instFunLike MvPolynomial.pderiv map Algebra.Presentation.relation	—	Pi.basisFun_apply RingHomInvPair.ids Module.Basis.constr_basis
aevalDifferential_toMatrix'_eq_mapMatrix_jacobiMatrix 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule Matrix LinearMap.addCommMonoid Matrix.addCommMonoid LinearMap.module Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.toMatrix' aevalDifferential Finite.of_fintype AlgHom MvPolynomial Matrix.semiring MvPolynomial.commSemiring Matrix.instAlgebra MvPolynomial.algebra AlgHom.funLike AlgHom.mapMatrix MvPolynomial.aeval Algebra.Generators.val Algebra.Presentation.toGenerators toPresentation jacobiMatrix	—	Matrix.ext RingHomInvPair.ids Function.smulCommClass Algebra.to_smulCommClass Finite.of_fintype smulCommClass_self LinearMap.toMatrix_eq_toMatrix' LinearMap.toMatrix_apply Pi.basisFun_apply Pi.basisFun_repr aevalDifferential_single jacobiMatrix_apply
baseChange_jacobian 📖	mathematical	—	jacobian TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule CommSemiring.toSemiring Algebra.TensorProduct.instCommRing Algebra.TensorProduct.leftAlgebra Algebra.id Algebra.to_smulCommClass baseChange TensorProduct.tmul AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	nonempty_fintype Algebra.to_smulCommClass jacobian_eq_jacobiMatrix_det Matrix.ext jacobiMatrix_apply MvPolynomial.pderiv_map RingHom.map_det Algebra.Generators.algebraMap_apply MvPolynomial.aeval_map_algebraMap TensorProduct.isScalarTower_left IsScalarTower.right MvPolynomial.aeval_one_tmul
baseChange_ring 📖	mathematical	—	Algebra.Generators.Ring TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule CommSemiring.toSemiring Algebra.id Algebra.TensorProduct.instCommRing Algebra.TensorProduct.leftAlgebra Algebra.to_smulCommClass Algebra.Presentation.toGenerators toPresentation baseChange	—	Algebra.to_smulCommClass
baseChange_toPresentation 📖	mathematical	—	toPresentation TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule CommSemiring.toSemiring Algebra.id Algebra.TensorProduct.instCommRing Algebra.TensorProduct.leftAlgebra Algebra.to_smulCommClass baseChange Algebra.Presentation.baseChange	—	Algebra.to_smulCommClass
card_relations_le_card_vars_of_isFinite 📖	mathematical	—	Nat.card	—	Nat.card_le_card_of_injective
comp_jacobian_eq_jacobian_smul_jacobian 📖	mathematical	—	jacobian comp Finite.instSum Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring	—	nonempty_fintype Finite.instSum Finite.of_fintype jacobian_eq_jacobiMatrix_det Matrix.fromBlocks_toBlocks Algebra.Generators.algebraMap_apply NonUnitalAlgSemiHomClass.toMulHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass Matrix.det_fromBlocks_zero₁₂ mul_comm Algebra.smul_def
comp_map 📖	mathematical	—	map comp	—	—
dimension_comp_eq_dimension_add_dimension 📖	mathematical	—	Algebra.Presentation.dimension toPresentation comp	—	card_relations_le_card_vars_of_isFinite Nat.card_sum
isUnit_jacobian_iff_aevalDifferential_bijective 📖	mathematical	—	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring jacobian Function.Bijective DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Pi.Function.module Semiring.toModule LinearMap.instFunLike aevalDifferential	—	jacobian_eq_det_aevalDifferential LinearMap.isUnit_iff_isUnit_det Module.Finite.pi Module.Finite.self Module.Free.function Module.Free.self Module.End.isUnit_iff
isUnit_jacobian_of_linearIndependent_of_span_eq_top 📖	mathematical	LinearIndependent DFunLike.coe AlgHom MvPolynomial CommRing.toCommSemiring CommSemiring.toSemiring MvPolynomial.commSemiring MvPolynomial.algebra Algebra.id AlgHom.funLike MvPolynomial.aeval Algebra.Generators.val Algebra.Presentation.toGenerators toPresentation Derivation NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule MvPolynomial.module Derivation.instFunLike MvPolynomial.pderiv map Algebra.Presentation.relation Pi.addCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Pi.Function.module Submodule.span Set.range Top.top Submodule Submodule.instTop	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero jacobian	—	isUnit_jacobian_iff_aevalDifferential_bijective LinearMap.bijective_of_linearIndependent_of_span_eq_top Module.Basis.span_eq Pi.basisFun_apply aevalDifferential_single
jacobiMatrix_apply 📖	mathematical	—	jacobiMatrix DFunLike.coe Derivation MvPolynomial CommRing.toCommSemiring MvPolynomial.commSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.algebra Algebra.id Semiring.toModule MvPolynomial.module Derivation.instFunLike MvPolynomial.pderiv map Algebra.Presentation.relation toPresentation	—	Finite.of_fintype RingHomInvPair.ids smulCommClass_self LinearEquiv.trans.congr_simp LinearEquiv.arrowCongr.congr_simp Pi.basisFun_equivFun Function.smulCommClass Algebra.to_smulCommClass Module.Basis.constr_apply_fintype Finset.sum_congr Fintype.sum_single_smul one_smul
jacobiMatrix_naive 📖	mathematical	—	jacobiMatrix HasQuotient.Quotient MvPolynomial CommRing.toCommSemiring Ideal CommSemiring.toSemiring MvPolynomial.commSemiring Ideal.instHasQuotient_1 MvPolynomial.instCommRingMvPolynomial Ideal.span Set.range Ideal.Quotient.commRing Ideal.instAlgebraQuotient MvPolynomial.algebra Algebra.id naive DFunLike.coe Derivation NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule MvPolynomial.module Derivation.instFunLike MvPolynomial.pderiv	—	Ideal.instIsTwoSided_1 Ideal.Quotient.mk_surjective jacobiMatrix_apply
jacobiMatrix_ofAlgEquiv 📖	mathematical	—	jacobiMatrix ofAlgEquiv	—	—
jacobiMatrix_reindex 📖	mathematical	—	jacobiMatrix reindex Matrix.map Algebra.Generators.Ring Algebra.Presentation.toGenerators toPresentation MvPolynomial CommRing.toCommSemiring DFunLike.coe Equiv Matrix EquivLike.toFunLike Equiv.instEquivLike Matrix.reindex Equiv.symm AlgHom CommSemiring.toSemiring MvPolynomial.commSemiring MvPolynomial.algebra Algebra.id AlgHom.funLike MvPolynomial.rename	—	Matrix.ext jacobiMatrix_apply MvPolynomial.pderiv_rename Equiv.injective
jacobian_eq_det_aevalDifferential 📖	mathematical	—	jacobian DFunLike.coe MonoidHom LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Pi.addCommGroup Ring.toAddCommGroup CommRing.toRing Pi.Function.module NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike LinearMap.det aevalDifferential	—	nonempty_fintype Finite.of_fintype AlgHomClass.toRingHomClass AlgHom.algHomClass jacobian_eq_jacobiMatrix_det Algebra.Generators.algebraMap_eq RingHom.map_det RingHomInvPair.ids Function.smulCommClass Algebra.to_smulCommClass Matrix.det.congr_simp aevalDifferential_toMatrix'_eq_mapMatrix_jacobiMatrix
jacobian_eq_jacobiMatrix_det 📖	mathematical	—	jacobian Finite.of_fintype DFunLike.coe RingHom Algebra.Generators.Ring Algebra.Presentation.toGenerators toPresentation Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap Algebra.Generators.instRing Matrix.det MvPolynomial.instCommRingMvPolynomial jacobiMatrix	—	Finite.of_fintype Algebra.Generators.algebraMap_apply LinearMap.det_toMatrix'
jacobian_ofAlgEquiv 📖	mathematical	—	jacobian ofAlgEquiv DFunLike.coe AlgEquiv CommRing.toCommSemiring CommSemiring.toSemiring AlgEquiv.instFunLike	—	nonempty_fintype Finite.of_fintype jacobian_eq_jacobiMatrix_det AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass Algebra.Generators.algebraMap_apply MvPolynomial.comp_aeval_apply
jacobian_reindex 📖	mathematical	—	jacobian reindex	—	nonempty_fintype jacobian_eq_jacobiMatrix_det Matrix.det.congr_simp jacobiMatrix_reindex Algebra.Generators.algebraMap_apply Matrix.det_submatrix_equiv_self AlgHom.map_det Matrix.map_map MvPolynomial.rename_comp_rename Equiv.self_comp_symm MvPolynomial.rename_id CompTriple.comp_eq CompTriple.instComp_id CompTriple.instIsIdId
localizationAway_jacobiMatrix 📖	mathematical	—	jacobiMatrix localizationAway PUnit.fintype Matrix.diagonal Algebra.Generators.Ring Algebra.Presentation.toGenerators toPresentation MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing MvPolynomial.instCommRingMvPolynomial DFunLike.coe RingHom MvPolynomial CommRing.toCommSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring RingHom.instFunLike MvPolynomial.C	—	map_sub Derivation.instAddMonoidHomClass Derivation.leibniz MvPolynomial.pderiv_X Pi.single_eq_same mul_one MvPolynomial.derivation_C MulZeroClass.mul_zero add_zero Derivation.map_one_eq_zero sub_zero Matrix.ext jacobiMatrix_apply
localizationAway_jacobian 📖	mathematical	—	jacobian localizationAway Finite.of_fintype PUnit.fintype DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap	—	Finite.of_fintype jacobian_eq_jacobiMatrix_det localizationAway_jacobiMatrix Matrix.det_unique Matrix.diagonal_apply_eq Algebra.Generators.algebraMap_apply MvPolynomial.algHom_C
localizationAway_map 📖	mathematical	—	map localizationAway	—	—
map_inj 📖	mathematical	—	map	—	—
naive_toPresentation 📖	mathematical	—	toPresentation HasQuotient.Quotient MvPolynomial CommRing.toCommSemiring Ideal CommSemiring.toSemiring MvPolynomial.commSemiring Ideal.instHasQuotient_1 MvPolynomial.instCommRingMvPolynomial Ideal.span Set.range Ideal.Quotient.commRing Ideal.instAlgebraQuotient MvPolynomial.algebra Algebra.id naive Algebra.Presentation.naive	—	Ideal.instIsTwoSided_1 Ideal.Quotient.mk_surjective
ofAlgEquiv_map 📖	mathematical	—	map ofAlgEquiv	—	—
ofAlgEquiv_toPresentation 📖	mathematical	—	toPresentation ofAlgEquiv Algebra.Presentation.ofAlgEquiv	—	—
ofBijectiveAlgebraMap_jacobian 📖	mathematical	Function.Bijective DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap	jacobian ofBijectiveAlgebraMap Finite.of_fintype Fintype.instPEmpty AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	Matrix.ext Finite.of_fintype jacobian_eq_jacobiMatrix_det RingHom.map_det Matrix.det_one
reindex_map 📖	mathematical	—	map reindex DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm	—	—
reindex_toPresentation 📖	mathematical	—	toPresentation reindex Algebra.Presentation.reindex	—	—
toGenerators_comp 📖	mathematical	—	Algebra.Presentation.toGenerators toPresentation comp Algebra.Generators.comp	—	—
toPresentation_comp 📖	mathematical	—	toPresentation comp Algebra.Presentation.comp	—	—

Algebra.SubmersivePresentation

Definitions

Name	Category	Theorems
aevalDifferentialEquiv 📖	CompOp	1 math math: aevalDifferentialEquiv_apply
baseChange 📖	CompOp	—
basisDeriv 📖	CompOp	1 math math: basisDeriv_apply
comp 📖	CompOp	—
id 📖	CompOp	—
localizationAway 📖	CompOp	1 math math: basisCotangent_localizationAway_apply
ofAlgEquiv 📖	CompOp	1 math math: ofAlgEquiv_toPreSubmersivePresentation
ofBijectiveAlgebraMap 📖	CompOp	—
ofSubsingleton 📖	CompOp	6 math math: ofSubsingleton_algebra_algebraMap, ofSubsingleton_relation, ofSubsingleton_val, ofSubsingleton_algebra_smul, ofSubsingleton_σ', ofSubsingleton_map
reindex 📖	CompOp	1 math math: reindex_toPreSubmersivePresentation
toPreSubmersivePresentation 📖	CompOp	37 math math: cotangentComplexAux_injective, reindex_toPreSubmersivePresentation, ofSubsingleton_algebra_algebraMap, map_jacobianOfHasCoeffs, StandardEtalePresentation.toSubmersivePresentation_toPreSubmersivePresentation_toPresentation, instHasCoeffs, ofSubsingleton_relation, ofAlgEquiv_toPreSubmersivePresentation, jacobianRelations_spec, map_invJacobianOfHasCoeffs, linearIndependent_aeval_val_pderiv_relation, sectionCotangent_eq_iff, StandardEtalePresentation.toSubmersivePresentation_map, coeffs_toPresentation_subset_coeffs, StandardEtalePresentation.toSubmersivePresentation_jacobian, subsingleton_h1Cotangent, ofSubsingleton_val, sum_jacobianRelationsOfHasCoeffs_mul_relationOfHasCoeffs, aeval_jacobianOfHasCoeffs, aeval_invJacobianOfHasCoeffs, basisCotangent_localizationAway_apply, cotangentComplexAux_surjective, basisKaehler_apply, exists_sum_eq_σ_jacobian_mul_σ_jacobian_inv_sub_one, aevalDifferentialEquiv_apply, ofSubsingleton_algebra_smul, ofSubsingleton_σ', rank_kaehlerDifferential, sectionCotangent_comp, jacobian_isUnit, free_cotangent, cotangentComplex_injective, basisCotangent_apply, Algebra.IsStandardSmoothOfRelativeDimension.out, cotangentEquiv_apply, basisDeriv_apply, ofSubsingleton_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aevalDifferentialEquiv_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Pi.Function.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv aevalDifferentialEquiv LinearMap LinearMap.instFunLike Algebra.PreSubmersivePresentation.aevalDifferential toPreSubmersivePresentation	—	RingHomInvPair.ids
basisDeriv_apply 📖	mathematical	—	DFunLike.coe Module.Basis CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Pi.Function.module Semiring.toModule Module.Basis.instFunLike basisDeriv AlgHom MvPolynomial MvPolynomial.commSemiring MvPolynomial.algebra Algebra.id AlgHom.funLike MvPolynomial.aeval Algebra.Generators.val Algebra.Presentation.toGenerators Algebra.PreSubmersivePresentation.toPresentation toPreSubmersivePresentation Derivation NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring MvPolynomial.module Derivation.instFunLike MvPolynomial.pderiv Algebra.PreSubmersivePresentation.map Algebra.Presentation.relation	—	RingHomInvPair.ids Pi.basisFun_apply Algebra.PreSubmersivePresentation.aevalDifferential_single
jacobian_isUnit 📖	mathematical	—	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Algebra.PreSubmersivePresentation.jacobian toPreSubmersivePresentation	—	—
linearIndependent_aeval_val_pderiv_relation 📖	mathematical	—	LinearIndependent DFunLike.coe AlgHom MvPolynomial CommRing.toCommSemiring CommSemiring.toSemiring MvPolynomial.commSemiring MvPolynomial.algebra Algebra.id AlgHom.funLike MvPolynomial.aeval Algebra.Generators.val Algebra.Presentation.toGenerators Algebra.PreSubmersivePresentation.toPresentation toPreSubmersivePresentation Derivation NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule MvPolynomial.module Derivation.instFunLike MvPolynomial.pderiv Algebra.PreSubmersivePresentation.map Algebra.Presentation.relation Pi.addCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Pi.Function.module	—	Module.Basis.linearIndependent
ofAlgEquiv_toPreSubmersivePresentation 📖	mathematical	—	toPreSubmersivePresentation ofAlgEquiv Algebra.PreSubmersivePresentation.ofAlgEquiv	—	—
ofSubsingleton_algebra_algebraMap 📖	mathematical	—	Algebra.algebraMap MvPolynomial CommRing.toCommSemiring MvPolynomial.commSemiring CommSemiring.toSemiring Algebra.Generators.algebra Algebra.Presentation.toGenerators Algebra.PreSubmersivePresentation.toPresentation toPreSubmersivePresentation Finite.of_fintype PUnit.fintype ofSubsingleton AlgHom.toRingHom MvPolynomial.algebra Algebra.id MvPolynomial.aeval AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	Finite.of_fintype
ofSubsingleton_algebra_smul 📖	mathematical	—	MvPolynomial CommRing.toCommSemiring Algebra.toSMul MvPolynomial.commSemiring CommSemiring.toSemiring Algebra.Generators.algebra Algebra.Presentation.toGenerators Algebra.PreSubmersivePresentation.toPresentation toPreSubmersivePresentation Finite.of_fintype PUnit.fintype ofSubsingleton Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DFunLike.coe RingHom RingHom.instFunLike AlgHom.toRingHom MvPolynomial.algebra Algebra.id MvPolynomial.aeval AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	Finite.of_fintype
ofSubsingleton_map 📖	mathematical	—	Algebra.PreSubmersivePresentation.map toPreSubmersivePresentation Finite.of_fintype PUnit.fintype ofSubsingleton	—	Finite.of_fintype
ofSubsingleton_relation 📖	mathematical	—	Algebra.Presentation.relation Algebra.PreSubmersivePresentation.toPresentation toPreSubmersivePresentation Finite.of_fintype PUnit.fintype ofSubsingleton Algebra.Generators.Ring AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing MvPolynomial CommRing.toCommSemiring MvPolynomial.instCommRingMvPolynomial RingHom.toAlgebra MvPolynomial.commSemiring AlgHom.toRingHom CommSemiring.toSemiring MvPolynomial.algebra Algebra.id MvPolynomial.aeval	—	Finite.of_fintype
ofSubsingleton_val 📖	mathematical	—	Algebra.Generators.val Algebra.Presentation.toGenerators Algebra.PreSubmersivePresentation.toPresentation toPreSubmersivePresentation Finite.of_fintype PUnit.fintype ofSubsingleton AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	Finite.of_fintype
ofSubsingleton_σ' 📖	mathematical	—	Algebra.Generators.σ' Algebra.Presentation.toGenerators Algebra.PreSubmersivePresentation.toPresentation toPreSubmersivePresentation Finite.of_fintype PUnit.fintype ofSubsingleton MvPolynomial CommRing.toCommSemiring AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing MvPolynomial.instCommRingMvPolynomial	—	Finite.of_fintype
reindex_toPreSubmersivePresentation 📖	mathematical	—	toPreSubmersivePresentation reindex Algebra.PreSubmersivePresentation.reindex	—	—

---

← Back to Index