← all areas

Namespace Module 212 theorems

— 93 · Basis 5 · End 34 · FaithfullyFlat 15 · Finite 7 · FinitePresentation 1 · Flat 25 · Free 1 · Grassmannian 11 · Invertible 12 · IsDirectLimit 3 · Projective 5

directly in Module 93

• Freeness from a full-length weakly regular sequence Module.free_of_isWeaklyRegular_of_isRegular_ofList_eq_maximalIdeal 0 below · cited by 2 · depth 9
• Length bound for additive trace-zero families on inertia Module.length_quotient_le_of_inertia_additive_family 0 below · cited by 1 · depth 12
• Length bound by q²-1 for a Leibniz family on unipotent inertia Module.length_quotient_le_of_inertia_leibniz_family 0 below · cited by 1 · depth 12
• Congruence module length growth along an adjoint pair Module.length_quotient_torsionBySet_sup_eq_add_of_map_torsionBySet_eq 0 below · cited by 1 · depth 12
• Equality in the congruence-module bound iff M[wp]=I· M Module.length_quotient_torsionBySet_sup_eq_iff 0 below · cited by 2 · depth 12
• Freeness over T from saturation, duality and rank equality Module.free_of_torsionBySet_eq_annihilator_smul 0 below · cited by 1 · depth 13
• Length of M/K bounded by length of N when ker f ⊆ K Module.length_quotient_le_of_ker_le 0 below · cited by 1 · depth 13
• Elements outside a maximal ideal act bijectively on modules killed by a power of it Module.bijective_smul_of_notMem_of_isMaximal_of_pow_smul_eq_bot 0 below · cited by 1 · depth 14
• Local freeness near a point with integrally closed local ring of dimension ≤ 1 Module.exists_notMem_and_free_localizedModule_of_isIntegrallyClosed_of_ringKrullDim_le_one 0 below · cited by 1 · depth 14
• Regular sequence generating 𝔪 forces freeness Module.free_of_isRegular_of_span_eq_maximalIdeal 0 below · cited by 4 · depth 14
• Length bound for M/(M[wp]+M[I]) via the congruence ideal Module.length_quotient_torsionBySet_sup_le 0 below · cited by 1 · depth 14
• Finite module without P-torsion is killed outside P Module.exists_notMem_forall_smul_eq_zero_of_isMaximal_of_forall_smul_eq_zero_imp 0 below · cited by 1 · depth 15
• Idempotent element projecting a finite submodule onto its P-primary part Module.exists_smul_smul_eq_and_smul_eq_iff_mem_iSup_torsionBySet_pow_of_finite 1 below · cited by 1 · depth 15
• Finite flat modules of constant stalk rank are finitely presented Module.finitePresentation_of_rankAtStalk_eq 0 below · cited by 3 · depth 15
• Local criterion for flatness via Tor₁ Module.flat_of_isLocalHom_of_isNoetherianRing_of_finite_of_tor_one_residueField_isZero_univ 0 below · cited by 1 · depth 15
• Rank at stalk is invariant under local isomorphism Module.rankAtStalk_eq_of_forall_localizedModule_equiv 0 below · cited by 2 · depth 15
• Freeness up to finite index from constant eigen-lattice rank Module.exists_injective_linearMap_pi_and_smul_mem_range_of_finrank_torsionBySet_eq_mul 0 below · cited by 1 · depth 16
• Characters of the operator algebra give eigenvectors after base change Module.exists_ne_zero_forall_baseChange_eq_smul_of_algHom 0 below · cited by 3 · depth 16
• Two generators modulo kerπ from an adjoint duality Module.exists_span_pair_union_ker_smul_eq_top_of_dualPairing_of_torsion_le_two 0 below · cited by 1 · depth 16
• Rank of the kerχ-torsion submodule after base change Module.finrank_torsionBySet_ker_eq_finrank_quotient_mul_finrank_iInf_eigenspace_baseChange 0 below · cited by 3 · depth 16
• Local criterion for flatness via Tor₁^R(κ_R,M) Module.flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField 0 below · cited by 3 · depth 16
• Local criterion for flatness via Tor₁ over the residue field Module.flat_of_isLocalHom_of_isNoetherianRing_of_finite_of_tor_one_residueField_isZero 0 below · cited by 1 · depth 16
• Freeness over a local algebra from a rank count Module.free_and_finrank_eq_of_finrank_eq_mul_of_finrank_residueField_tensor_le 0 below · cited by 1 · depth 16
• Galois descent: a semilinear action with open stabilisers has a fixed basis Module.exists_basis_forall_semilinear_apply_eq_of_isGalois 1 below · cited by 2 · depth 17
• Characters of a faithful finite algebra have eigenvectors Module.exists_ne_zero_forall_smul_eq_smul_of_algHom 0 below · cited by 3 · depth 17
• Constant rank descends along a square-zero quotient Module.finrank_baseChange_eq_of_quotient_squareZero_linearEquiv 0 below · cited by 1 · depth 17
• Constant stalk rank one gives one-dimensional fibre over any field Module.finrank_baseChange_eq_one_of_rankAtStalk_eq_one 0 below · cited by 1 · depth 17
• Degree of a power of a finite map: rank nm Module.free_and_finrank_tensorProduct_quot_span_tmul_pow_sub_eq_mul 0 below · cited by 1 · depth 17
• Matching ℚ- and ℤₚ-bases across a base-change isomorphism Module.exists_basis_rat_eq_basis_padicInt_of_linearEquiv_baseChange 2 below · cited by 1 · depth 18
• Generic fibre of a faithful module with a quadratic relation Module.exists_isArtinianRing_isReduced_faithful_baseChange_of_quadraticRelation 0 below · cited by 1 · depth 18
• Local criterion for flatness at a contracted prime Module.flat_of_comap_maximalIdeal_rTensor_injective 0 below · cited by 2 · depth 18
• Guralnick's lifting theorem for varpi-torsion-free modules Module.nonempty_linearEquiv_of_forall_exists_quotient_pow_smul_linearEquiv 0 below · cited by 1 · depth 18
• Depth is bounded by dim R/𝔭 for associated primes Module.depth_le_ringKrullDim_quotient_of_mem_associatedPrimes 0 below · cited by 1 · depth 19
• Depth drops by one modulo an M-regular element of 𝔪 Module.depth_quotSMulTop_succ_eq 0 below · cited by 2 · depth 19
• Depth is unchanged under passing to a quotient ring Module.depth_quotient_eq_depth 0 below · cited by 1 · depth 19
• Constant fibre rank gives a basis after inverting one element Module.exists_forall_notMem_and_linearIndependent_and_smul_mem_span_of_finrank_baseChange_eq 0 below · cited by 1 · depth 19
• Degree-zero cohomology and base change when H¹ vanishes Module.ker_baseChange_field_of_subsingleton_H1 6 below · cited by 1 · depth 19
• Mumford's truncation of a bounded flat complex Module.exists_mumfordTruncation_of_flat_complex 3 below · cited by 1 · depth 20
• Dimension of a faithfully flat algebra trivialised by base change Module.finrank_eq_mul_of_tensorProduct_linearEquiv_baseChange 0 below · cited by 2 · depth 20
• Degree-zero base change to a field with vanishing H¹ Module.ker_baseChange_field_of_subsingleton_H1_of_projective 1 below · cited by 1 · depth 20
• Base change in degree 0 for a complex with finite free tail Module.free_coker_and_ker_baseChange_of_ker_le_range_residueField 0 below · cited by 1 · depth 21
• Counting 𝔪-torsion in M/pM via base change to k Module.card_torsionBySet_quotient_natCast_smul_top_eq_pow_finrank_iInf_ker_baseChange 0 below · cited by 1 · depth 22
• Joint kernel dimension is invariant under field extension Module.finrank_iInf_ker_baseChange_eq_finrank_iInf_ker 0 below · cited by 1 · depth 22
• Adapted basis for a nested pair of p-integral lattices Module.exists_basis_padicValRat_apply_nonneg_iff_pair 0 below · cited by 2 · depth 24
• Normal domains finite over regular local rings of dimension ≤ 2 are free Module.free_of_isIntegrallyClosed_of_finite_of_isRegularLocalRing_of_ringKrullDim_le_two 11 below · cited by 10 · depth 24
• Noether–Deuring theorem over a finite base field Module.nonempty_linearEquiv_of_linearEquiv_baseChange_of_finite 0 below · cited by 1 · depth 27
• Constant fibre dimension over a reduced ring implies projectivity Module.projective_of_isReduced_of_finrank_fiber_const 0 below · cited by 1 · depth 27
• Chain of surjections of torsion modules over a DVR eventually bijective Module.exists_forall_bijective_of_forall_surjective_of_forall_smul_pow_eq_zero 0 below · cited by 1 · depth 28
• Depth is bounded by Krull dimension Module.depth_le_ringKrullDim 0 below · cited by 1 · depth 30
• Projective finite modules are free on a basic open Module.exists_away_forall_nonempty_basis_tensorProduct_of_projective_of_finite 0 below · cited by 1 · depth 30
• A common regular element in 𝔪 for two modules Module.exists_mem_maximalIdeal_isSMulRegular_isSMulRegular 0 below · cited by 1 · depth 30
• Finite principal Zariski covers are faithfully flat Module.faithfullyFlat_pi_localizationAway_of_span_eq_top 0 below · cited by 2 · depth 30
• Equal residue- and generic-fibre dimensions force freeness Module.free_and_finrank_eq_of_finrank_residueField_tensor_eq_of_finrank_fractionRing_tensor_eq 0 below · cited by 2 · depth 30
• Finite modules of depth dim R over regular local rings are free Module.free_of_depth_eq_ringKrullDim_of_isRegularLocalRing 0 below · cited by 2 · depth 30
• Depth is invariant under module-finite local base change Module.depth_eq_depth_of_finite_of_isLocalHom 0 below · cited by 1 · depth 31
• Rank is unchanged modulo a regular element Module.finrank_quotSMulTop_eq 3 below · cited by 1 · depth 31
• Freeness descends from M/xM along a regular element Module.free_of_quotSMulTop_free 3 below · cited by 1 · depth 31
• Unique compatible lift along an I-adic tower Module.existsUnique_compatible_lift_of_range_eq_ker_of_ker_le_pow_smul 0 below · cited by 2 · depth 32
• Surjectivity after base change spreads from a single fibre Module.exists_forall_isUnit_surjective_baseChange_of_surjective_baseChange_residueField 0 below · cited by 1 · depth 32
• Adic systems: the kernel system is the kernel module's truncation Module.exists_forall_surjective_ker_eq_pow_smul_top_of_adic_of_range_eq_ker 3 below · cited by 1 · depth 32
• Zariski-local criterion for ker(δ⊗ A) finite projective of rank r Module.finite_projective_ker_baseChange_of_forall_exists_isUnit 0 below · cited by 1 · depth 32
• Descent of exactness and ker dimension along K ⊆ K' Module.ker_baseChange_le_range_and_finrank_eq_of_field_extension 0 below · cited by 1 · depth 32
• Locally constant rank after inverting one more element Module.exists_forall_isUnit_rankAtStalk_baseChange_eq_finrank_residueField_tensor 0 below · cited by 1 · depth 33
• Universal ideal for rank-r local freeness after base change Module.exists_ideal_forall_projective_and_rankAtStalk_eq_iff 0 below · cited by 1 · depth 33
• A power of J kills ker u and coker u Module.exists_pow_smul_ker_eq_zero_and_pow_smul_le_range_of_forall_exists_pow_smul 0 below · cited by 1 · depth 33
• Inverse limit of an I-adic system of modules Module.exists_submodule_pi_forall_surjective_ker_eq_pow_smul_top_of_adic_system 0 below · cited by 1 · depth 33
• Two-term free model computing ker d⁰ after base change Module.exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex 0 below · cited by 1 · depth 33
• Closedness of the locus where im f ⊆ 𝔭 Q Module.isClosed_setOf_range_le_smul_top 0 below · cited by 2 · depth 33
• Lifting a basis of M/π M to a basis of M Module.exists_basis_coe_eq_of_isAdicComplete_of_isHausdorff_of_isSMulRegular 1 below · cited by 1 · depth 34
• Faithful flatness of a product over a basic open cover Module.faithfullyFlat_pi_of_forall_faithfullyFlat_localizationAway_of_span_eq_top 0 below · cited by 2 · depth 34
• Cokernel of a map to a finite free module is free when residual relations lift Module.free_quotient_range_of_ker_baseChange_residueField_le 0 below · cited by 1 · depth 34
• Independence of the zeroth determinantal ideal of a presentation Module.span_det_submatrix_eq_of_ker_eq_span_range 0 below · cited by 1 · depth 34
• Dual family trace equals the constant stalk rank Module.sum_dual_apply_eq_natCast_of_rankAtStalk_eq 1 below · cited by 1 · depth 34
• Local alternating length formula for a bounded free complex Module.toNat_length_ker_add_sum_neg_one_pow_toNat_length_eq_neg_one_pow_mul_toNat_length_quotient 6 below · cited by 1 · depth 34
• Constant Euler characteristic of fibres of a flat complex Module.exists_forall_alternatingSum_finrank_cohomology_baseChange_eq_of_flat_complex_of_isLocalRing 6 below · cited by 1 · depth 35
• Base change of a finite-length module is killed by a power of mathfrak m_B Module.exists_pow_maximalIdeal_smul_top_baseChange_eq_bot_of_isFiniteLength_of_isPrime 0 below · cited by 1 · depth 35
• Descent of finiteness and faithful flatness along faithfully flat base change Module.finite_and_faithfullyFlat_of_faithfullyFlat_tensorProduct 0 below · cited by 1 · depth 35
• Finite-dimensionality and length formula for modules with finite support Module.finite_and_finrank_eq_sum_length_localizedModule_of_forall_subsingleton 0 below · cited by 2 · depth 35
• Acyclicity in degrees below the length of rs Module.forall_eq_zero_and_mem_range_of_isWeaklyRegular_complex 0 below · cited by 1 · depth 35
• Length duality for top cokernels of finite free complexes Module.length_quotient_range_eq_length_dual_quotient_of_isRegular_of_exact 2 below · cited by 1 · depth 35
• Cokernel of d^* is R/I under a kernel-lifting criterion Module.nonempty_dual_quotient_range_dualMap_linearEquiv_quotient_of_forall_surjective_iff 1 below · cited by 1 · depth 35
• Cokernel of the transpose corepresents ker(B ⊗ d) Module.exists_hom_dual_quotient_range_dualMap_linearEquiv_ker_lTensor_natural 0 below · cited by 1 · depth 36
• Mumford's lemma: projective model of a bounded flat complex Module.exists_projective_complex_quasiIso_of_flat_complex 2 below · cited by 3 · depth 36
• Cocycles of a dualised finite free complex compute Ext Module.exists_surjective_linearMap_ext_of_exact_of_free 0 below · cited by 1 · depth 36
• Faithful flatness of a finite product of algebras Module.faithfullyFlat_pi_of_forall_faithfullyFlat 1 below · cited by 1 · depth 36
• Euler characteristic of a bounded complex of finite-dimensional vector spaces Module.finrank_add_alternatingSum_finrank_eq_of_finite_complex 0 below · cited by 1 · depth 36
• Acyclicity over the residue field gives acyclicity after localisation Module.forall_baseChange_localization_eq_zero_and_mem_range_of_forall_baseChange_field 1 below · cited by 1 · depth 36
• Base change preserves quasi-isomorphisms of bounded flat complexes Module.quasiIso_baseChange_of_quasiIso_of_flat 3 below · cited by 3 · depth 36
• Length of Ext^g(N,R) over a regular local ring Module.subsingleton_ext_and_length_ext_eq_length_of_isWeaklyRegular_of_ofList_eq_maximalIdeal 0 below · cited by 1 · depth 36
• Nakayama acyclicity for complexes of finite free modules Module.forall_eq_zero_and_mem_range_of_forall_baseChange_residueField_of_finite_free 0 below · cited by 1 · depth 37
• Upper semicontinuity of Čech cohomology ranks over Spec R Module.isClosed_setOf_le_finrank_cohomology_baseChange_residueField_of_projective 6 below · cited by 1 · depth 37
• Colength of a column span read in a rank-two basis Module.length_quotient_comap_span_columns_eq_length_quotient_range_mulVecLin 0 below · cited by 3 · depth 37
• Local flatness criterion for a finite module over a local extension Module.flat_of_maximalIdeal_rTensor_injective_of_isLocalHom 0 below · cited by 1 · depth 39

