← all areas

Namespace LinearMap 59 theorems

— 55 · BilinForm 4

directly in LinearMap 55

• Characteristic polynomial of a rank-two endomorphism LinearMap.charpoly_of_finrank_eq_two 0 below · cited by 11 · depth 8
• Characteristic polynomial of a rank-two endomorphism: coefficient criterion LinearMap.charpoly_eq_iff_of_finrank_eq_two 1 below · cited by 3 · depth 9
• Trace and determinant are invariant under semiconjugation LinearMap.trace_eq_and_det_eq_of_semiconj 0 below · cited by 1 · depth 9
• Trace from a quadratic relation and the determinant in rank two LinearMap.trace_eq_of_sq_sub_smul_add_eq_zero_of_det_eq 1 below · cited by 2 · depth 9
• Diagonality of a tame inertia operator in a Frobenius eigenbasis LinearMap.exists_apply_basis_eq_smul_of_mul_eq_pow_mul_of_toMatrix_sub_one_mem 1 below · cited by 1 · depth 11
• Hensel eigenbasis for a rank-2 endomorphism with distinct residual eigenvalues LinearMap.exists_basis_apply_eq_smul_of_charpoly_map_residue_eq 6 below · cited by 1 · depth 11
• Rank-two unipotent endomorphism has charpoly (X-1)² LinearMap.charpoly_eq_X_sub_one_sq_of_sub_one_mul_self_eq_zero 0 below · cited by 2 · depth 14
• Nakayama: injective map with 𝔪-divisible cokernel is an isomorphism on coinvariants LinearMap.exists_linearEquiv_quotient_smul_top_and_finrank_eq_of_injective_of_smul_top_eq_top 0 below · cited by 1 · depth 14
• Kernel of the dual map has the same dimension LinearMap.finrank_ker_dualMap_eq_finrank_ker 0 below · cited by 1 · depth 16
• Additivity of dimker-dimcoker in short exact sequences LinearMap.finrank_ker_sub_finrank_quotient_range_eq_add_of_exact 0 below · cited by 4 · depth 17
• Burnside spanning and traces under base change LinearMap.baseChange_free_finrank_two_and_span_eq_top_and_trace_eq 0 below · cited by 2 · depth 18
• Clearing denominators: ι ∘ j = a J with j injective LinearMap.exists_injective_comp_eq_smul_of_forall_exists_smul_mem_range 0 below · cited by 1 · depth 18
• Kernel of a base-changed integral endomorphism and vₚ(det) LinearMap.finrank_ker_baseChange_le_padicValInt_det 0 below · cited by 1 · depth 18
• Transfer of ker d⁰ and ker dⁱ⁺¹/im dⁱ along a degreewise isomorphism LinearMap.nonempty_kerModRange_equiv_of_equiv_comm 0 below · cited by 7 · depth 18
• Duality preserves exactness of linear maps over a field LinearMap.exact_dualMap_of_exact 0 below · cited by 2 · depth 19
• Euler characteristic of a nine-term exact sequence of k-vector spaces LinearMap.finrank_even_eq_finrank_odd_of_nineTerm_exact 0 below · cited by 1 · depth 19
• At most one dimension for a simultaneous Hecke eigenspace LinearMap.finrank_iInf_eigenspace_le_one_of_coeff_hecke_law 0 below · cited by 1 · depth 19
• Pointwise limits of linear maps on a finite-dimensional function space are eventually injective LinearMap.exists_forall_eq_zero_of_tendsto_apply_of_finiteDimensional 0 below · cited by 3 · depth 20
• Integer points avoiding finitely many affine hyperplanes LinearMap.exists_int_forall_apply_ne 0 below · cited by 3 · depth 20
• Integer points avoiding finitely many linear conditions LinearMap.exists_int_forall_apply_notMem 1 below · cited by 2 · depth 20
• Fibrewise surjectivity is open when the cokernel is finitely generated LinearMap.isOpen_setOf_surjective_baseChange_residueField 0 below · cited by 2 · depth 20
• Power sums of charpoly roots equal traces of powers LinearMap.sum_roots_charpoly_map_pow_eq_trace_pow 0 below · cited by 2 · depth 20
• Common kernel of translates of an I-invariant linear form LinearMap.exists_submodule_mem_iff_forall_apply_eq_zero_of_forall_comp_eq_of_normal 0 below · cited by 1 · depth 23
• Generic bijectivity persists under extension of the domain LinearMap.bijective_baseChange_baseChange_of_bijective_baseChange_fractionRing 0 below · cited by 1 · depth 24
• Kernel of a map A^r → torsion module is free of rank r LinearMap.exists_injective_range_eq_ker_of_isTorsion 0 below · cited by 1 · depth 24
• Isogeny invariance of cokernel length over a DVR LinearMap.length_quotient_range_eq_of_injective_of_comp_eq_comp 0 below · cited by 1 · depth 25
• Semilinear Fitting count: #{Uv=Sv}=p^{dim W} LinearMap.natCard_setOf_apply_eq_frobeniusSemilinear_eq_pow_finrank_iInf_range_pow 2 below · cited by 1 · depth 25
• Perfectness of a pairing descends from the residue field LinearMap.bijective_and_flip_bijective_of_baseChange_residueField 0 below · cited by 1 · depth 26
• Surjection with acyclic kernel induces isomorphisms on cohomology LinearMap.exists_ker_linearEquiv_and_quotient_linearEquiv_of_surjective_of_forall_exact 0 below · cited by 4 · depth 26
• Alternating sum of dimensions along a long exact sequence LinearMap.sum_neg_one_pow_mul_finrank_eq_zero_of_exact 0 below · cited by 1 · depth 27
• Finiteness of ker d₁ and coker d₁ in a ladder of two-term complexes LinearMap.finiteDimensional_ker_and_quotient_range_of_exact_of_finiteDimensional 0 below · cited by 1 · depth 28
• Openness of the isomorphism locus of u : A^m → M LinearMap.isOpen_setOf_bijective_baseChange_residueField_and_forall_bijective_baseChange_iff 1 below · cited by 1 · depth 30
• Descent of linear maps along K ∩ ̂ O = O LinearMap.existsUnique_baseChange_eq_of_isFractionRing_of_forall_rTensor_apply_eq 0 below · cited by 1 · depth 31
• Gluing a linear map from locally representable stalk maps LinearMap.exists_forall_localizedModule_mk_eq_of_forall_exists_chart 1 below · cited by 1 · depth 33
• Stone–von Neumann–Mackey over a ring, Zariski-locally LinearMap.exists_span_eq_top_forall_exists_bijective_and_apply_eq_of_comp_eq_smul_comp 0 below · cited by 1 · depth 33
• Kernel and cokernel torsion bounds under flat base change LinearMap.forall_smul_eq_zero_of_baseChange_eq_zero_and_forall_exists_baseChange_eq_smul_of_flat 0 below · cited by 2 · depth 33
• Trace defect of a quadratic endomorphism in dimension two LinearMap.trace_sub_mul_sq_sub_eq_zero_of_finrank_eq_two 0 below · cited by 1 · depth 33
• Flat base change of torsion bounds for a two-term complex LinearMap.forall_smul_eq_zero_and_forall_exists_eq_smul_of_ker_of_equiv_baseChange_of_flat 1 below · cited by 1 · depth 34
• Index of the image equals q^{ ord(det f)} LinearMap.index_range_eq_card_residueField_pow_of_associated_det_pow 1 below · cited by 2 · depth 34
• Smith normal form with at most r non-unit factors LinearMap.exists_basis_apply_eq_smul_and_isUnit_and_card_le_of_finrank_ker_baseChange_le 0 below · cited by 2 · depth 35
• Coherent lifts with prescribed restriction to the relation module LinearMap.exists_forall_comp_eq_comp_subtype_eq_of_forall_sub_mem_pow_smul_sup_range 0 below · cited by 1 · depth 35
• Index of varpi^s M in f⁻¹(varpi^s M) equals q^{min(s,m)} LinearMap.relIndex_pow_smul_top_comap_eq_card_pow_min_of_finrank_ker_baseChange_le_one 1 below · cited by 2 · depth 35
• Two maps of extensions agreeing on the ends differ uniquely LinearMap.existsUnique_sub_eq_comp_comp_of_extension 0 below · cited by 2 · depth 36
• Two presentations give Jⁿ⁺¹-congruent classes after a uniform shift LinearMap.exists_forall_exists_finAppend_mkQ_sub_mkQ_mem_pow_smul_top 1 below · cited by 1 · depth 36
• Flat base change of the Ext¹-quotient of a presentation LinearMap.exists_isBaseChange_extQuot_of_flat_of_surjective 0 below · cited by 1 · depth 36
• Flat base change of the relation module of a finite free presentation LinearMap.exists_isBaseChange_ker_span_range_eq_top_of_flat 0 below · cited by 1 · depth 36
• Compatible lifts of a presentation along a J-adic tower LinearMap.exists_lifts_comp_eq_forall_comp_eq_comp_subtype_sub_mem_pow_smul_top 2 below · cited by 1 · depth 36
• Presentation-independence of the Ext¹-quotient LinearMap.exists_linearEquiv_extQuot_forall_comp_eq_of_surjective 0 below · cited by 1 · depth 36
• Bijectivity from bijectivity of all residue base changes LinearMap.bijective_of_forall_bijective_baseChange_quotient_maximal 0 below · cited by 1 · depth 37
• Uniform Artin–Rees lifting of maps into N/IⁿN LinearMap.exists_forall_exists_mkQ_comp_eq_factor_comp 1 below · cited by 2 · depth 37
• Artin–Rees for Hom modules LinearMap.exists_forall_mem_pow_smul_top_of_range_le_pow_smul 0 below · cited by 6 · depth 37
• Additivity of Euler characteristic along a long exact sequence LinearMap.finite_and_sum_finrank_eq_of_exact_of_exact_of_exact 0 below · cited by 1 · depth 37
• Quasi-isomorphism transfers cohomology dimensions to a finite complex LinearMap.finrank_ker_eq_and_finrank_add_finrank_eq_of_quasiIso 0 below · cited by 1 · depth 37
• Defect of two compatible comparison maps is I-adically Cauchy LinearMap.exists_forall_sub_eq_comp_comp_and_sub_mem_pow_smul_top_of_comp_eq_of_comp_eq 3 below · cited by 1 · depth 38
• Compatible maps into Artin–Rees quotients lift Cauchy-wise LinearMap.exists_forall_sub_mem_pow_smul_top_and_mkQ_comp_eq_of_compatible 2 below · cited by 1 · depth 39

LinearMap.BilinForm 4

• A coisotropic stable subspace plus ideal image cannot exhaust V LinearMap.BilinForm.sup_iSup_range_ne_top_of_orthogonal_le_of_finrank_ker_aeval_eq_two_mul 0 below · cited by 1 · depth 23
• Orthogonal of the toric part lies in toric + old LinearMap.BilinForm.orthogonal_le_sup_of_restrict_nondegenerate_of_forall_sub_mem_sup 0 below · cited by 1 · depth 27
• Maximal isotropic subspace equals its orthogonal; V/A ≅ A^∨ LinearMap.BilinForm.forall_mem_of_forall_apply_eq_zero_and_exists_quotient_equiv_dual_of_isotropic_of_card_sq_eq 0 below · cited by 1 · depth 29
• Orthogonal of a subspace moved onto by a similitude LinearMap.BilinForm.orthogonal_le_of_similitude_of_forall_map_sub_mem 0 below · cited by 1 · depth 31