← all areas

Namespace Algebra 302 theorems

Landmarks here: Taylor–Wiles patching: a patched level with zero relation ideal

— 145 · DescentCofaces 1 · Etale 29 · FinitePresentation 4 · FiniteType 6 · FormallyEtale 3 · FormallySmooth 21 · FormallyUnramified 8 · H1Cotangent 2 · IsAlgebraic 1 · IsIntegral 3 · IsInvariant 8 · IsPushout 3 · IsSeparable 3 · IsSmoothAt 2 · IsStandardEtale 3 · IsStandardSmooth 1 · IsStandardSmoothOfRelativeDimension 4 · IsUnramifiedAt 3 · PatchingDatum 5 · PatchingLevel 1 · PointDerivations 4 · QuasiFinite 3 · QuasiFiniteAt 2 · Smooth 8 · TensorProduct 28 · adjoin 1

directly in Algebra 145

• Lifting a complete-intersection presentation from the residue field Algebra.exists_presentation_of_residueField 7 below · cited by 1 · depth 9
• Finite algebras over complete local rings split into local factors Algebra.finite_maximalSpectrum_and_bijective_localization_of_module_finite 2 below · cited by 3 · depth 9
• Flat Taylor–Wiles level tower assembles into a patching datum Algebra.nonempty_patchingDatum_of_flatLevelTower 9 below · cited by 3 · depth 10
• Patching datum from a strict-ordinary Taylor–Wiles level tower Algebra.nonempty_patchingDatum_of_strictOrdinaryLevelTower 9 below · cited by 2 · depth 10
• Taylor–Wiles level data produce a patching datum Algebra.nonempty_patchingDatum_of_levelData 8 below · cited by 2 · depth 11
• Values of mathbf Z_{(ℓ)}-finite algebras lie in places above ℓ Algebra.algHom_apply_mem_valuationSubring_of_finite_ratLocalizedAt_tensor 0 below · cited by 1 · depth 12
• Lifting residue-field points of a finite flat ℤ-algebra Algebra.exists_algHom_residue_comp_eq_of_finite_of_flat_ratLocalizedAt_tensor 0 below · cited by 1 · depth 12
• Points into an algebraically closed field separate elements Algebra.eq_zero_of_forall_algHom_apply_eq_zero_of_isReduced_tensorProduct 0 below · cited by 9 · depth 13
• Finite flat complete intersections over a DVR are Gorenstein Algebra.exists_pairing_of_exists_presentation 4 below · cited by 1 · depth 13
• Generic étaleness of level sets over a local base Algebra.exists_polynomial_isUnit_aeval_imp_etale_levelSet 0 below · cited by 1 · depth 14
• Reduced algebras over a perfect field are geometrically reduced Algebra.isReduced_tensorProduct_of_perfectField 0 below · cited by 12 · depth 14
• Clearing denominators: a nonzero q₀∈ L[f] with q₀z valuation-integral Algebra.exists_adjoin_ne_zero_mul_forall_valuationSubring_mem 0 below · cited by 2 · depth 15
• Reduced finite-dimensional algebras carry a nondegenerate trace form Algebra.exists_linearMap_apply_mul_eq_zero_imp_of_isReduced 0 below · cited by 1 · depth 15
• Norms of integral elements lie in an integrally closed base Algebra.exists_monoidHom_algebraMap_eq_norm_of_isIntegrallyClosed 0 below · cited by 1 · depth 15
• Finiteness of the integral closure of k[x] in a function field Algebra.finite_integralClosure_adjoin_singleton_of_isAlgClosed 0 below · cited by 1 · depth 15
• Level sets of a finite flat coordinate are free of rank d Algebra.levelSet_finite_free_finrank_of_flat_polynomial 0 below · cited by 2 · depth 15
• Norms commute with base change, read in fraction fields Algebra.norm_algebraMap_eq_of_isPushout_of_isFractionRing 1 below · cited by 1 · depth 15
• Norm splitting when F₂⊗_F F₁≅ Z× Z' Algebra.algebraMap_norm_eq_norm_mul_norm_of_adjoin_eq_top 1 below · cited by 2 · depth 16
• Points of a finite algebra bounded by special-fibre dimension Algebra.card_algHom_le_finrank_residueField_tensorProduct 0 below · cited by 1 · depth 16
• Spreading out étaleness away from finitely many primes Algebra.exists_etale_localizationAway_of_forall_isEtaleAt 0 below · cited by 5 · depth 16
• Equal fibre ranks at a finite point and at ∞ Algebra.finrank_quotient_span_sub_eq_of_isLocalization_away_of_mul_eq_one 0 below · cited by 2 · depth 16
• Generic rank equals degree of fraction field extension Algebra.finrank_tensorProduct_eq_finrank_of_isFractionRing_of_finite 0 below · cited by 4 · depth 16
• Norm of a scalar plus a nilpotent element Algebra.norm_eq_pow_finrank_of_isNilpotent_sub_algebraMap 0 below · cited by 2 · depth 16
• Norm of an element of a subsingleton algebra is 1 Algebra.norm_of_subsingleton 0 below · cited by 1 · depth 16
• Base change of the algebra norm Algebra.norm_one_tmul_eq_algebraMap_norm 0 below · cited by 1 · depth 16
• Norm of a product algebra is the product of norms Algebra.norm_prod 0 below · cited by 2 · depth 16
• A nonzero proper ideal strictly drops transcendence degree Algebra.trdeg_quotient_lt 0 below · cited by 2 · depth 16
• Pointwise fibrewise criterion for smoothness Algebra.isSmoothAt_of_isSmoothAt_fiber 0 below · cited by 1 · depth 17
• Norm as a product over rank-many algebra maps to a field Algebra.algebraMap_norm_eq_prod_apply_of_card_eq_finrank 0 below · cited by 3 · depth 18
• Weil restriction along a finite étale extension is finite flat Algebra.finite_and_flat_of_weilRestriction_points_equiv 4 below · cited by 1 · depth 18
• Counting K-points of a finite flat algebra over a valuation ring Algebra.natCard_algHom_eq_finrank_residueField_tensorProduct_of_flat_of_isReduced 0 below · cited by 2 · depth 18
• Norm of c-x as a power of minpoly(x) at c Algebra.norm_algebraMap_sub_eq_eval_minpoly_pow 1 below · cited by 2 · depth 18
• Norm multiplicativity along a full-rank injection into B₀ × B₁ Algebra.norm_eq_norm_fst_mul_norm_snd_of_injective 0 below · cited by 1 · depth 18
• Counting algebra maps into a field by branch ranks Algebra.card_algHom_le_finsum_finrank_quotient 0 below · cited by 1 · depth 19
• Counting 𝒪̂-embeddings of fixed slope into a valued field Algebra.card_algHom_le_finsum_finrank_quotient_of_valuation_pow_eq 0 below · cited by 2 · depth 19
• Representability of Weil restriction for affine schemes Algebra.exists_weilRestriction_points_equiv 0 below · cited by 2 · depth 19
• Base change of a split Weil restriction is finite free Algebra.finite_and_free_baseChange_of_weilRestriction_points_equiv_of_algEquiv_pi 2 below · cited by 1 · depth 19
• Finite algebra over a complete local ring splits into local factors Algebra.finite_maximalSpectrum_and_bijective_localization_of_module_finite_univ 2 below · cited by 1 · depth 19
• Norm of c-x as minimal polynomial value Algebra.norm_algebraMap_sub_eq_minpoly_eval 0 below · cited by 1 · depth 19
• Norm of 1+ε⊗ f equals 1+ε Tr(f) Algebra.norm_one_add_eps_tmul 0 below · cited by 1 · depth 19
• A finite free A-algebra representing a product of Hom-functors Algebra.exists_algHom_equiv_pi 0 below · cited by 1 · depth 20
• Split case of Weil restriction points: Hom_B(H,B⊗_A T)≅prodᵢHom_{A'}(Fᵢ,T) Algebra.exists_finite_free_algHom_tensorProduct_equiv_pi_of_algEquiv_pi 0 below · cited by 1 · depth 20
• Unit discriminant forces S to contain the integral closure Algebra.integralClosure_le_of_isUnit_discr_of_span_eq_top 1 below · cited by 1 · depth 20
• Trace of an integral element is integral Algebra.isIntegral_trace_of_finiteDimensional 0 below · cited by 1 · depth 21
• Trace of logarithmic derivative equals logarithmic derivative of norm Algebra.trace_inv_mul_derivation_eq_inv_norm_mul_derivation_norm 0 below · cited by 1 · depth 21
• Extracting m-th roots of finitely many units fppf-locally Algebra.exists_faithfullyFlat_finitePresentation_forall_pow_eq 0 below · cited by 1 · depth 22
• Norm as a product of residue norms weighted by local lengths Algebra.norm_eq_finprod_norm_quotient_pow_length 0 below · cited by 1 · depth 23
• Rational points avoiding finitely many non-zero functions Algebra.exists_algHom_forall_apply_ne_zero_of_finiteType_of_isAlgClosed 0 below · cited by 1 · depth 25
• Weil restriction along a finite free extension preserves finite type Algebra.exists_weilRestriction_points_equiv_finiteType 1 below · cited by 1 · depth 25
• Flat module-finite algebra unramified at all primes is étale Algebra.etale_of_moduleFinite_of_flat_of_forall_isUnramifiedAt 0 below · cited by 1 · depth 27
• Finite type algebras descend to a finite subextension Algebra.exists_intermediateField_finiteDimensional_tensorProduct_algEquiv_of_finiteType_of_isAlgebraic 0 below · cited by 1 · depth 27
• Unramifiedness off the closed point passes to completions Algebra.isUnramifiedAt_adicCompletion_of_forall_not_isMaximal 3 below · cited by 2 · depth 27
• Unramifiedness at a height-one prime: DVR criterion Algebra.isUnramifiedAt_iff_map_maximalIdeal_eq_and_isSeparable_of_height_eq_one 1 below · cited by 9 · depth 27
• Purity of the branch locus for finite flat extensions Algebra.isUnramifiedAt_of_forall_le_height_eq_one_of_flat_of_isIntegrallyClosed 12 below · cited by 1 · depth 27
• Unramifiedness at a horizontal height-one prime from ramification index one Algebra.isUnramifiedAt_of_height_eq_one_of_not_mem_of_forall_ramificationIndexAlong_eq_one 0 below · cited by 2 · depth 27
• Residue ring of a π-integral extension is algebraic over ℤ/r Algebra.isAlgebraic_zmod_quotient_of_card_quotient_eq_of_forall_exists_monic_aeval_mem 0 below · cited by 1 · depth 28
• Purity of the branch locus for finite free normal covers Algebra.isUnramifiedAt_of_forall_le_height_eq_one_of_free_of_isIntegrallyClosed 11 below · cited by 8 · depth 28
• Unramified at a height-one prime with ramification index one Algebra.isUnramifiedAt_of_height_eq_one_of_not_mem_of_ramificationIndexAlong_eq_one_of_centre 0 below · cited by 9 · depth 28
• Analytic chart from an étale coordinate on a smooth curve Algebra.exists_bijOn_eval_differentiableOn_of_smooth_of_kaehlerDifferential 3 below · cited by 4 · depth 29
• Cyclotomic Galois cover adjoining a primitive m-th root Algebra.exists_cyclotomic_galois_cover_of_isUnit 4 below · cited by 1 · depth 29
• Idempotents of a finite projective algebra are represented by an étale algebra Algebra.exists_etale_algHom_equiv_isIdempotentElem_tensorProduct_of_projective 0 below · cited by 1 · depth 29
• A height-one prime containing the different inside a given prime Algebra.exists_le_height_eq_one_of_comap_one_div_traceDual_le_of_free_of_isIntegrallyClosed 4 below · cited by 2 · depth 29
• Largest étale subalgebra of a finite k-algebra Algebra.exists_subalgebra_etale_forall_le_forall_baseChange_le_forall_tensorProduct_le 2 below · cited by 1 · depth 29
• Reducedness of a finite algebra via counting geometric points Algebra.isReduced_iff_natCard_algHom_eq_finrank_of_isAlgClosed 1 below · cited by 3 · depth 29
• Different ideal cuts out the ramification locus Algebra.isUnramifiedAt_iff_not_le_comap_one_div_traceDual_of_free_of_isIntegrallyClosed 5 below · cited by 2 · depth 29
• Ramification index one and separable residue extension give unramifiedness Algebra.isUnramifiedAt_of_ramificationIdx_eq_one_of_isSeparable 0 below · cited by 1 · depth 29
• Isomorphisms of finitely presented algebras descend to a stage Algebra.exists_algEquiv_tensorProduct_map_eq_of_finitePresentation_of_isDirectLimit 2 below · cited by 1 · depth 30
• Every algebra is a direct limit of finitely presented algebras Algebra.exists_isDirectLimit_of_finitePresentation 0 below · cited by 3 · depth 30
• Standard étale chart for a smooth complex curve at an étale coordinate Algebra.exists_isStandardEtale_polynomial_localizationAway_of_smooth_of_kaehlerDifferential 0 below · cited by 1 · depth 30
• Norm of a determinant is polynomial in the coefficients Algebra.exists_mvPolynomial_forall_eval_eq_norm_det_sum_smul 0 below · cited by 2 · depth 30
• Perfectness of the trace pairing at a prime descends to the fibre Algebra.exists_notMem_forall_dual_eq_trace_iff_fiber 0 below · cited by 1 · depth 30
• Zariski-local splitting of two maps out of a Galois cover Algebra.exists_span_eq_top_forall_exists_algebraMap_comp_eq_comp_of_bijective_tensorProduct 0 below · cited by 1 · depth 30
• Maximal étale subalgebra of a finite k-algebra Algebra.exists_subalgebra_etale_forall_le_forall_exists_pow_expChar_pow_sub_isNilpotent 0 below · cited by 2 · depth 30
• Smoothness spreads to specialisations with constant differential rank Algebra.isSmoothAt_of_le_of_finrank_tensorProduct_kaehlerDifferential_eq 2 below · cited by 1 · depth 30
• Pointwise trace criterion for unramifiedness of a finite algebra over a field Algebra.isUnramifiedAt_iff_exists_notMem_forall_dual_eq_trace_of_field 1 below · cited by 1 · depth 30
• Unramifiedness at a prime is detected on the fibre Algebra.isUnramifiedAt_iff_isUnramifiedAt_fiber 0 below · cited by 1 · depth 30
• Étale subalgebras lie in an étale radicial-nilpotent base Algebra.le_of_etale_of_forall_exists_pow_expChar_pow_sub_isNilpotent 1 below · cited by 1 · depth 30
• The different avoids a prime iff trace duality is perfect there Algebra.not_comap_one_div_traceDual_le_iff_exists_notMem_forall_dual_eq_trace 0 below · cited by 1 · depth 30
• Galois descent: C⊗_𝒪𝒪'xrightarrow ∼ A for twisted invariants Algebra.bijective_tensorProduct_lift_of_forall_iff_mem_range_of_galois 0 below · cited by 1 · depth 31
• Algebra maps between base changes descend to a finite stage Algebra.exists_algHom_tensorProduct_map_eq_of_finitePresentation_of_isDirectLimit 0 below · cited by 1 · depth 31
• Analytic chart on a smooth complex affine variety from étale coordinates Algebra.exists_bijOn_eval_differentiableOn_pi_of_smooth_of_kaehlerDifferential 3 below · cited by 2 · depth 31
• Étale-local splitting off the finite part over a prime Algebra.exists_etale_isIdempotentElem_finite_away_forall_liesOver_notMem 0 below · cited by 1 · depth 31
• Spreading out a finitely presented algebra over a directed colimit Algebra.exists_finitePresentation_tensorProduct_algEquiv_of_isDirectLimit 0 below · cited by 1 · depth 31
• Glueing locally defined n-th roots of unity along a Zariski cover Algebra.exists_pow_eq_one_and_forall_algHom_apply_eq_of_locally_of_isUnit_natCast 1 below · cited by 1 · depth 31
• Adapted smooth ambient coordinates at a point of a permissible centre Algebra.exists_smooth_surjective_localizationAway_basis_kaehlerDifferential_comap_eq_span 6 below · cited by 1 · depth 31
• Finite-type algebra maps agreeing over a direct limit agree at a finite stage Algebra.exists_tensorProduct_map_apply_eq_of_finiteType_of_isDirectLimit 0 below · cited by 1 · depth 31
• Trace-form criterion for unramifiedness of a finite algebra Algebra.formallyUnramified_iff_traceForm_nondegenerate_of_finite 0 below · cited by 1 · depth 31
• Unique transversal branch over t in a normal finite cover Algebra.existsUnique_prime_le_map_sup_span_eq_maximalIdeal_of_isUnramifiedAt_of_isDedekindDomain_quotient 26 below · cited by 1 · depth 32
• Standard étale presentation at étale coordinates over ℂ Algebra.exists_isStandardEtale_mvPolynomial_localizationAway_of_smooth_of_kaehlerDifferential 0 below · cited by 1 · depth 32
• Minimal standard smooth ambient for a finitely presented algebra Algebra.exists_isStandardSmooth_surjective_localizationAway_basis_kaehlerDifferential_of_basis_residueField 2 below · cited by 1 · depth 32
• Generic absolutely irreducible hypersurface model of a finite-type domain Algebra.exists_monic_irreducible_map_algebraicClosure_hypersurfaceModel_of_forall_isSeparable 4 below · cited by 1 · depth 32
• Kernel vanishes near a smooth point with no cotangent-rank drop Algebra.exists_notMem_map_ker_eq_bot_of_surjective_of_isSmoothAt_of_finrank_le 1 below · cited by 1 · depth 32
• Clearing denominators in the subalgebra R[I/a]⊆ S Algebra.exists_pow_mul_eq_of_mem_adjoin_div 0 below · cited by 2 · depth 32
• Openness of the smooth-and-free locus; minimal primes lie in it Algebra.isOpen_setOf_isSmoothAt_and_mem_freeLocus_and_minimalPrimes_subset 4 below · cited by 1 · depth 32
• Hom-wise universal property implies IsPushout Algebra.isPushout_of_forall_existsUnique_algHom_comp_eq 0 below · cited by 10 · depth 32
• dt generates the cotangent space along a holomorphic branch Algebra.ker_smul_top_sup_span_kaehlerDifferentialD_eq_top_of_bijOn_of_differentiableOn 0 below · cited by 2 · depth 32
• Discriminant is associated to the norm of the Jacobian determinant Algebra.associated_discr_norm_jacobianDet_of_square_presentation 17 below · cited by 1 · depth 33
• A unique transversal branch over t at each maximal ideal Algebra.existsUnique_prime_le_map_sup_span_eq_maximalIdeal_of_isUnramifiedAt_of_isDedekindDomain_quotient_of_isLocalRing 18 below · cited by 1 · depth 33
• Holomorphic character branches are value-open at each point Algebra.exists_forall_mem_of_norm_sub_lt_of_bijOn_of_differentiableOn 4 below · cited by 1 · depth 33
• Generic Noether normalisation over a domain Algebra.exists_ne_zero_algebraicIndependent_forall_isIntegral_pow_smul_of_finiteType 0 below · cited by 3 · depth 33
• Generic smoothness from dense points with separable residue fields Algebra.isSmoothAt_of_mem_minimalPrimes_of_dense_of_formallySmooth_residueField 3 below · cited by 1 · depth 33
• Unramifiedness away from s descends to the n-adic completion Algebra.isUnramifiedAt_adicCompletion_of_forall_not_isMaximal_of_not_mem 3 below · cited by 2 · depth 33
• Surjection of formally smooth local k-algebras with no cotangent rank drop is injective Algebra.ker_algebraMap_eq_bot_of_formallySmooth_of_finrank_le 0 below · cited by 1 · depth 33
• Universal factorisation through φ forces generation by its image Algebra.adjoin_range_eq_top_and_finiteType_of_forall_existsUnique_comp_eq 0 below · cited by 2 · depth 34
• Twisting a trace-like form multiplies its Gram determinant by the norm Algebra.det_dual_mul_mul_eq_norm_mul_det 0 below · cited by 1 · depth 34
• Extending ρ to the subalgebra generated by red(T) Algebra.exists_algHom_adjoin_range_apply_eq_of_forall_apply_mem_bot 0 below · cited by 2 · depth 34
• Scheja–Storch trace form for a square presentation Algebra.exists_dual_bijective_mul_and_trace_eq_jacobianDet_mul_of_square_presentation 14 below · cited by 1 · depth 34
• Splitting a Hochschild 1-cocycle via a separability element Algebra.exists_forall_add_sub_eq_zero_of_map_mul_of_separabilityElement_tensor 0 below · cited by 1 · depth 34
• No dual-number points implies reduced, with rank the point count Algebra.isReduced_and_finrank_eq_natCard_algHom_of_forall_dualNumber_snd_eq_zero 2 below · cited by 2 · depth 34
• Perfect linear form gives unit Gram determinant Algebra.isUnit_det_dual_mul_of_bijective 0 below · cited by 1 · depth 34
• Mac Lane separability descends to minimal primes Algebra.linearIndepOn_pow_localization_atPrime_of_mem_minimalPrimes_of_dense 0 below · cited by 1 · depth 34
• Tame bound (t) ⊆ √(t) d in Sₓ Algebra.map_span_le_radical_mul_map_comap_one_div_traceDual_of_isUnramifiedAt_of_charZero 14 below · cited by 1 · depth 34
• Different elements lie in ̄ x^{ n-1} on the special fibre Algebra.mk_mem_pow_ramificationIdx_sub_one_of_mem_comap_one_div_traceDual 1 below · cited by 1 · depth 34
• Base-change maps from F⊗_{A[a]}B as A-algebra maps with prescribed value at a Algebra.nonempty_algHom_tensorProduct_adjoin_equiv_subtype_apply_eq 0 below · cited by 2 · depth 34
• Scheja–Storch: the Bezoutian dualises a finite free complete intersection Algebra.bijective_rTensor_dual_bezoutian_of_square_presentation 9 below · cited by 1 · depth 35
• Faithfully flat descent for graded algebras Algebra.bijective_tensorProduct_equalizer_of_faithfullyFlat_of_cocycle 1 below · cited by 1 · depth 35
• Non-zero dual-number point at a rational point with 𝔪² ≠ 𝔪 Algebra.exists_algHom_dualNumber_snd_ne_zero_of_sq_ne 0 below · cited by 1 · depth 35
• Kummer cover: roots of finitely many units Algebra.exists_etale_faithfullyFlat_finite_forall_exists_units_pow_eq_of_isUnit 1 below · cited by 1 · depth 35
• Elements of the different give trace functionals on S/IS Algebra.exists_forall_dual_quotient_eq_trace_of_mem_comap_one_div_traceDual 0 below · cited by 1 · depth 35
• Presentation independence for square-presented rational local k-algebras Algebra.exists_ker_map_localization_eq_span_of_surjective_of_exists_square_presentation_of_surjective_algebraMap_residueField 6 below · cited by 1 · depth 35
• Tame different bound at a height-one prime above t Algebra.exists_mem_comap_one_div_traceDual_mul_eq_mul_of_height_eq_one_of_charZero 1 below · cited by 1 · depth 35
• Finite flat algebras over a local ring are finitely presented Algebra.finitePresentation_of_finite_of_flat_of_isLocalRing 0 below · cited by 1 · depth 35
• Different becomes principal at a factorial localisation Algebra.isPrincipal_map_comap_one_div_traceDual_of_uniqueFactorizationMonoid 0 below · cited by 1 · depth 35
• Idempotent maximal ideals force a finite algebra to be Ωⁿ Algebra.isReduced_and_finrank_eq_natCard_algHom_of_forall_isMaximal_sq_eq 0 below · cited by 1 · depth 35
• Bezoutian determinant multiplies to the Jacobian determinant Algebra.lmul_bezoutian_eq_jacobianDet 1 below · cited by 1 · depth 35
• Balancedness of the Bezoutian of a square presentation Algebra.tmul_one_mul_bezoutian_eq_one_tmul_mul 0 below · cited by 2 · depth 35
• Trace formula via a balanced Casimir element Algebra.trace_eq_dual_lmul_of_bijective_rTensor 0 below · cited by 1 · depth 35
• Affine blow-up chart C[I/a] under flat base change Algebra.adjoin_div_tensorProduct_bijective_of_flat 0 below · cited by 1 · depth 36
• Bezoutian contraction bijective: reduction to algebraically closed fields Algebra.bijective_rTensor_dual_bezoutian_of_forall_field 1 below · cited by 1 · depth 36
• Scheja–Storch bijectivity over an algebraically closed field Algebra.bijective_rTensor_dual_bezoutian_of_isAlgClosed 6 below · cited by 1 · depth 36
• Effective faithfully flat descent for commutative algebras Algebra.bijective_tensorProduct_equalizer_of_faithfullyFlat_of_descentDatum 1 below · cited by 1 · depth 36
• Algebra-valued character on a multiplicative spanning family Algebra.exists_algHom_adjoin_range_apply_eq_of_forall_sum_smul_eq_zero_of_algebra 0 below · cited by 2 · depth 36
• Presentation-independence of square truncated presentations Algebra.exists_ker_eq_span_of_surjective_truncated_of_ker_eq_span 4 below · cited by 1 · depth 36
• Elements of an affine blow-up chart are g/a^N with g ∈ J^N Algebra.exists_pow_mem_mul_pow_eq_of_mem_adjoin_blowupChart 0 below · cited by 2 · depth 36
• Krull dimension equals transcendence degree for finitely generated domains Algebra.ringKrullDim_eq_toENat_trdeg_of_finiteType 0 below · cited by 5 · depth 36
• Trace-transferred Gram determinant over a free algebra Algebra.det_trace_basis_mul_basis_mul_eq_discr_pow_card_mul_norm_det 0 below · cited by 1 · depth 37
• Two minimal truncated presentations differ by an automorphism Algebra.exists_algEquiv_comp_eq_of_surjective_of_ker_le_sq_truncated 1 below · cited by 1 · depth 37
• Localising at powers of r: finite free faithfully flat algebras over S_{gr} Algebra.exists_algebra_away_mul_finite_free_faithfullyFlat_finitePresentation_of_isLocalization_powers 0 below · cited by 1 · depth 37
• Lifting a based free algebra with monogenic special fibre Algebra.exists_lift_basis_of_surjective_of_monogenic_specialFibre 0 below · cited by 1 · depth 37
• Spreading a finite flat algebra over a local ring to a basic open Algebra.exists_not_mem_finite_free_isLocalization_algebraMapSubmonoid_primeCompl_of_finite_of_faithfullyFlat_atPrime 2 below · cited by 1 · depth 37
• Trace commutes with base change on 1 ⊗ x Algebra.trace_baseChange_one_tmul 0 below · cited by 1 · depth 37
• Descent of a finite projective algebra to a finitely generated subring Algebra.exists_finset_forall_exists_subalgebra_isPushout_of_span_eq_top 0 below · cited by 1 · depth 38
• Zariski-local injectivity of T⊗_S H¹(L_{S/R})→ H¹(L_{T/R}) Algebra.injective_liftBaseChange_h1CotangentMap_of_span_eq_top_of_forall_exists_isWeaklyRegular 1 below · cited by 1 · depth 39
• Left exactness of Jacobi–Zariski for Koszul-acyclic presentations Algebra.injective_liftBaseChange_h1CotangentMap_of_ker_eq_span_range_of_forall_exists_alternating 0 below · cited by 1 · depth 40
• Trace of an elementary tensor in L ⊗_K A Algebra.trace_tensorProduct_rightActions_tmul_eq_algebraMap_trace_mul 0 below · cited by 1 · depth 40

Algebra.DescentCofaces 1

• Locally constant ℤ/p-valued Amitsur cocycles over ℤ are coboundaries Algebra.DescentCofaces.exists_finite_flat_unramified_nonempty_ringHom_iff_isCoboundary 9 below · cited by 1 · depth 15

Algebra.Etale 29

• Étale algebras over reduced Noetherian rings are reduced Algebra.Etale.isReduced_of_isReduced_of_isNoetherianRing 0 below · cited by 2 · depth 14
• Étale algebras over an algebraically closed field: point count equals dimension Algebra.Etale.natCard_algHom_eq_finrank_of_isAlgClosed 0 below · cited by 7 · depth 14
• Simultaneous splitting of finitely many finite étale algebras Algebra.Etale.exists_faithfullyFlat_forall_nonempty_algEquiv_pi 1 below · cited by 5 · depth 15
• Finite étale algebras over a Noetherian local ring split after finite étale base change Algebra.Etale.exists_finite_etale_faithfullyFlat_tensorProduct_algEquiv_pi 1 below · cited by 3 · depth 15
• Finite étale algebras of constant rank split after finite étale base change Algebra.Etale.exists_finite_etale_faithfullyFlat_tensorProduct_algEquiv_pi_of_rankAtStalk_eq 0 below · cited by 4 · depth 16
• Local rings of an étale algebra over a normal domain Algebra.Etale.isDomain_and_isIntegrallyClosed_of_isLocalization_atPrime 0 below · cited by 9 · depth 16
• Finite étale algebras are split by the algebraic closure Algebra.Etale.finite_and_bijective_lift_pi_algHom_algebraicClosure 2 below · cited by 2 · depth 17
• Maps into an étale algebra are determined by Ω-points Algebra.Etale.algHom_ext_of_forall_comp_eq 0 below · cited by 3 · depth 18
• Geometric points separate elements of an étale algebra Algebra.Etale.eq_of_forall_algHom_apply_eq 0 below · cited by 7 · depth 18
• Full faithfulness of geometric points on étale K-algebras Algebra.Etale.existsUnique_algHom_forall_comp_eq_of_equivariant 0 below · cited by 2 · depth 18
• Reduced finite algebras over a perfect field are étale Algebra.Etale.of_isReduced_of_perfectField 0 below · cited by 4 · depth 20
• Étale local extensions with full automorphism group are Galois Algebra.Etale.exists_sum_mul_smul_eq_ite_of_isLocalRing 0 below · cited by 1 · depth 26
• Finite étale algebras split over an algebraically closed extension Algebra.Etale.finite_and_bijective_lift_pi_algHom_of_isAlgClosed 2 below · cited by 2 · depth 26
• Étale base change preserves integral closedness of domains Algebra.Etale.isIntegrallyClosed_tensorProduct_of_isDomain 1 below · cited by 1 · depth 27
• Finite flat with formally unramified residue fibre is étale Algebra.Etale.of_formallyUnramified_residueField_baseChange 1 below · cited by 3 · depth 27
• Rigidity of algebra maps from a finite étale algebra over a henselian local ring Algebra.Etale.algHom_ext_of_forall_sub_mem_map_maximalIdeal_of_henselianLocalRing 0 below · cited by 3 · depth 28
• Hensel lifting of bialgebra maps from a finite étale bialgebra Algebra.Etale.existsUnique_bialgHom_baseChange_residueField_eq_of_moduleFinite_of_henselianLocalRing 5 below · cited by 1 · depth 29
• Lifting a residue-field isomorphism to finite étale local algebras Algebra.Etale.exists_algEquiv_residue_eq_of_isLocalRing_of_isAdicComplete 4 below · cited by 2 · depth 29
• Local étale base change of a normal domain is normal Algebra.Etale.isDomain_and_isIntegrallyClosed_tensorProduct_of_isLocalRing 1 below · cited by 3 · depth 29
• Lifting algebra maps from a finite étale algebra over a henselian local ring Algebra.Etale.existsUnique_algHom_baseChange_residueField_eq_of_moduleFinite_of_henselianLocalRing 4 below · cited by 2 · depth 30
• Finite étale algebras over a residue field lift Algebra.Etale.exists_free_nonempty_algEquiv_baseChange_residueField_of_isLocalRing 0 below · cited by 1 · depth 30
• Étaleness descends from the maximal-adic completion Algebra.Etale.of_etale_adicCompletion_tensorProduct 0 below · cited by 1 · depth 30
• Unramified maps between standard smooth algebras of equal dimension are étale Algebra.Etale.of_formallyUnramified_of_isStandardSmoothOfRelativeDimension 0 below · cited by 3 · depth 30
• Étale coordinates from a basis of differentials Algebra.Etale.of_basis_eq_D 2 below · cited by 1 · depth 32
• An m-fold tensor power classifying m-tuples of points Algebra.Etale.exists_finite_etale_forall_existsUnique_comp_eq 0 below · cited by 1 · depth 33
• Two points of an étale algebra agree on a distinguished idempotent Algebra.Etale.exists_isIdempotentElem_mul_eq_mul_and_not_mem_iff 0 below · cited by 1 · depth 33
• Inverting an idempotent of a finite étale algebra Algebra.Etale.finite_etale_faithfullyFlat_away_of_isIdempotentElem 0 below · cited by 1 · depth 33
• Finite étale local algebras with equinumerous finite residue fields Algebra.Etale.nonempty_algEquiv_of_isLocalRing_of_finite_residueField_of_card_eq 6 below · cited by 1 · depth 35
• Étale truncations of a flat unramified local algebra Algebra.Etale.quotient_tensorProduct_of_flat_of_map_maximalIdeal_eq_of_isSeparable 3 below · cited by 1 · depth 38

Algebra.FinitePresentation 4

• Finite presentation from factoring maps through directed colimits Algebra.FinitePresentation.of_forall_isDirectLimit_exists_comp_eq 1 below · cited by 1 · depth 29
• A presentation with Jacobian minor nonzero at a prime Algebra.FinitePresentation.exists_surjective_aeval_det_pderiv_not_mem_of_basis_residueField 0 below · cited by 1 · depth 33
• Finite presentation descends along faithfully flat algebras Algebra.FinitePresentation.of_faithfullyFlat_of_finitePresentation 6 below · cited by 1 · depth 36
• Finite presentation descends along a nilpotent thickening Algebra.FinitePresentation.of_surjective_of_isNilpotent_ker_of_flat_of_finitePresentation 0 below · cited by 1 · depth 45

Algebra.FiniteType 6

• Descent of finite type along faithfully flat finitely presented algebras Algebra.FiniteType.of_faithfullyFlat_of_finitePresentation 5 below · cited by 4 · depth 16
• Finite residue fields at maximal ideals of finite-type ℤ-algebras Algebra.FiniteType.finite_quotient_and_exists_charP_of_isMaximal_int 1 below · cited by 2 · depth 30
• Finitely generated ℤ-algebras have a finite residue field Algebra.FiniteType.exists_isMaximal_and_finite_quotient_of_int 1 below · cited by 1 · depth 32
• Two residue characteristics for a finitely generated ℤ-algebra domain Algebra.FiniteType.exists_isMaximal_natCast_mem_of_ne_of_charZero 0 below · cited by 1 · depth 32
• Generic upper bound for transcendence degree along a prime Algebra.FiniteType.exists_notMem_under_forall_trdeg_quotient_le 1 below · cited by 1 · depth 32
• Positive residue characteristic of faithfully flat local algebras Algebra.FiniteType.exists_prime_charP_residueField_of_isMaximal_of_faithfullyFlat 2 below · cited by 1 · depth 32

Algebra.FormallyEtale 3

• Unique lifting of algebra maps mod p for formally étale H Algebra.FormallyEtale.existsUnique_algHom_baseChange_eq_of_module_finite_free_zmodp 3 below · cited by 4 · depth 21
• Reduced finite 𝔽ₚ-algebras lift to formally étale 𝒪-algebras Algebra.FormallyEtale.exists_baseChange_algEquiv_of_isReduced_zmodp 1 below · cited by 1 · depth 24
• Differential criterion for formal étaleness over an intermediate ring Algebra.FormallyEtale.of_formallySmooth_of_bijective_mapBaseChange 0 below · cited by 3 · depth 29

Algebra.FormallySmooth 21

• Points of formally smooth algebras lift along p-adic reduction Algebra.FormallySmooth.exists_algHom_baseChange_eq_of_isAdicComplete 0 below · cited by 1 · depth 22
• Formal smoothness of a one-dimensional local domain over a perfect field Algebra.FormallySmooth.of_maximalIdeal_eq_span_of_perfectField 1 below · cited by 3 · depth 24
• Étale coordinate on a formally smooth local algebra of relative dimension one Algebra.FormallySmooth.exists_formallyUnramified_aeval_and_maximalIdeal_eq_of_finrank_kaehlerDifferential_eq_one 1 below · cited by 1 · depth 25
• Formal smoothness of a flat regular local algebra with retraction Algebra.FormallySmooth.of_isRegularLocalRing_of_algHom_of_maximalIdeal_eq_span 2 below · cited by 1 · depth 25
• Formal smoothness of a local ring with principal maximal ideal Algebra.FormallySmooth.of_maximalIdeal_eq_span_of_isSeparable_residueField 0 below · cited by 1 · depth 25
• Power-series expansion along a section with prescribed parameter Algebra.FormallySmooth.exists_powerSeries_expansion_along_section_apply_eq_X 1 below · cited by 3 · depth 26
• Étale coordinate: A[X]→ S, X↦ t, when dt is a basis Algebra.FormallySmooth.formallySmooth_and_formallyUnramified_aeval_of_existsUnique_smul_D_eq 0 below · cited by 1 · depth 26
• Regular local rings with k-rational residue field are formally smooth Algebra.FormallySmooth.of_isRegularLocalRing_of_surjective_algebraMap_residueField 1 below · cited by 1 · depth 26
• Power-series expansion along a formally smooth section Algebra.FormallySmooth.exists_powerSeries_expansion_along_section 0 below · cited by 1 · depth 27
• Formal smoothness of S/tS when Ω_{S/A} is free on dt Algebra.FormallySmooth.quotient_span_singleton_of_existsUnique_eq_smul_D 2 below · cited by 1 · depth 27
• Étale coordinate at a rational point over a DVR Algebra.FormallySmooth.exists_etaleCoordinate_of_krullDimLE_one 7 below · cited by 3 · depth 28
• Smooth curve over k is a DVR at a rational point Algebra.FormallySmooth.isDiscreteValuationRing_localizationAtPrime_of_krullDimLE_one 1 below · cited by 1 · depth 29
• Local rings of smooth DVR-algebras with prime uniformiser are domains Algebra.FormallySmooth.isDomain_of_isLocalizationAtPrime_of_prime_algebraMap 0 below · cited by 1 · depth 29
• Distinct minimal primes over a uniformiser are comaximal Algebra.FormallySmooth.sup_eq_top_of_mem_minimalPrimes_span_of_isDiscreteValuationRing 2 below · cited by 9 · depth 29
• Fibrewise formal smoothness of a normal relative curve Algebra.FormallySmooth.residueField_fiber_of_isIntegrallyClosed_quotient_of_transcendental 5 below · cited by 3 · depth 30
• Formal coordinates along a section of a formally smooth algebra Algebra.FormallySmooth.existsUnique_algHom_apply_eq_of_isNilpotent 0 below · cited by 1 · depth 31
• Reducedness of the fibre of a smooth algebra at a maximal ideal Algebra.FormallySmooth.isReduced_quotient_map_of_isMaximal_of_finitePresentation 1 below · cited by 2 · depth 31
• Formally smooth field extensions are separable in Mac Lane's sense Algebra.FormallySmooth.linearIndepOn_pow_of_linearIndepOn_id 1 below · cited by 1 · depth 34
• Étale coordinates from a basis of Ω_{A/R} Algebra.FormallySmooth.etale_aeval_of_basis_kaehlerDifferential 0 below · cited by 1 · depth 36
• Uniqueness of formally smooth lifts along a nilpotent ideal Algebra.FormallySmooth.exists_algEquiv_comp_eq_of_isNilpotent_of_ker_eq_map 0 below · cited by 1 · depth 37
• Symmetric normalised Hochschild 2-cocycles are coboundaries for formally smooth algebras Algebra.FormallySmooth.exists_linearMap_eq_of_symmetric_hochschild_two_cocycle 0 below · cited by 1 · depth 37

Algebra.FormallyUnramified 8

• Finite reduced algebras over a perfect field are formally unramified Algebra.FormallyUnramified.of_isReduced_of_perfectField 0 below · cited by 1 · depth 13
• A nonzero finite flat unramified ℤ-algebra has a ℤ-point Algebra.FormallyUnramified.nonempty_ringHom_int 1 below · cited by 2 · depth 15
• Inertia fixes ℚ̄ₚ-points of finite unramified ℤₚ-algebras Algebra.FormallyUnramified.algEquiv_apply_eq_of_mem_inertiaSubgroupIn_padicIntegers 2 below · cited by 1 · depth 18
• Formal unramifiedness descends from the residue fibre Algebra.FormallyUnramified.of_residueField_baseChange_of_finite 0 below · cited by 1 · depth 28
• Finite unramified algebras are split by a finite Galois subextension Algebra.FormallyUnramified.exists_isGalois_forall_algHom_apply_mem 0 below · cited by 1 · depth 30
• Uniqueness of formally unramified maps into I-adically separated rings Algebra.FormallyUnramified.ext_of_isHausdorff 0 below · cited by 1 · depth 30
• Fibre regularity ascends along a formally unramified local algebra Algebra.FormallyUnramified.isRegularLocalRing_quotient_span_of_ringKrullDim_quotient_eq_one 0 below · cited by 7 · depth 31
• Formal unramifiedness from all geometric base changes Algebra.FormallyUnramified.of_forall_isAlgClosed_formallyUnramified_tensorProduct_map 0 below · cited by 1 · depth 32

Algebra.H1Cotangent 2

• Jacobi–Zariski left exactness over a smooth algebra Algebra.H1Cotangent.liftBaseChange_map_injective_of_smooth 3 below · cited by 1 · depth 37
• Injectivity of the base-changed H¹-cotangent map for étale extensions Algebra.H1Cotangent.liftBaseChange_map_injective_of_etale 2 below · cited by 1 · depth 38

Algebra.IsAlgebraic 1

• Algebraic over R[g] from finiteness over K(g) Algebra.IsAlgebraic.adjoin_singleton_of_finiteDimensional_intermediateField_adjoin_of_isFractionRing 0 below · cited by 4 · depth 26

Algebra.IsIntegral 3

• Krull dimension grows along injective integral extensions Algebra.IsIntegral.ringKrullDim_le_of_injective 0 below · cited by 4 · depth 29
• Discrete valuative criterion for integrality Algebra.IsIntegral.of_forall_valuationSubring_isDiscreteValuationRing_apply_mem 7 below · cited by 4 · depth 31
• Integral A-algebra maps into a domain over A are injective Algebra.IsIntegral.injective_of_injective_algebraMap 0 below · cited by 1 · depth 32

Algebra.IsInvariant 8

• Invariants under a transitive action on maximal ideals form a local ring Algebra.IsInvariant.exists_isLocalRing_maximalIdeal_eq_under_of_forall_isMaximal_exists_smul_eq 0 below · cited by 2 · depth 21
• Noether's finiteness theorem for finite group actions Algebra.IsInvariant.moduleFinite_and_finiteType_of_finiteType 0 below · cited by 15 · depth 26
• Two Ω-points agreeing on an invariant subring are G-conjugate Algebra.IsInvariant.exists_ringHom_eq_comp_toRingHom_of_comp_algebraMap_eq 0 below · cited by 1 · depth 27
• Completion at n replaces G by its stabilizer Algebra.IsInvariant.isInvariant_adicCompletion_stabilizer_and_injective_and_finite 2 below · cited by 7 · depth 27
• Subgroup of inertia: invariants surject onto the residue field Algebra.IsInvariant.exists_forall_smul_eq_and_sub_mem_of_le_inertia 0 below · cited by 1 · depth 29
• Invariants of a flat finite-type algebra over a Dedekind domain Algebra.IsInvariant.flat_and_finiteType_of_isDedekindDomain 1 below · cited by 1 · depth 29
• Local rings of invariants of a one-dimensional regular ring Algebra.IsInvariant.isDiscreteValuationRing_localization_atPrime_of_forall_isMaximal 0 below · cited by 1 · depth 30
• Separable residue extension at a prime below tame inertia Algebra.IsInvariant.isSeparable_of_isFractionRing_quotient_of_lt_of_isUnit_card_inertia 6 below · cited by 1 · depth 34

Algebra.IsPushout 3

• Gluing three congruent automorphisms over a triple fibre product Algebra.IsPushout.exists_algEquiv_slice_eq_of_flat 1 below · cited by 1 · depth 39
• Gluing three congruent endomorphisms along a flat pushout Algebra.IsPushout.exists_algHom_slice_eq_of_flat 1 below · cited by 1 · depth 40
• Slices of a flat pushout along a triple fibre product Algebra.IsPushout.slice_ext_and_exists_of_flat 0 below · cited by 3 · depth 40

Algebra.IsSeparable 3

• Separability from [F:Fᵖ]=p and a non-p-th-power in E Algebra.IsSeparable.of_finrank_fieldRange_frobenius_eq 0 below · cited by 3 · depth 13
• Finite extensions of degree coprime to the exponential characteristic are separable Algebra.IsSeparable.of_coprime_finrank_expChar 0 below · cited by 6 · depth 17
• Base change of a finite separable field extension Algebra.IsSeparable.isReduced_and_isSeparable_and_finite_tensorProduct 0 below · cited by 1 · depth 26

Algebra.IsSmoothAt 2

• Smoothness at a prime implies flatness of the local ring Algebra.IsSmoothAt.flat_localization_atPrime 0 below · cited by 1 · depth 27
• Smoothness at a prime descends along a smooth algebra Algebra.IsSmoothAt.of_isSmoothAt_of_smooth 4 below · cited by 1 · depth 36

Algebra.IsStandardEtale 3

• Points of a standard étale k[X]-algebra lie on a plane chart Algebra.IsStandardEtale.exists_forall_algHom_evalEval_eq_zero_and_ext_and_surj_and_repr 0 below · cited by 1 · depth 30
• Points of a standard étale algebra over k[X₁,…,Xₙ] Algebra.IsStandardEtale.exists_forall_algHom_eval_map_eval_eq_zero_and_ext_and_surj_and_repr_of_mvPolynomial 0 below · cited by 1 · depth 32
• Standard étale algebras lift along surjections of the base Algebra.IsStandardEtale.exists_isStandardEtale_tensorProduct_algEquiv_of_surjective 0 below · cited by 1 · depth 34

Algebra.IsStandardSmooth 1

• Standard smooth algebras have some relative dimension Algebra.IsStandardSmooth.exists_isStandardSmoothOfRelativeDimension_of_field 0 below · cited by 1 · depth 16

Algebra.IsStandardSmoothOfRelativeDimension 4

• Local rings of a standard smooth curve are DVRs Algebra.IsStandardSmoothOfRelativeDimension.isDiscreteValuationRing_localization_atPrime 0 below · cited by 13 · depth 14
• Standard smooth domains of relative dimension 1 are Dedekind Algebra.IsStandardSmoothOfRelativeDimension.isDedekindDomain 1 below · cited by 1 · depth 28
• Standard smooth algebras are étale over a polynomial ring Algebra.IsStandardSmoothOfRelativeDimension.exists_etale_aeval 2 below · cited by 2 · depth 29
• Lifting standard smooth algebras along a surjection with nil kernel Algebra.IsStandardSmoothOfRelativeDimension.exists_isPushout_of_surjective_of_forall_isNilpotent 0 below · cited by 1 · depth 36

Algebra.IsUnramifiedAt 3

• Unramified with dimension inequality implies étale over a normal base Algebra.IsUnramifiedAt.isEtaleAt_of_ringKrullDim_le 1 below · cited by 1 · depth 18
• Unramified off the closed fibre persists under local base change Algebra.IsUnramifiedAt.baseChange_of_ne_maximalIdeal_of_map_maximalIdeal_eq 0 below · cited by 1 · depth 26
• Regularity at non-maximal primes of a finite unramified algebra Algebra.IsUnramifiedAt.isRegularLocalRing_localization_of_ne_maximalIdeal 0 below · cited by 2 · depth 26

Algebra.PatchingDatum 5

• Transport of a patching datum along an isomorphism R ≅ T Algebra.PatchingDatum.exists_module_of_bijective_of_exists_presentation 13 below · cited by 4 · depth 8
• landmark Taylor–Wiles patching: a patched level with zero relation ideal Algebra.PatchingDatum.nonempty_patchingLevel_bot 5 below · cited by 2 · depth 8
• Patching datum forces isomorphism and complete-intersection presentation Algebra.PatchingDatum.bijective_and_exists_presentation_of_surjective_of_exists 13 below · cited by 2 · depth 9
• Patching data from complete-intersection presentations over 𝒪 Algebra.PatchingDatum.nonempty_of_exists_presentation_of_free 12 below · cited by 2 · depth 9
• Patching exit: R ≅ T, M free, T a power-series quotient Algebra.PatchingDatum.bijective_and_free_of_surjective 12 below · cited by 3 · depth 10

Algebra.PatchingLevel 1

• Patching descent at zero relation ideal: M free, kerψ=(φ(Xᵢ)) Algebra.PatchingLevel.free_and_ker_eq_span 5 below · cited by 2 · depth 8

Algebra.PointDerivations 4

• Reading point-derivation-valued cocycles as tensors W ⊗ Hom(V^∨,H₁) Algebra.PointDerivations.exists_reader_tensor_linearMap_dual_of_linearEquiv_tensor 0 below · cited by 1 · depth 30
• Point derivations with values in M are P(k)⊗_k M Algebra.PointDerivations.exists_linearEquiv_tensor_forall_map_eq_of_finiteType 0 below · cited by 1 · depth 31
• Descent of a point derivation along an injective linear map Algebra.PointDerivations.exists_eq_and_map_eq_map_of_forall_apply_eq 0 below · cited by 2 · depth 35
• Point derivations as Hom_k(Ω, M): finiteness and dimension Algebra.PointDerivations.finite_and_finrank_eq_mul_of_surjective_of_ker 0 below · cited by 1 · depth 35

Algebra.QuasiFinite 3

• Quasi-finiteness from flatness and a quasi-finite generic fibre Algebra.QuasiFinite.of_flat_of_quasiFinite_genericFiber 1 below · cited by 1 · depth 15
• Quasi-finiteness from flatness and a module-finite generic fibre Algebra.QuasiFinite.of_flat_of_finiteType_of_moduleFinite_baseChange_fractionRing 0 below · cited by 1 · depth 31
• Generic finiteness at a minimal prime (ring form) Algebra.QuasiFinite.exists_not_mem_finite_awayMap_of_mem_minimalPrimes 0 below · cited by 1 · depth 38

Algebra.QuasiFiniteAt 2

• Birational corollary of Zariski's main theorem Algebra.QuasiFiniteAt.exists_algebraMap_mul_eq_of_isIntegrallyClosed_of_injective 0 below · cited by 3 · depth 24
• Quasi-finiteness at an isolated point of its fibre Algebra.QuasiFiniteAt.of_minimal_of_maximal 0 below · cited by 4 · depth 24

Algebra.Smooth 8

• Smooth algebras over integrally closed domains have normal localisations Algebra.Smooth.isDomain_and_isIntegrallyClosed_of_isIntegrallyClosed_of_isLocalization_atPrime 1 below · cited by 3 · depth 15
• Smooth algebras over reduced Noetherian rings are reduced Algebra.Smooth.isReduced_of_isReduced_of_isNoetherianRing 2 below · cited by 12 · depth 18
• Local rings of smooth algebras over a UFD are normal Algebra.Smooth.isDomain_and_isIntegrallyClosed_of_isLocalization_atPrime 1 below · cited by 10 · depth 19
• Smooth A₀-subalgebra of a field: finiteness, normality, fibre primes Algebra.Smooth.fg_and_isIntegral_mem_and_minimalPrimes_and_formallySmooth_localizationAtPrime 3 below · cited by 9 · depth 27
• Smooth algebras over normal domains are integrally closed Algebra.Smooth.isIntegrallyClosed_of_isDomain 2 below · cited by 7 · depth 28
• Normal affine curves over a perfect field are smooth Algebra.Smooth.of_isIntegrallyClosed_of_krullDimLE_one_of_perfectField 2 below · cited by 6 · depth 31
• Quotients of a smooth algebra by minimal primes are normal Algebra.Smooth.isIntegrallyClosed_quotient_of_mem_minimalPrimes 2 below · cited by 2 · depth 33
• Smooth algebras over a field are reduced Algebra.Smooth.isReduced_of_field 3 below · cited by 4 · depth 35

Algebra.TensorProduct 28

• F ⊗_k K is a field when k is algebraically closed in F Algebra.TensorProduct.isField_of_isSeparable_of_forall_isAlgebraic_mem_range 0 below · cited by 7 · depth 14
• A second branch through every zero of v Algebra.TensorProduct.exists_mem_minimalPrimes_ne_and_le_of_mul_eq_pow_of_tmul_mem 0 below · cited by 2 · depth 15
• Integral closedness ascends to L ⊗_{k_0} S Algebra.TensorProduct.isDomain_and_isIntegrallyClosed_of_isField_of_isSeparable 0 below · cited by 1 · depth 16
• Normality of a flat base change from reduced special fibre Algebra.TensorProduct.isDomain_and_isIntegrallyClosed_of_isReduced_fibre 2 below · cited by 7 · depth 16
• Geometric reducedness over a perfect field Algebra.TensorProduct.isReduced_of_perfectField_of_isReduced 0 below · cited by 1 · depth 16
• Base change along Λ → k factors through Λ/I Algebra.TensorProduct.nonempty_algEquiv_tensor_quotient_of_isScalarTower 0 below · cited by 1 · depth 16
• Kernel of id_C⊗ε lies in the Jacobson radical Algebra.TensorProduct.ker_lift_le_jacobson_of_isLocalRing 0 below · cited by 1 · depth 18
• Base-changed norm as product of Galois conjugates Algebra.TensorProduct.algebraMap_norm_eq_prod_map_algEquiv 0 below · cited by 14 · depth 23
• Pairs of L-points separate A ⊗_K A Algebra.TensorProduct.eq_zero_of_forall_lift_apply_eq_zero 0 below · cited by 3 · depth 23
• Special-fibre coordinates pass to a tensor product of towers Algebra.TensorProduct.specialFibre_coordinates_sumElim_tmul 0 below · cited by 2 · depth 24
• Flat base change of a subalgebra of a domain-valued algebra Algebra.TensorProduct.isDomain_of_injective_of_flat 0 below · cited by 2 · depth 26
• Finite-group invariants commute with flat base change Algebra.TensorProduct.injective_map_fixedPoints_val_and_range_eq_of_flat 0 below · cited by 2 · depth 29
• Primes over both closed points are kernels of κ(A)-characters Algebra.TensorProduct.exists_ringHom_residueField_eq_ker_lift_of_isPrime_of_isAlgClosed 0 below · cited by 2 · depth 30
• Reduced fibre over a perfect residue field under local base change Algebra.TensorProduct.isReduced_residueField_tensorProduct_of_perfectField 1 below · cited by 4 · depth 30
• Surjectivity after base change descends to a f.g. subalgebra Algebra.TensorProduct.exists_fg_subalgebra_surjective_map_of_surjective_map 0 below · cited by 1 · depth 31
• Trivial idempotents persist under base change from an algebraically closed field Algebra.TensorProduct.nontrivial_and_forall_isIdempotentElem_of_isAlgClosed 0 below · cited by 1 · depth 31
• Transcendence degree and minimality over a generic fibre point Algebra.TensorProduct.trdeg_quotient_le_and_mem_minimalPrimes_iff_of_mem_minimalPrimes 1 below · cited by 1 · depth 32
• Invariants and Hilbert 90 for L⊗_K F, L/K cyclic Algebra.TensorProduct.exists_one_tmul_eq_of_map_eq_and_exists_units_eq_map_mul_inv_of_prod_iterate_map_eq_one 0 below · cited by 2 · depth 33
• Tensor product commutes with direct limits of algebras Algebra.TensorProduct.isDirectLimit_map_of_isDirectLimit 0 below · cited by 4 · depth 33
• Base-changed norm equals product of Galois conjugates Algebra.TensorProduct.algebraMap_norm_eq_prod_congr_apply_of_isGalois 2 below · cited by 8 · depth 34
• Primary extensions: L ⊗_K Ω has prime nilradical Algebra.TensorProduct.nilradical_isPrime_of_isAlgebraic_of_forall_isSeparable_mem_range 1 below · cited by 1 · depth 34
• Tensor product over a monogenic base as a quotient Algebra.TensorProduct.nonempty_ringEquiv_quotient_span_tmul_sub_tmul_of_adjoin_singleton_eq_top 0 below · cited by 4 · depth 34
• Splitting of L⊗_K F over a Galois extension Algebra.TensorProduct.bijective_productMap_pi_comp_of_isGalois 0 below · cited by 1 · depth 35
• Transition isomorphism of two base changes is a graded descent datum Algebra.TensorProduct.descent_datum_trans_symm_of_apply_tmul 0 below · cited by 1 · depth 35
• Integrality of a generic element whose finite-part image is integral Algebra.TensorProduct.exists_eq_one_tmul_of_map_eq_one_tmul_of_mul_one_tmul_eq 0 below · cited by 1 · depth 35
• Primary extensions are linearly disjoint from separable ones Algebra.TensorProduct.isField_of_isSeparable_of_forall_isSeparable_mem_range 0 below · cited by 1 · depth 35
• Norms commute with base change along ι : E → F Algebra.TensorProduct.map_norm_eq_norm_map_of_rightAlgebra 0 below · cited by 1 · depth 35
• Cocycle condition for a transition isomorphism from comparison identities Algebra.TensorProduct.cocycle_trans_symm_of_comparison_identities 0 below · cited by 1 · depth 36

Algebra.adjoin 1

• Unramifiedness of O[e] at primes over mathfrak m_O Algebra.adjoin.isDiscreteValuationRing_localization_and_maximalIdeal_eq_of_separable_map 0 below · cited by 2 · depth 34