Module.Basis 5

• Basis coordinates of elements of I · N lie in I Module.Basis.repr_apply_mem_of_mem_ideal_smul_top 0 below · cited by 1 · depth 10
• Galois conjugation of a common eigenvector of rational operators Module.Basis.exists_forall_apply_eq_ringHom_smul_of_repr_mem_range_ratCast 2 below · cited by 1 · depth 16
• Lifting a mod p common eigenvector to a p-primitive lattice vector Module.Basis.exists_not_exists_eq_smul_and_forall_exists_sub_smul_eq_smul_of_mulVec_eq_smul 1 below · cited by 1 · depth 16
• Rational coordinates from a separating family of rational forms Module.Basis.repr_mem_range_ratCast_of_forall_dual 0 below · cited by 1 · depth 16
• R-linear independence of a triple tensor K-basis Module.Basis.tensorProduct_tensorProduct_linearIndependent_restrictScalars 0 below · cited by 1 · depth 20

Module.End 34

• Trace from a quadratic relation in dimension 2 Module.End.trace_eq_of_mul_self_sub_smul_add_smul_eq_zero 0 below · cited by 1 · depth 9
• Common eigenvector for a commuting family of endomorphisms Module.End.exists_forall_apply_eq_smul_of_pairwise_commute 0 below · cited by 4 · depth 10
• Characters of a ring stabilising a faithful lattice are eigenvalue systems Module.End.exists_ne_zero_forall_apply_eq_smul_of_ringHom 0 below · cited by 1 · depth 10
• Common eigenspaces in the complexification of a real lattice Module.End.finrank_iInf_eigenspace_baseChange_complex_eq_add 0 below · cited by 3 · depth 13
• Common eigenspace dimension is invariant under field base change Module.End.finrank_iInf_eigenspace_baseChange_eq 0 below · cited by 3 · depth 13
• Regular semisimple element with trace-zero centraliser vector outside U Module.End.exists_charpoly_eq_and_commute_and_trace_eq_zero_and_notMem_of_irreducible 0 below · cited by 1 · depth 14
• Dichotomy for joint eigenvectors along an exact window Module.End.exists_eigenvector_or_exists_eigenvector_of_dualMap_comp_eq_smul 3 below · cited by 1 · depth 16
• Killing all common eigenvectors forces nilpotence Module.End.isNilpotent_of_mem_adjoin_of_forall_eigenvector_apply_eq_zero 1 below · cited by 2 · depth 16
• Joint eigenvectors exist iff joint dual eigenvectors exist Module.End.exists_ne_zero_forall_apply_eq_smul_iff_exists_ne_zero_forall_dualMap_apply_eq_smul 1 below · cited by 1 · depth 17
• Joint eigenvectors lift from a quotient to the whole space Module.End.exists_ne_zero_forall_apply_eq_smul_of_forall_sub_smul_mem 0 below · cited by 1 · depth 17
• Adjoin of commuting semisimple endomorphisms: semisimple and reduced Module.End.forall_isSemisimple_and_isReduced_adjoin_of_commute 0 below · cited by 2 · depth 17
• Geometric sums of a finite-order endomorphism vanish in characteristic p Module.End.sum_range_pow_eq_zero_of_pow_eq_one_of_mul_dvd 0 below · cited by 1 · depth 17
• Common eigenvector for a commuting family of endomorphisms Module.End.exists_common_eigenvector_of_commute 1 below · cited by 3 · depth 18
• From a simultaneous dual eigenvector to a simultaneous eigenvector Module.End.exists_ne_zero_forall_apply_eq_smul_of_dual_comp_eq_smul 0 below · cited by 1 · depth 18
• Idempotent-like operators from scalar actions separating indices Module.End.exists_mem_adjoin_apply_eq_self_and_apply_eq_zero_of_forall_ne_exists_ne 0 below · cited by 1 · depth 19
• Divisor-string modules are cyclic with one-dimensional joint eigenspaces Module.End.mem_span_prod_apply_and_finrank_iInf_eigenspace_le_one_of_divisorString 0 below · cited by 1 · depth 19
• Rank-one freeness and multiplicity one for a commutative operator algebra Module.End.nonempty_basis_fin_one_and_finrank_iInf_eigenspace_eq_one_of_iSupIndep_of_cyclic 0 below · cited by 1 · depth 19
• Dixmier's Schur lemma over ℂ in countable dimension Module.End.rank_le_one_of_countable_of_commute_of_forall_invariant_eq_bot_or_eq_top 0 below · cited by 1 · depth 19
• Dimension bound for the 𝔪-annihilator of a commuting family Module.End.CommFamily.finrank_inf_annPart_le_finrank_mul_of_forall_finrank_inf_iInf_ker_le 0 below · cited by 1 · depth 20
• Joint generalised eigenspace dimensions are independent of the extension field Module.End.finrank_iInf_maxGenEigenspace_baseChange_eq_mul_prod_rootMultiplicity_of_isAlgClosed 0 below · cited by 1 · depth 20
• Semisimplicity of a base change descends and spreads to all extensions Module.End.maxGenEigenspace_baseChange_le_eigenspace_of_isAlgClosed 0 below · cited by 1 · depth 20
• Left ideals of End(M) are double annihilators over ℤ/n Module.End.mem_ideal_of_forall_apply_eq_zero_zmod 0 below · cited by 1 · depth 20
• Joint generalised eigenspace of coordinate operators on a box Module.End.finrank_iInf_maxGenEigenspace_eq_prod_rootMultiplicity_of_apply_eq_sum_update 1 below · cited by 1 · depth 21
• Dimension of simultaneous generalised eigenspaces on a tensor product Module.End.finrank_iInf_maxGenEigenspace_map_tensorProduct_eq_mul 0 below · cited by 1 · depth 22
• Good operators generate at a multiplicity-one eigenvector Module.End.exists_mem_adjoin_aeval_ne_zero_mul_eq_of_ratForm_of_multiplicityOne 0 below · cited by 1 · depth 23
• Rational and analytic characteristic polynomials of a complex torus endomorphism Module.End.exists_monic_map_eq_charpoly_and_charpoly_eq_sq_of_span_real_dual_eq_top 0 below · cited by 1 · depth 24
• Basis of mathfraksl₂-strings from primitive vectors Module.End.exists_primitive_strings_basis_of_sl2_of_iSup_eigenspace_eq_top 0 below · cited by 1 · depth 24
• Common eigen-functional for a commuting family of endomorphisms Module.End.exists_dual_ne_zero_forall_apply_eq_mul_of_commute 0 below · cited by 1 · depth 26
• An endomorphism conjugate to its q-th power is quasi-unipotent Module.End.exists_isNilpotent_pow_sub_one_of_mul_eq_pow_mul_of_isUnit 0 below · cited by 2 · depth 28
• Quasi-unipotent operator commuting with a division algebra has g^e=1 Module.End.pow_eq_one_of_isNilpotent_pow_sub_one_of_forall_commute_of_forall_isUnit_of_finrank_eq 1 below · cited by 2 · depth 28
• Nilpotent endomorphisms commuting with a division algebra vanish Module.End.eq_zero_of_isNilpotent_of_forall_commute_of_forall_isUnit_of_finrank_eq 0 below · cited by 1 · depth 29
• Minkowski–Serre rigidity modulo ℓᵃ≥ 3 Module.End.sub_one_pow_eq_zero_of_pow_sub_one_pow_eq_zero_of_eq_one_add_pow_smul 0 below · cited by 1 · depth 29
• Rigidity of finite-order endomorphisms congruent to 1 mod pᵃ Module.End.eq_one_of_pow_eq_one_of_forall_exists_sub_eq_prime_pow_smul 0 below · cited by 1 · depth 31
• A two-dimensional M₂(k)-module is the standard one Module.End.exists_linearEquiv_forall_algHom_matrix_apply_eq_mulVec_of_finrank_eq_two 0 below · cited by 1 · depth 38

