← all areas

Namespace AlgHom 31 theorems

• The Wiles–Lenstra numerical criterion for R ≅ T AlgHom.bijective_and_exists_presentation_of_length_cotangent_le 11 below · cited by 3 · depth 8
• Nonzero congruence ideal for a reduced augmented algebra AlgHom.congruenceIdeal_ne_bot_of_isReduced 0 below · cited by 5 · depth 8
• Surjection onto a free algebra with small kernel is injective AlgHom.injective_of_surjective_of_ker_le_map_maximalIdeal 0 below · cited by 2 · depth 9
• Complete intersection gives equality of cotangent and congruence lengths AlgHom.length_cotangent_eq_of_exists_presentation 7 below · cited by 3 · depth 9
• Monotonicity of cotangent length and congruence ideal under surjections AlgHom.length_cotangent_le_and_congruenceIdeal_le_of_surjective 0 below · cited by 2 · depth 9
• Easy inequality of the Wiles–Lenstra numerical criterion AlgHom.length_quotient_congruenceIdeal_le_length_cotangent 0 below · cited by 2 · depth 10
• Numerical criterion transported across a level change AlgHom.bijective_and_free_of_length_le_of_levelChange 21 below · cited by 2 · depth 11
• Equality d ℓ(Φ_R)=ℓ(Ω) for complete intersections with free M AlgHom.length_cotangent_mul_eq_length_quotient_of_free 9 below · cited by 2 · depth 11
• Numerical criterion with pairing: R=T complete intersection, M free AlgHom.bijective_and_free_of_length_le 19 below · cited by 1 · depth 12
• Base change preserves convolution of bialgebra points AlgHom.liftEquiv_symm_withConv_mul 0 below · cited by 8 · depth 12
• Numerical criterion with a Hecke module: R=T and M[wp]=IM AlgHom.bijective_and_torsionBySet_eq_smul_of_length_le 15 below · cited by 1 · depth 13
• Maps from a finite product to a domain factor through a projection AlgHom.exists_eq_comp_evalAlgHom_of_isDomain 0 below · cited by 1 · depth 13
• Intertwining R-algebra map from generators, via faithful action AlgHom.exists_intertwiner_of_adjoin_eq_top_of_injective 0 below · cited by 1 · depth 14
• Finite k-algebra maps between domains with common fraction field are injective AlgHom.injective_of_finite_of_isFractionRing 1 below · cited by 1 · depth 16
• Algebra maps into a field from a d-split algebra AlgHom.nonempty_equiv_fin_of_tensorProduct_algEquiv_pi 0 below · cited by 4 · depth 16
• Extension criterion for points along a p-isogeny with augmentation AlgHom.comp_injective_and_exists_comp_eq_iff_of_sub_one_mem_span_of_mul_sub_eq_zero 0 below · cited by 1 · depth 17
• Rigidity of maps from a formally unramified algebra AlgHom.eq_of_forall_sub_mem_of_le_jacobson_of_formallyUnramified 0 below · cited by 4 · depth 17
• Transitivity of Aut_K(Ω) on K-embeddings into Ω AlgHom.exists_algEquiv_comp_eq_of_isAlgClosed 0 below · cited by 2 · depth 17
• Image of a k(X)-valued map integral over k[b₀] AlgHom.range_eq_range_aeval_X_of_isIntegral_adjoin_singleton 0 below · cited by 1 · depth 18
• Lifting residue-field points of a finite flat algebra AlgHom.exists_residue_comp_eq_of_moduleFinite_of_flat_of_isAlgClosed_fractionRing 0 below · cited by 2 · depth 21
• Injectivity of algebra maps from domains of transcendence degree ≤ 1 AlgHom.injective_of_trdeg_le_one_of_exists_transcendental 0 below · cited by 2 · depth 22
• Points of a finite reduced algebra over an algebraically closed field AlgHom.natCard_eq_finrank_of_isReduced_of_isAlgClosed 0 below · cited by 11 · depth 24
• Cotangent functionals of an augmentation and lifts to the trivial square-zero extension AlgHom.existsUnique_lift_trivSqZeroExt_of_cotangent_linearMap 0 below · cited by 3 · depth 25
• Lifts of an augmentation factor through the cotangent module AlgHom.exists_cotangent_linearMap_of_fst_eq 0 below · cited by 3 · depth 25
• Points separating K-algebra maps into a split algebra AlgHom.eq_of_forall_comp_eq_of_injective_lift_pi 0 below · cited by 1 · depth 26
• Lifting K-points along a faithfully flat finite K-algebra AlgHom.exists_comp_eq_of_faithfullyFlat_of_isAlgClosed 0 below · cited by 1 · depth 29
• Factoring a compatible pair through a compositum AlgHom.exists_ringHom_comp_eq_of_closure_range_union_eq_top_of_forall_sum_mul_eq_zero 0 below · cited by 2 · depth 29
• Kernel of a transcendental A₀-algebra map is a minimal prime AlgHom.ker_mem_minimalPrimes_of_transcendental_of_isIntegral_adjoin_singleton 0 below · cited by 4 · depth 34
• Equal kernels: both A-algebra maps factor through φ₁(B) AlgHom.exists_rangeRestrict_factor_of_ker_eq 0 below · cited by 1 · depth 36
• Endomorphisms congruent to the identity modulo a square-zero ideal AlgHom.bijective_and_comap_eq_of_forall_sub_mem_map_of_mul_eq_bot 0 below · cited by 1 · depth 37
• Transitive automorphism action makes #Hom_k(B,k) divide dim_k B AlgHom.natCard_dvd_finrank_of_forall_exists_comp_algEquiv_eq_of_isAlgClosed 0 below · cited by 1 · depth 40