← all areas

Namespace RingHom 41 theorems

— 36 · Etale 1 · Finite 1 · Flat 2 · QuasiFinite 1

directly in RingHom 36

• Extending a character along an integral extension into an algebraically closed field RingHom.exists_comp_algebraMap_eq_of_isIntegral_of_isAlgClosed 0 below · cited by 8 · depth 9
• Values of a ring map on a module-finite algebra generate a finite extension RingHom.finiteDimensional_adjoin_range_of_finite_of_forall_mem_range 0 below · cited by 13 · depth 9
• Extending a character along an integral extension with prescribed kernel RingHom.exists_comp_algebraMap_eq_and_ker_eq_of_isIntegral_of_isAlgClosed 0 below · cited by 2 · depth 10
• Surjections acting on a nontrivial free module are bijective RingHom.bijective_of_surjective_of_smul_eq 0 below · cited by 1 · depth 11
• Reducedness of A/(kerσ₀+kerσ₁) for p-th-power crossing RingHom.isReduced_quotient_ker_sup_ker_of_exists_apply_eq_pow 0 below · cited by 2 · depth 13
• Equal-kernel homomorphisms to a field differ by a Frobenius power RingHom.exists_forall_eq_pow_prime_pow_of_ker_eq_of_finite_range 0 below · cited by 1 · depth 14
• Unique ring map from a product of rings ℤ[1/dₐ] RingHom.existsUnique_apply_eq_of_completeOrthogonalIdempotents_of_corner_denominators 0 below · cited by 1 · depth 17
• Affine quotient by a finite locally free equivalence relation RingHom.isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation 0 below · cited by 1 · depth 19
• Complex roots of unity lie in the image of σ RingHom.mem_range_of_pow_eq_one 0 below · cited by 2 · depth 19
• Finite faithful flatness over a subalgebra with reduced fibre RingHom.finite_and_faithfullyFlat_of_isReduced_baseChange_of_injective_zmodp 5 below · cited by 1 · depth 22
• Open subsets of ℂⁿ contain points with coordinates in σ(F) RingHom.exists_mem_forall_mem_range_of_isOpen 1 below · cited by 2 · depth 23
• Finite faithful flatness over a local E with mathfrak m_E=pE RingHom.finite_and_faithfullyFlat_of_maximalIdeal_eq_span_natCast_of_mem_jacobson 0 below · cited by 1 · depth 23
• Image of an algebraically closed field is dense in ℂ RingHom.denseRange_of_isAlgClosed 0 below · cited by 1 · depth 24
• Formal smoothness and unramifiedness pass to directed unions RingHom.formallySmooth_and_formallyUnramified_of_directed_union 0 below · cited by 2 · depth 25
• Extending a point to an algebraically closed field along an integral map RingHom.exists_comp_eq_and_ker_eq_of_isIntegral_of_isAlgClosed 0 below · cited by 2 · depth 26
• The crossing model is not formally smooth over the base RingHom.not_formallySmooth_of_ringEquiv_adicCompletion_crossingModel 1 below · cited by 3 · depth 26
• Formally smooth local algebras: Ω_{S/A} free on dt RingHom.existsUnique_eq_smul_kaehlerDifferential_D_of_formallySmooth_of_maximalIdeal_eq_map_sup_span 0 below · cited by 1 · depth 27
• Invariant compatible families of formal points descend to R RingHom.existsUnique_forall_quotientMap_comp_eq_of_forall_smul_eq_of_isNoetherianRing 0 below · cited by 1 · depth 27
• Two fraction-field presentations with equal kernels are κ-isomorphic RingHom.exists_algEquiv_comp_eq_of_ker_eq_of_forall_exists_mul_eq 0 below · cited by 15 · depth 27
• Laurent expansion intertwines d/dt with the universal derivation RingHom.laurentSeries_derivative_eq_of_kaehlerDifferential_D_eq_smul 0 below · cited by 1 · depth 27
• Integral power series from a retraction and a cotangent generator RingHom.exists_powerSeries_map_eq_and_constantCoeff_eq_of_retraction_of_ker_le_span_sup_sq 1 below · cited by 1 · depth 28
• Formal étaleness of the coordinate map A[X]→ S, X↦ t RingHom.formallySmooth_and_formallyUnramified_eval2RingHom_of_existsUnique_eq_smul_D 1 below · cited by 2 · depth 28
• Integrality of an element from integrality of its q-expansion RingHom.mem_map_of_powerSeries_map_eq_of_forall_coeff_mem 0 below · cited by 1 · depth 28
• Étale ℤ-algebras with prime residues lie in henselian subrings RingHom.apply_mem_range_algebraMap_of_etale_int_of_henselianLocalRing 1 below · cited by 1 · depth 29
• Maps from a finite-type ring into a directed colimit are eventually equal RingHom.exists_comp_eq_comp_of_finiteType_of_directedSystem 0 below · cited by 2 · depth 29
• Low coefficients in 𝔪 iff membership in Iⁿ + 𝔪 A RingHom.forall_coeff_mem_iff_mem_pow_sup_map_of_forall_coeff_eq_zero_iff 0 below · cited by 2 · depth 29
• A lift of a fibre uniformiser is an étale coordinate RingHom.formallySmooth_and_formallyUnramified_eval2RingHom_of_maximalIdeal_eq_span_pair 3 below · cited by 2 · depth 29
• Ω_{S/A} is free of rank one on dt RingHom.existsUnique_eq_smul_kaehlerDifferential_D_of_formallySmooth_of_maximalIdeal_eq_span_pair 0 below · cited by 1 · depth 30
• Uniqueness of ring maps agreeing on a dense subring RingHom.eq_of_forall_exists_sub_mem_pow_of_comp_eq 0 below · cited by 6 · depth 31
• Casimir element with unit product modulo ℓ RingHom.exists_casimir_map_mul_eq_one_of_surjective_of_forall_map_eq_zero_iff 0 below · cited by 1 · depth 31
• Congruences descend along a ring map intertwining two endomorphisms RingHom.map_sub_self_mem_comap_of_comp_eq 0 below · cited by 5 · depth 32
• Adic completions along a surjection with 𝔭-adically null kernel RingHom.exists_adicCompletion_ringEquiv_of_surjective_of_ker_le_comap_pow 0 below · cited by 6 · depth 34
• Twisted geometric series for a finite-order ring endomorphism RingHom.one_sub_prod_iterate_mul_eq_sum_prod_iterate_mul_iterate_of_apply_eq_mul_add 0 below · cited by 1 · depth 34
• Linear relations over K among φ(k)-valued functions descend to k RingHom.exists_eq_sum_mul_of_forall_sum_mul_eq_zero_of_forall_mem_range 0 below · cited by 2 · depth 37
• Surjectivity criterion for maps out of adically complete rings RingHom.surjective_of_isAdicComplete_of_le_map_sup_sq 0 below · cited by 1 · depth 38
• Flat patching along a fibre product of nilpotent thickenings RingHom.exists_pullbackRing_isPushout_flat_of_isPushout_of_flat_of_surjective_of_isNilpotent 2 below · cited by 1 · depth 44

RingHom.Etale 1

• The Frobenius square of an étale ring map is a pushout RingHom.Etale.isPushout_frobenius 0 below · cited by 1 · depth 29

RingHom.Finite 1

• Finiteness of local rings at a unique prime above its contraction RingHom.Finite.finite_localRingHom_of_forall_comap_eq 0 below · cited by 1 · depth 27

RingHom.Flat 2

• Flatness descends to quotients by an ideal of the base RingHom.Flat.quotientMap 0 below · cited by 1 · depth 33
• Flatness over a fibre product along nilpotent thickenings RingHom.Flat.of_pullbackRing_of_isPushout_of_surjective_of_isNilpotent 0 below · cited by 1 · depth 45

RingHom.QuasiFinite 1

• Quasi-finiteness codescends along faithfully flat ring maps RingHom.QuasiFinite.codescendsAlong_faithfullyFlat 0 below · cited by 1 · depth 20