Module.FaithfullyFlat 15

• Split twisted forms of ℤ^G over ℤ are coboundaries Module.FaithfullyFlat.exists_completeOrthogonalIdempotents_eq_sum_tmul_of_isBaseChange 2 below · cited by 1 · depth 16
• Effective descent along an idempotent Amitsur cocycle Module.FaithfullyFlat.exists_submodule_forall_mem_iff_sum_mul_tmul_isBaseChange 1 below · cited by 1 · depth 16
• Amitsur 1-cocycles of units split when Pic R is trivial Module.FaithfullyFlat.exists_eq_inv_tmul_of_amitsur_cocycle 2 below · cited by 1 · depth 17
• Effectivity of descent data for modules along a faithfully flat extension Module.FaithfullyFlat.isBaseChange_eqLocus_of_descentDatum 0 below · cited by 4 · depth 17
• Degree-zero exactness of the Amitsur complex Module.FaithfullyFlat.exists_algebraMap_eq_of_tmul_one_eq_one_tmul 0 below · cited by 3 · depth 20
• Effective faithfully flat descent for modules Module.FaithfullyFlat.exists_submodule_isBaseChange_of_cocycle 1 below · cited by 1 · depth 20
• Flatness plus field-valued points over all maximal ideals gives faithful flatness Module.FaithfullyFlat.of_forall_isMaximal_exists_ringHom_field 0 below · cited by 1 · depth 20
• Finite product over a Zariski cover is faithfully flat, finitely presented Module.FaithfullyFlat.pi_and_finitePresentation_pi_of_span_eq_top 0 below · cited by 2 · depth 30
• Lifting geometric points along a faithfully flat finite-type algebra Module.FaithfullyFlat.exists_ringHom_comp_algebraMap_eq_of_finiteType_of_isAlgClosed 0 below · cited by 2 · depth 32
• Faithful flatness from flat algebras reviving each maximal ideal Module.FaithfullyFlat.of_forall_isMaximal_exists_flat_algebra 0 below · cited by 1 · depth 32
• Geometric points lift along a faithfully flat algebra Module.FaithfullyFlat.exists_isAlgClosed_algebra_isScalarTower_of_isAlgClosed 0 below · cited by 2 · depth 33
• Points with values in fields lift along faithfully flat algebras Module.FaithfullyFlat.exists_ringHom_isAlgClosed_comp_algebraMap_eq 0 below · cited by 3 · depth 33
• Faithful flatness is local on the base Module.FaithfullyFlat.of_isLocalized_span 0 below · cited by 1 · depth 33
• Additive Amitsur 1-cocycles are coboundaries (faithfully flat descent) Module.FaithfullyFlat.exists_eq_tmul_one_sub_one_tmul_of_amitsur_cocycle 0 below · cited by 1 · depth 35
• Faithful flatness of a complete local ring with the same adic quotients Module.FaithfullyFlat.of_isAdicComplete_of_forall_pow_maximalIdeal 0 below · cited by 1 · depth 45

Module.Finite 7

• Finiteness over a precomplete local ring from the special fibre Module.Finite.of_finite_quotient_map_maximalIdeal 0 below · cited by 1 · depth 11
• Finiteness over R of A/I when I contains a polynomial with unit leading coefficient Module.Finite.quotient_of_isUnit_leadingCoeff_of_mem 0 below · cited by 5 · depth 17
• Finiteness sandwich over a Noetherian ring Module.Finite.of_ker_le_range_of_isNoetherianRing 0 below · cited by 3 · depth 19
• Finiteness of an algebra representing idempotents of Q Module.Finite.of_algHom_equiv_isIdempotentElem_tensorProduct_of_etale_of_rankAtStalk_eq 1 below · cited by 1 · depth 29
• Complete Nakayama lemma for adically Hausdorff modules Module.Finite.of_isAdicComplete_of_isHausdorff_of_quotient 0 below · cited by 4 · depth 30
• Compatible families M → N/Iⁿ⁺¹N come uniquely from widehatHom(M,N) Module.Finite.existsUnique_forall_mkQ_comp_eq_of_forall_factor_comp_eq 2 below · cited by 1 · depth 32
• Trace via dual families on finitely generated projective modules Module.Finite.exists_trace_end_eq_sum_dual_apply_of_projective 0 below · cited by 1 · depth 34

Module.FinitePresentation 1

• Spreading a fibre basis to a basic open neighbourhood Module.FinitePresentation.exists_notMem_basis_localizedModule_of_basis_residueField_tensor 0 below · cited by 1 · depth 32

Module.Flat 25

• Miracle flatness for a local map of regular local rings Module.Flat.of_isLocalHom_of_isRegularLocalRing_of_ringKrullDim_quotient_eq_zero 4 below · cited by 7 · depth 15
• Fibrewise criterion of flatness over a general base, affine form Module.Flat.of_finitePresentation_of_forall_flat_residueField_tensorProduct 4 below · cited by 4 · depth 16
• Descent of flatness at a prime to a finitely generated subalgebra Module.Flat.exists_fg_subalgebra_flat_localization_tensorProduct 1 below · cited by 2 · depth 17
• Flatness descends to a finitely generated subalgebra of the base Module.Flat.exists_fg_subalgebra_flat_tensorProduct 4 below · cited by 3 · depth 17
• Fibrewise flatness criterion over a principal ideal domain Module.Flat.of_forall_flat_residueField_tensorProduct_of_isPrincipalIdealRing 1 below · cited by 1 · depth 17
• Openness of the flat locus for finite type algebras Module.Flat.isOpen_setOf_flat_localization_atPrime 2 below · cited by 2 · depth 18
• Nonzerodivisor on all geometric fibres: flatness of B/gB Module.Flat.mem_nonZeroDivisors_and_flat_quotient_span_of_forall_isAlgClosed 0 below · cited by 1 · depth 18
• Generic flatness over a Noetherian domain Module.Flat.exists_ne_zero_flat_localization_tensorProduct 0 below · cited by 3 · depth 19
• Miracle flatness for finite local maps of regular local rings Module.Flat.of_finite_of_isLocalHom_of_isRegularLocalRing_of_ringKrullDim_eq 3 below · cited by 2 · depth 30
• Base change for a bounded complex of flat modules Module.Flat.projective_ker_and_bijective_kerBaseChangeHom_of_forall_ker_baseChange_le_range 5 below · cited by 1 · depth 31
• Universal acyclicity and projectivity near a good fibre Module.Flat.exists_forall_isUnit_projective_ker_baseChange_of_ker_baseChange_residueField_le_range 10 below · cited by 1 · depth 32
• Bounded flat complexes: flatness of ker d⁰ and base change Module.Flat.flat_ker_and_bijective_kerBaseChangeHom_of_forall_ker_le_range 0 below · cited by 4 · depth 32
• Fibrewise exactness implies exactness for bounded flat complexes Module.Flat.ker_le_range_of_forall_isMaximal_ker_baseChange_quotient_le_range 3 below · cited by 2 · depth 32
• Fibrewise exactness of a bounded flat complex spreads out Module.Flat.exists_forall_isUnit_ker_baseChange_le_range_of_ker_baseChange_residueField_le_range 7 below · cited by 1 · depth 33
• Base change of a bounded exact complex of flat modules Module.Flat.ker_baseChange_eq_bot_and_ker_le_range_of_flat_of_exact 2 below · cited by 3 · depth 33
• Kernel of a surjection of flat modules is flat Module.Flat.ker_of_surjective_of_flat 1 below · cited by 3 · depth 33
• Base change of ker d⁰ where g becomes invertible Module.Flat.projective_ker_baseChange_of_isLocalizationAway_of_ker_baseChange_le_range 1 below · cited by 1 · depth 33
• Flat base change commutes with kernels and homology Module.Flat.bijective_kerBaseChangeHom_and_nonempty_homology_baseChange_linearEquiv 0 below · cited by 1 · depth 34
• Exactness over a local ring from exactness on the residue field Module.Flat.ker_baseChange_le_range_of_forall_ker_baseChange_residueField_le_range 5 below · cited by 2 · depth 34
• Left exactness after tensoring when the cokernel is flat Module.Flat.lTensor_injective_of_exact_of_surjective_of_flat 0 below · cited by 3 · depth 34
• Flatness over a finite flat algebra with reduced generic fibre Module.Flat.of_module_fractionRing_of_isReduced_baseChange 0 below · cited by 1 · depth 34
• Flatness descends along a faithfully flat ring extension Module.Flat.of_flat_of_faithfullyFlat_right 0 below · cited by 1 · depth 37
• Truncations of a flat unramified local extension are finite free Module.Flat.finite_free_finrank_quotient_tensorProduct_of_map_maximalIdeal_eq 0 below · cited by 1 · depth 39
• Cocycles in I C₁ come from I C₀ Module.Flat.exists_mem_smul_top_map_eq_of_ker_baseChange_le_range 0 below · cited by 1 · depth 40
• Flatness from flatness modulo all powers of I Module.Flat.of_forall_flat_quotient_pow_tensor_of_map_le_jacobson 0 below · cited by 1 · depth 41

Module.Free 1

• Freeness descends along a surjective ring map compatible with scalars Module.Free.of_surjective_of_smul_eq 0 below · cited by 1 · depth 11

Module.Grassmannian 11

• Representability and projectivity of the Grassmannian of a finite module Module.Grassmannian.exists_scheme_represents_and_isClosedImmersion_toProjSpace 14 below · cited by 2 · depth 32
• Plücker embedding: a represented Grassmannian is projective over R Module.Grassmannian.exists_isClosedImmersion_toProjSpace_of_represents 6 below · cited by 1 · depth 33
• Representability of the Grassmannian functor by affine charts Module.Grassmannian.exists_scheme_represents_and_isAffineOpen_chart_cover 8 below · cited by 1 · depth 33
• Chart of a representing Grassmannian scheme is generated by coordinates Module.Grassmannian.adjoin_eq_top_of_isOpenImmersion_of_opensRange_eq 1 below · cited by 1 · depth 34
• Zariski gluing for the Grassmannian functor over standard opens Module.Grassmannian.existsUnique_forall_map_toAlgHom_eq_of_isLocalization_away 0 below · cited by 1 · depth 34
• The standard Grassmannian chart is represented by Sym_R(M^k)/J Module.Grassmannian.exists_chart_equiv_algHom_symmetricAlgebra_quotient 1 below · cited by 1 · depth 34
• Standard charts from a generating family cover field-valued Grassmannian points Module.Grassmannian.exists_injective_and_bijective_of_span_eq_top 0 below · cited by 2 · depth 34
• Grassmannian charts are open subfunctors Module.Grassmannian.exists_isOpen_forall_bijective_map_iff_range_comap_subset 0 below · cited by 1 · depth 34
• Plücker coordinates on the standard Grassmannian charts Module.Grassmannian.exists_pluckerCoordinate_eq_det_and_bijective_iff_isUnit 1 below · cited by 1 · depth 34
• Standard Grassmannian chart at a k-tuple as linear maps Module.Grassmannian.exists_chart_equiv_linearMap 0 below · cited by 3 · depth 35
• Representability of endomorphism-stable Hopf ideals with rank-k quotient Module.Grassmannian.exists_scheme_represents_isHopfIdeal_and_isClosedImmersion_toProjSpace 17 below · cited by 1 · depth 37

Module.Invertible 12

• Finitely generated projectives of rank one at all fields are invertible Module.Invertible.of_projective_of_forall_finrank_eq_one 0 below · cited by 11 · depth 15
• Faithfully flat descent of invertibility of modules Module.Invertible.of_invertible_tensorProduct_of_faithfullyFlat 0 below · cited by 4 · depth 18
• Invertibility of a module transports along a ring isomorphism Module.Invertible.of_ringEquiv 0 below · cited by 4 · depth 18
• Invertibility of a finitely presented module is local Module.Invertible.of_localization_maximal 1 below · cited by 2 · depth 30
• Invertibility of a module is Zariski-local Module.Invertible.of_isLocalizedModule_of_span_eq_top 0 below · cited by 2 · depth 32
• Bijectivity at a prime of a map of invertible modules Module.Invertible.bijective_localizedModule_map_of_not_range_le 0 below · cited by 8 · depth 33
• Invertible modules are cyclic over a basic open set Module.Invertible.exists_notMem_and_forall_exists_pow_smul_eq_smul 0 below · cited by 1 · depth 33
• Composite equal to a scalar in 𝔭: one image lies in 𝔭 Module.Invertible.range_le_smul_top_or_of_comp_eq_smul 0 below · cited by 7 · depth 33
• Invertibility of a module is Zariski-local Module.Invertible.of_isLocalizedModule_span 0 below · cited by 1 · depth 34
• Saturation over a valuation ring of a co-invertible subspace Module.Invertible.quotient_span_rTensor_mem_and_span_image_eq_of_valuationRing 0 below · cited by 2 · depth 34
• Invertibility is local on a finite basic-open cover Module.Invertible.of_isLocalizedModule_of_span_range_eq_top 1 below · cited by 1 · depth 35
• Invertibility descends along a nilpotent surjection Module.Invertible.of_invertible_baseChange_of_surjective_of_isNilpotent_ker 1 below · cited by 1 · depth 37

Module.IsDirectLimit 3

• Isomorphisms of finitely presented modules descend to a stage Module.IsDirectLimit.exists_linearEquiv_of_finitePresentation 0 below · cited by 1 · depth 18
• Invertible modules over a directed colimit descend to a stage Module.IsDirectLimit.exists_invertible_linearEquiv_baseChange 0 below · cited by 1 · depth 19
• Descent of isomorphisms of finitely presented modules to a stage Module.IsDirectLimit.exists_stage_linearEquiv_of_finitePresentation_compat 0 below · cited by 1 · depth 19

Module.Projective 5

• Finite projective modules lift along a square-zero quotient Module.Projective.exists_baseChange_quotient_iso_of_squareZero 0 below · cited by 1 · depth 17
• Lifting isomorphisms of f.g. projectives along square-zero ideals Module.Projective.exists_linearEquiv_of_baseChange_quotient_of_squareZero_of_compat 0 below · cited by 1 · depth 17
• Lifting isomorphisms of f.g. projectives along a square-zero quotient Module.Projective.nonempty_linearEquiv_of_baseChange_quotient_of_squareZero 0 below · cited by 1 · depth 19
• Finitely generated vanishing ideal of a section of a projective module Module.Projective.exists_ideal_fg_forall_tmul_eq_zero_iff_map_eq_bot 0 below · cited by 1 · depth 35
• Vanishing ideal of an element of a projective module Module.Projective.exists_ideal_forall_tmul_eq_zero_iff_map_eq_bot 0 below · cited by 1 · depth 38