| Name | Category | Theorems |
|---|
instAlgebra 📖 | CompOp | 227 mathmath: RatFunc.mk_def_of_ne, Algebra.exists_unramified_of_isUnramifiedAt, RatFunc.ofFractionRing_mk', RatFunc.mk_coe_def, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection_apply, HasStandardEtaleSurjectionOn.isStandardEtale, ClassGroup.mk0_integralRep, Localization.algebraMap_injective_of_span_eq_top, PrimeSpectrum.preimageEquivFiber_symm_apply_coe, PrimeSpectrum.residueField_specComap, Localization.epi', FractionalIdeal.isPrincipal_of_isPrincipal_num, Ideal.exists_mem_span_singleton_map_residueField_eq, Ideal.ker_algebraMap_residueField, ClassGroup.Quot_mk_eq_mk, LocalizedModule.restrictScalars_map_eq, Polynomial.fiberEquivQuotient_tmul, Module.rankAtStalk_eq, IsDedekindRing.toIsIntegralClosure, instLiesOverFiberOfIsPrime, Localization.mk_eq_mk', MaximalSpectrum.toPiLocalization_apply_apply, Localization.algEquiv_apply, Module.freeLocus_localization, Module.FinitePresentation.exists_notMem_bijective, Localization.algEquiv_mk', Localization.localRingHom_mk', Algebra.basicOpen_subset_etaleLocus_iff_etale, Algebra.IsSmoothAt.exists_notMem_isStandardSmooth, instIsLocalizationAlgebraMapSubmonoidPrimeComplLocalization, AlgebraicGeometry.Scheme.basic_open_isOpenImmersion, Ideal.algebraMap_quotient_residueField_mk, AlgebraicGeometry.localRingHom_comp_stalkIso_apply, Algebra.QuasiFinite.instResidueField, Localization.localRingHom_to_map, Algebra.Generators.compLocalizationAwayAlgHom_toAlgHom_toComp, Algebra.basicOpen_subset_unramifiedLocus_iff, Localization.mk_algebraMap, Polynomial.UniversalCoprimeFactorizationRing.homEquiv_comp_snd, instIsSeparableFractionRingLocalizationAlgebraMapSubmonoidPrimeCompl, instFinitePresentationAway, AlgebraicGeometry.Scheme.isOpenImmersion_SpecMap_localizationAway, FractionalIdeal.isUnit_num, AlgebraicGeometry.Scheme.instIsOpenImmersionMapOfHomAwayAlgebraMap, LocalizedModule.map_surjective, FractionRing.algebraMap_liftAlgebra, PrimeSpectrum.coe_preimageHomeomorphFiber_apply_asIdeal, Algebra.FormallyEtale.instLocalization, instIsPushoutFractionRingPolynomial_1, Localization.AtPrime.eq_maximalIdeal_iff_comap_eq, IsLocalizedModule.map_surjective_iff_localizedModuleMap_surjective, PrimeSpectrum.coe_preimageOrderIsoFiber_symm_apply_coe_asIdeal, Localization.algHom_ext_iff, LocalizedModule.equivTensorProduct_symm_apply_tmul_one, LocalizedModule.equivTensorProduct_apply_mk, Localization.toLocalizationMap_eq_monoidOf, LocalizedModule.map_injective, coeSubmodule_differentIdeal_fractionRing, Ideal.Fiber.lift_residueField_surjective, Algebra.Generators.compLocalizationAwayAlgHom_X_inl, LocalizedModule.equivTensorProduct_symm_apply_tmul, RatFunc.mk_def, RatFunc.mk_eq_div', Ring.instIsScalarTowerSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure, Algebra.algebraMap_intNorm_fractionRing, Localization.epi, Ideal.algebraMap_residueField_surjective, HomogeneousLocalization.val_awayMap, Ring.instIsScalarTowerFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure_1, IsLocalization.instIsScalarTowerLocalizationAtPrime, Ideal.ResidueField.ringHom_ext_iff, WeierstrassCurve.Affine.CoordinateRing.mk_XYIdeal'_neg_mul, Algebra.basicOpen_subset_smoothLocus_iff_smooth, Polynomial.UniversalCoprimeFactorizationRing.homEquiv_comp_fst, Ideal.surjectiveOnStalks_residueField, Localization.algEquiv_mk, isIntegral_localization', PrimeSpectrum.preimageEquivFiber_apply_asIdeal, AlgebraicGeometry.Spec_map_localization_isIso, PrimeSpectrum.mem_image_comap_basicOpen, AlgebraicIndependent.lift_reprField, AlgHom.IsArithFrobAt.localize_algebraMap, Ideal.ResidueField.liftₐ_comp_toAlgHom, AlgebraicGeometry.Spec.germ_stalkMapIso_hom_assoc, Algebra.Generators.sq_ker_comp_le_ker_compLocalizationAwayAlgHom, Localization.mk_eq_mk'_apply, instIsScalarTowerAtPrimeFractionRing, LocalizedModule.coe_map_eq, Localization.AtPrime.mapPiEvalRingHom_comp_algebraMap, Algebra.QuasiFinite.finite_fiber, Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq_aux₂, Module.rankAtStalk_eq_finrank_tensorProduct, RatFunc.ofFractionRing_comp_algebraMap, Ideal.ResidueField.map_algebraMap, algebraMap_mk, Ideal.ResidueField.exists_smul_eq_tmul_one, map_equiv_traceDual, Localization.AtPrime.comap_maximalIdeal, Algebra.isUnramifiedAt_iff_map_eq, Ideal.relNorm_algebraMap', Localization.localAlgHom_apply, PrimeSpectrum.residueField_comap, Localization.algEquiv_symm_mk', RatFunc.liftRingHom_ofFractionRing_algebraMap, Algebra.basicOpen_subset_etaleLocus_iff, Ideal.relNorm_algebraMap, Localization.algEquiv_symm_mk, WittVector.exists_frobenius_solution_fractionRing, Algebra.Smooth.exists_span_eq_top_isStandardSmooth, IsGaloisGroup.toFractionRing, Localization.mk_one_eq_algebraMap, Algebra.IsSmoothAt.exists_notMem_smooth, Algebra.instEssFiniteTypeLocalization, Algebra.IsUnramifiedAt.not_minpoly_sq_dvd, instLiesOverResidueFieldBotIdeal, Localization.monoidOf_eq_algebraMap, IsLocalization.Away.instHMulAwayCoeRingHomAlgebraMap, IsLocalization.Away.instHMulAwayCoeRingHomAlgebraMap_1, Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq, Algebra.IsEtaleAt.exists_isStandardEtale, AlgebraicGeometry.Scheme.Spec.algebraMap_residueFieldIso_inv, WeierstrassCurve.Affine.CoordinateRing.mk_XYIdeal'_mul_mk_XYIdeal', AlgebraicIndependent.liftAlgHom_comp_reprField, Module.FinitePresentation.linearEquivMapExtendScalars_apply, ClassGroup.mk_eq_mk, Localization.isLocalization, instFiniteTypeAway, PrimeSpectrum.coe_primesOverOrderIsoFiber_apply_asIdeal, Ideal.IsDedekindDomain.ramificationIdx_eq_one_iff, AlgebraicGeometry.Spec.algebraMap_stalkIso_inv, ClassGroup.equivPic_symm_apply, instEssFiniteTypeResidueField, IsLocalizedModule.map_bijective_iff_localizedModuleMap_bijective, Ideal.ResidueField.algHom_ext_iff, Algebra.exists_formallyUnramified_of_isUnramifiedAt, localization_unit_isIso, Ideal.ResidueField.lift_algebraMap, WeierstrassCurve.Affine.Point.toClass_some, Algebra.FormallySmooth.instLocalization, TopCat.Presheaf.SubmonoidPresheaf.toLocalizationPresheaf_app, isNilpotent_tensor_residueField_iff, Algebra.weaklyQuasiFiniteAt_iff, PrimeSpectrum.coe_preimageOrderIsoFiber_apply_asIdeal, LocalizedModule.map_id, Module.mem_support_iff_nontrivial_residueField_tensorProduct, IsLocalization.instFiniteTypeLocalizationOfFGSubtypeMemSubmonoid, instIsSeparableFractionRingAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl, Localization.coe_algEquiv, AlgHom.IsArithFrobAt.isArithFrobAt_localize, RatFunc.mk_def_of_mem, LocalizedModule.algebraMap_mk, instFiniteResidueField, Algebra.exists_etale_of_isEtaleAt, AlgebraicIndependent.aevalEquivField_apply_coe, AlgebraicGeometry.basicOpenIsoSpecAway_inv_homOfLE_assoc, AlgebraicGeometry.isIso_SpecMap_stakMap_localization, Surreal.dyadicMap_apply, HomogeneousLocalization.Away.eventually_smul_mem, Algebra.IsAlgebraic.rank_fractionRing, instIsPushoutFractionRingPolynomial, IsLocalizedModule.map_injective_iff_localizedModuleMap_injective, AlgebraicGeometry.basicOpenIsoSpecAway_inv_homOfLE, instIsScalarTowerQuotientIdealResidueField, AlgebraicGeometry.Spec.algebraMap_stalkIso_inv_assoc, RatFunc.ofFractionRing_eq, PrimeSpectrum.range_comap_algebraMap_localization_compl_eq_range_comap_quotientMk, AlgebraicGeometry.Scheme.affineOpenCoverOfSpanRangeEqTop_f, HomogeneousLocalization.den_smul_val, Algebra.IsUnramifiedAt.exists_notMem_forall_ne_mem_and_adjoin_eq_top, AlgebraicGeometry.Scheme.Spec.algebraMap_residueFieldIso_inv_assoc, WittVector.exists_frobenius_solution_fractionRing_aux, Algebra.Generators.compLocalizationAwayAlgHom_relation_eq_zero, Polynomial.UniversalCoprimeFactorizationRing.factor₁_mul_factor₂, PrimeSpectrum.coe_preimageHomeomorphFiber_symm_apply_coe_asIdeal, RatFunc.mk_one', Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq_aux, IsLocalization.isLocalization_atPrime_localization_atPrime, exists_bijective_map_powers, AlgebraicIndependent.aevalEquivField_algebraMap_apply_coe, Algebra.IsAlgebraic.rank_fractionRing_mvPolynomial, PrimeSpectrum.coe_primesOverOrderIsoFiber_symm_apply_coe, LocalizedModule.map_mk, RingHom.locally_iff_finite, Algebra.algebraMap_intTrace_fractionRing, AlgebraicGeometry.Spec.germ_stalkMapIso_hom, localization_unit_isIso', PrimeSpectrum.mem_image_comap_zeroLocus_sdiff, RatFunc.toFractionRingRingEquiv_symm_eq, IsLocalization.ideal_eq_iInf_comap_map_away, Polynomial.residueFieldMapCAlgEquiv_symm_X, ClassGroup.equivPic_apply, WeierstrassCurve.Affine.CoordinateRing.XYIdeal'_eq, Ideal.algebraMap_residueField_eq_zero, Ideal.absNorm_algebraMap, Ideal.ResidueField.liftₐ_algebraMap, Algebra.basicOpen_subset_smoothLocus_iff, Ring.instIsScalarTowerNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure_1, Algebra.QuasiFinite.instIsArtinianRingFiber, instIsLocalizedModuleLinearMapIdLocalizationLocalizedModuleMapOfFinitePresentation, ClassGroup.integralRep_mem_nonZeroDivisors, AlgebraicGeometry.localRingHom_comp_stalkIso, Localization.AtPrime.map_eq_maximalIdeal, instFiniteDimensionalFractionRingOfFinite, Polynomial.residueFieldMapCAlgEquiv_algebraMap, Surreal.dyadicMap_apply_pow, RatFunc.toFractionRingAlgEquiv_apply, Localization.awayMap_awayMap_surjective, Algebra.IsAlgebraic.rank_fractionRing_polynomial, ClassGroup.mk_def, Ideal.Fiber.exists_smul_eq_one_tmul, FractionRing.mk_eq_div, Ideal.ResidueField.mapₐ_apply, WeierstrassCurve.Affine.Point.toClass_apply, Algebra.Etale.instAway, PrimeSpectrum.nontrivial_iff_mem_rangeComap, Polynomial.instEtaleUniversalCoprimeFactorizationRing, Localization.AtPrime.mapPiEvalRingHom_algebraMap_apply, Algebra.QuasiFinite.instLocalization, instIsPushoutFractionRingMvPolynomial_1, RatFunc.ofFractionRing_algebraMap, Algebra.FormallyUnramified.instLocalization, Algebra.instIsStandardOpenImmersionAway, Module.FinitePresentation.linearEquivMapExtendScalars_symm_apply, Localization.coe_algEquiv_symm, instIsPushoutFractionRingMvPolynomial, Localization.algEquiv_symm_apply, RatFunc.toFractionRing_eq
|
instCommRing 📖 | CompOp | 145 mathmath: Algebra.IsUnramifiedAt.exists_primesOver_under_adjoin_eq_singleton_and_residueField_bijective, Algebra.exists_unramified_of_isUnramifiedAt, HasStandardEtaleSurjectionOn.isStandardEtale, ClassGroup.mk0_integralRep, PrimeSpectrum.preimageEquivFiber_symm_apply_coe, PrimeSpectrum.residueField_specComap, Localization.epi', FractionalIdeal.isPrincipal_of_isPrincipal_num, Ideal.exists_mem_span_singleton_map_residueField_eq, Ideal.ker_algebraMap_residueField, ClassGroup.Quot_mk_eq_mk, Polynomial.fiberEquivQuotient_tmul, Module.rankAtStalk_eq, IsDedekindRing.toIsIntegralClosure, instLiesOverFiberOfIsPrime, Module.freeLocus_localization, Algebra.basicOpen_subset_etaleLocus_iff_etale, instIsAlgebraicResidueFieldOfIsIntegral, Algebra.IsSmoothAt.exists_notMem_isStandardSmooth, AlgebraicGeometry.Scheme.basic_open_isOpenImmersion, Ideal.algebraMap_quotient_residueField_mk, AlgebraicGeometry.localRingHom_comp_stalkIso_apply, Algebra.QuasiFinite.instResidueField, Algebra.basicOpen_subset_unramifiedLocus_iff, Algebra.instFiniteResidueFieldOfQuasiFiniteAt, Algebra.WeaklyQuasiFiniteAt.finite_residueField, instIsSeparableFractionRingLocalizationAlgebraMapSubmonoidPrimeCompl, AlgebraicGeometry.Scheme.isOpenImmersion_SpecMap_localizationAway, FractionalIdeal.isUnit_num, AlgebraicGeometry.Scheme.instIsOpenImmersionMapOfHomAwayAlgebraMap, FractionRing.isSeparable_of_isLocalization, PrimeSpectrum.coe_preimageHomeomorphFiber_apply_asIdeal, AlgebraicGeometry.stalkwise_SpecMap_iff, Algebra.FormallyEtale.instLocalization, PrimeSpectrum.coe_preimageOrderIsoFiber_symm_apply_coe_asIdeal, instEssFiniteTypeResidueField_1, Localization.AtPrime.isDedekindDomain, Ideal.Fiber.lift_residueField_surjective, Algebra.algebraMap_intNorm_fractionRing, Localization.epi, Ideal.algebraMap_residueField_surjective, Algebra.IsSmoothAt.exists_isStandardEtale_mvPolynomial, Ideal.ResidueField.ringHom_ext_iff, instIsSeparableResidueFieldOfQuotientIdeal, Algebra.basicOpen_subset_smoothLocus_iff_smooth, Ideal.surjectiveOnStalks_residueField, isIntegral_localization', PrimeSpectrum.preimageEquivFiber_apply_asIdeal, AlgebraicGeometry.Spec_map_localization_isIso, PrimeSpectrum.mem_image_comap_basicOpen, Ideal.ResidueField.liftₐ_comp_toAlgHom, AlgebraicGeometry.Spec.germ_stalkMapIso_hom_assoc, instIsAlgebraicQuotientIdealResidueField, Algebra.QuasiFinite.finite_fiber, Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq_aux₂, Algebra.QuasiFinite.instFiniteResidueField, Ideal.ResidueField.map_algebraMap, algebraMap_mk, AlgebraicGeometry.Scheme.Spec.residue_residueFieldIso_hom_assoc, Ideal.ResidueField.exists_smul_eq_tmul_one, Algebra.isUnramifiedAt_iff_map_eq, PrimeSpectrum.residueField_comap, Algebra.instFiniteResidueFieldOfIsUnramifiedAt, Ring.instIsSeparableFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure, Algebra.basicOpen_subset_etaleLocus_iff, RingHom.SurjectiveOnStalks.residueFieldMap_bijective, instIsTopologicalRingLocalization, WittVector.exists_frobenius_solution_fractionRing, Algebra.Smooth.exists_span_eq_top_isStandardSmooth, Algebra.IsSmoothAt.exists_notMem_smooth, Algebra.instEssFiniteTypeLocalization, Algebra.IsUnramifiedAt.not_minpoly_sq_dvd, Algebra.instIsSeparableResidueFieldOfIsUnramifiedAt, instLiesOverResidueFieldBotIdeal, IsDedekindDomainDvr.is_dvr_at_nonzero_prime, Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq, RingHom.HoldsForLocalization.localRingHom, Algebra.IsEtaleAt.exists_isStandardEtale, AlgebraicGeometry.Scheme.Spec.algebraMap_residueFieldIso_inv, ClassGroup.mk_eq_mk, PrimeSpectrum.coe_primesOverOrderIsoFiber_apply_asIdeal, AlgebraicGeometry.Spec.algebraMap_stalkIso_inv, AlgebraicGeometry.stalkwise_Spec_map_iff, instEssFiniteTypeResidueField, Ideal.ResidueField.algHom_ext_iff, Algebra.exists_formallyUnramified_of_isUnramifiedAt, localization_unit_isIso, Ideal.ResidueField.lift_algebraMap, Algebra.FormallySmooth.instLocalization, TopCat.Presheaf.SubmonoidPresheaf.toLocalizationPresheaf_app, isNilpotent_tensor_residueField_iff, Algebra.weaklyQuasiFiniteAt_iff, PrimeSpectrum.coe_preimageOrderIsoFiber_apply_asIdeal, Module.mem_support_iff_nontrivial_residueField_tensorProduct, instIsSeparableFractionRingAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl, AlgHom.IsArithFrobAt.isArithFrobAt_localize, instFiniteResidueField, Algebra.exists_etale_of_isEtaleAt, AlgebraicGeometry.basicOpenIsoSpecAway_inv_homOfLE_assoc, AlgebraicGeometry.isIso_SpecMap_stakMap_localization, Ideal.injective_algebraMap_quotient_residueField, RingHom.Flat.localRingHom, AlgebraicGeometry.basicOpenIsoSpecAway_inv_homOfLE, instIsScalarTowerQuotientIdealResidueField, AlgebraicGeometry.Spec.algebraMap_stalkIso_inv_assoc, AlgebraicGeometry.Scheme.affineOpenCoverOfSpanRangeEqTop_f, Algebra.IsUnramifiedAt.exists_notMem_forall_ne_mem_and_adjoin_eq_top, AlgebraicGeometry.Scheme.Spec.algebraMap_residueFieldIso_inv_assoc, WittVector.exists_frobenius_solution_fractionRing_aux, Algebra.instFormallyUnramifiedAtPrimeOfIsUnramifiedAt, PrimeSpectrum.coe_preimageHomeomorphFiber_symm_apply_coe_asIdeal, RingHom.RespectsIso.isLocalization_away_iff, Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq_aux, PrimeSpectrum.coe_primesOverOrderIsoFiber_symm_apply_coe, RingHom.locally_iff_finite, Algebra.algebraMap_intTrace_fractionRing, AlgebraicGeometry.Spec.germ_stalkMapIso_hom, localization_unit_isIso', instIsDedekindDomainLocalizationAlgebraMapSubmonoidPrimeCompl, PrimeSpectrum.mem_image_comap_zeroLocus_sdiff, Polynomial.residueFieldMapCAlgEquiv_symm_X, Algebra.isSeparable_residueField_iff, WeierstrassCurve.Affine.CoordinateRing.XYIdeal'_eq, Ideal.algebraMap_residueField_eq_zero, Ideal.bijective_algebraMap_quotient_residueField, Ideal.ResidueField.liftₐ_algebraMap, Algebra.basicOpen_subset_smoothLocus_iff, Algebra.QuasiFinite.instIsArtinianRingFiber, ClassGroup.integralRep_mem_nonZeroDivisors, AlgebraicGeometry.localRingHom_comp_stalkIso, AlgebraicGeometry.Scheme.localRingHom_comp_stalkIso, Polynomial.residueFieldMapCAlgEquiv_algebraMap, ClassGroup.mk_def, instIsIntegralAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl, Ideal.Fiber.exists_smul_eq_one_tmul, AlgebraicGeometry.Scheme.Spec.residue_residueFieldIso_hom, Ideal.ResidueField.mapₐ_apply, AlgebraicGeometry.Scheme.localRingHom_comp_stalkIso_apply, Algebra.Etale.instAway, PrimeSpectrum.nontrivial_iff_mem_rangeComap, Polynomial.instEtaleUniversalCoprimeFactorizationRing, Polynomial.residueFieldMapCAlgEquiv_symm_C, Algebra.QuasiFinite.instLocalization, Algebra.FormallyUnramified.instLocalization, instIsFractionRingQuotientIdealResidueField
|
instCommSemiring 📖 | CompOp | 101 mathmath: RatFunc.mk_def_of_ne, RatFunc.ofFractionRing_mk', RatFunc.mk_coe_def, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection_apply, instIsScalarTowerLocalizationAlgebraMapSubmonoidPrimeCompl, FractionRing.instIsScalarTower, Module.Flat.localizedModule, instIsScalarTowerLocalizationAlgebraMapSubmonoidPrimeComplFractionRing, Localization.mk_eq_mk', Localization.algEquiv_apply, Localization.algEquiv_mk', Localization.localRingHom_mk', instIsLocalizationAlgebraMapSubmonoidPrimeComplLocalization, Polynomial.UniversalCoprimeFactorizationRing.exists_liesOver_residueFieldMap_bijective, AlgebraicGeometry.localRingHom_comp_stalkIso_apply, instIsScalarTowerAtPrimeFractionRing_1, instIsFractionRingAtPrimeFractionRing, Module.associatedPrimes.mem_associatePrimes_localizedModule_atPrime_of_mem_associated_primes, instIsScalarTowerAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl, instIsScalarTowerAtPrimeLocalizationAlgebraMapSubmonoidPrimeComplFractionRing, instIsLocalHomAtPrimeRingHomAlgebraMap, FractionRing.algebraMap_liftAlgebra, instIsPushoutFractionRingPolynomial_1, Localization.AtPrime.eq_maximalIdeal_iff_comap_eq, Localization.toLocalizationMap_eq_monoidOf, coeSubmodule_differentIdeal_fractionRing, Algebra.Generators.compLocalizationAwayAlgHom_X_inl, Ring.instIsScalarTowerSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure, FractionRing.instIsScalarTower_1, HomogeneousLocalization.val_awayMap, Ring.instIsScalarTowerFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure_1, IsLocalization.instIsScalarTowerLocalizationAtPrime, IsFractionRing.instAtPrimeFractionRing, isIntegral_localization', Localization.mk_eq_mk'_apply, instIsScalarTowerAtPrimeFractionRing, Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq_aux₂, AlgebraicGeometry.Scheme.Spec.residue_residueFieldIso_hom_assoc, Localization.AtPrime.comap_maximalIdeal, FractionRing.instIsFractionRing, Algebra.isUnramifiedAt_iff_map_eq, Ideal.relNorm_algebraMap', Localization.finite_of_primesOver_eq_singleton, Ring.instIsSeparableFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure, Localization.algEquiv_symm_mk', Ideal.relNorm_algebraMap, IsGaloisGroup.toFractionRing, IsLocalization.Away.instHMulAwayCoeRingHomAlgebraMap, IsLocalization.Away.instHMulAwayCoeRingHomAlgebraMap_1, instFlatAtPrime, Module.FinitePresentation.linearEquivMapExtendScalars_apply, Localization.instIsTorsionFreeAtPrimeAlgebraMapSubmonoidPrimeComplOfIsDomain, Localization.isLocalization, Ideal.IsDedekindDomain.ramificationIdx_eq_one_iff, ClassGroup.equivPic_symm_apply, instFiniteAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl, Ring.instIsScalarTowerFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure, instFiniteFractionRingLocalizationAlgebraMapSubmonoidNonZeroDivisors, Ring.instFiniteDimensionalFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure, IsLocalization.instIsScalarTowerAtPrimeFractionRing, Localization.AtPrime.instIsScalarTower_1, Localization.AtPrime.instIsScalarTower, instIsSeparableFractionRingAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl, Localization.coe_algEquiv, AlgHom.IsArithFrobAt.isArithFrobAt_localize, Module.associatedPrimes.mem_associatedPrimes_atPrime_of_mem_associatedPrimes, RatFunc.mk_def_of_mem, LocalizedModule.algebraMap_mk, Surreal.dyadicMap_apply, Algebra.IsAlgebraic.rank_fractionRing, instIsPushoutFractionRingPolynomial, instFiniteLocalizationAlgebraMapSubmonoidPrimeCompl, Module.Invertible.instLocalizationLocalizedModule, ModuleCat.localizedModuleMap_hom_apply, RatFunc.ofFractionRing_eq, PrimeSpectrum.range_comap_algebraMap_localization_compl_eq_range_comap_quotientMk, IsLocalization.isLocalization_atPrime_localization_atPrime, FractionRing.isScalarTower_liftAlgebra, Algebra.IsAlgebraic.rank_fractionRing_mvPolynomial, instIsTorsionFreeLocalizationAlgebraMapSubmonoidPrimeCompl_2, instIsScalarTowerLocalizationAlgebraMapSubmonoid, RatFunc.toFractionRingRingEquiv_symm_eq, ClassGroup.equivPic_apply, Ideal.absNorm_algebraMap, instIsFractionRingLocalizationAlgebraMapSubmonoidPrimeComplFractionRing, Ring.instIsScalarTowerNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure_1, instIsScalarTowerLocalizationAlgebraMapSubmonoidPrimeCompl_1, Localization.AtPrime.map_eq_maximalIdeal, instFiniteDimensionalFractionRingOfFinite, Polynomial.UniversalCoprimeFactorizationRing.isCoprime_factor₁_factor₂, Surreal.dyadicMap_apply_pow, Localization.awayMap_awayMap_surjective, Algebra.IsAlgebraic.rank_fractionRing_polynomial, AlgebraicGeometry.Scheme.Spec.residue_residueFieldIso_hom, instIsPushoutFractionRingMvPolynomial_1, Algebra.instIsStandardOpenImmersionAway, Module.FinitePresentation.linearEquivMapExtendScalars_symm_apply, Localization.coe_algEquiv_symm, instIsPushoutFractionRingMvPolynomial, Localization.algEquiv_symm_apply, RatFunc.toFractionRing_eq
|
instDivisionRingNonZeroDivisors 📖 | CompOp | 10 mathmath: RatFunc.mk_def, RatFunc.mk_eq_div', RatFunc.ofFractionRing_div, WittVector.exists_frobenius_solution_fractionRing, WittVector.StandardOneDimIsocrystal.frobenius_apply, Ring.instFiniteDimensionalFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure, WittVector.exists_frobenius_solution_fractionRing_aux, RatFunc.div_def, instFiniteDimensionalFractionRingOfFinite, FractionRing.mk_eq_div
|
instFieldNonZeroDivisors 📖 | CompOp | — |
instModule 📖 | CompOp | 33 mathmath: Module.Finite.instLocalizationLocalizedModule, LocalizedModule.restrictScalars_map_eq, Module.Flat.localizedModule, Module.freeLocus_localization, Module.FinitePresentation.exists_notMem_bijective, Module.basicOpen_subset_freeLocus_iff, Module.associatedPrimes.mem_associatePrimes_localizedModule_atPrime_of_mem_associated_primes, LocalizedModule.map_surjective, IsLocalizedModule.map_surjective_iff_localizedModuleMap_surjective, LocalizedModule.equivTensorProduct_symm_apply_tmul_one, LocalizedModule.equivTensorProduct_apply_mk, LocalizedModule.map_injective, LocalizedModule.equivTensorProduct_symm_apply_tmul, LocalizedModule.coe_map_eq, Module.FinitePresentation.exists_free_localizedModule_powers, Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq_aux₂, Module.rankAtStalk_eq_finrank_tensorProduct, instFinitePresentationLocalizationLocalizedModule, instIsLocalizedModuleQuotientSubmoduleLocalizedModuleLocalizationLocalizedToLocalizedQuotient, Module.FinitePresentation.linearEquivMapExtendScalars_apply, Module.FinitePresentation.exists_lift_equiv_of_isLocalizedModule, IsLocalizedModule.map_bijective_iff_localizedModuleMap_bijective, LocalizedModule.map_id, Module.associatedPrimes.mem_associatedPrimes_atPrime_of_mem_associatedPrimes, Module.Invertible.instLocalizationLocalizedModule, IsLocalizedModule.map_injective_iff_localizedModuleMap_injective, exists_bijective_map_powers, LocalizedModule.map_mk, Module.mem_freeLocus, IsLocalizedModule.instIsTorsionFreeLocalizationLocalizedModuleOfIsDomain, instIsLocalizedModuleLinearMapIdLocalizationLocalizedModuleMapOfFinitePresentation, Module.FinitePresentation.exists_basis_localizedModule_powers, Module.FinitePresentation.linearEquivMapExtendScalars_symm_apply
|
instModuleOfIsScalarTower 📖 | CompOp | 62 mathmath: IsLocalizedModule.iso_symm_apply', LocalizedModule.restrictScalars_map_eq, nsmul_eq_nsmul, Module.FinitePresentation.exists_notMem_bijective, IsLocalizedModule.iso_symm_apply, IsLocalizedModule.iso_apply_mk, LocalizedModule.divBy_apply, LocalizedModule.divBy_mul_by, LocalizedModule.map_surjective, IsLocalizedModule.map_surjective_iff_localizedModuleMap_surjective, LocalizedModule.mem_ker_mkLinearMap_iff, IsLocalizedModule.fromLocalizedModule.bij, LocalizedModule.equivTensorProduct_symm_apply_tmul_one, LocalizedModule.equivTensorProduct_apply_mk, LocalizedModule.map_injective, LocalizedModule.equivTensorProduct_symm_apply_tmul, Module.FinitePresentation.linearEquivMap_symm_apply, IsLocalizedModule.iso_symm_comp, IsLocalizedModule.fromLocalizedModule.inj, Algebra.WeaklyQuasiFiniteAt.finite_locoalization, LocalizedModule.coe_map_eq, zsmul_eq_zsmul, LocalizedModule.subsingleton_iff_ker_eq_top, Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq_aux₂, IsLocalizedModule.fromLocalizedModule_mk, Module.rankAtStalk_eq_finrank_tensorProduct, Module.FinitePresentation.linearEquivMap_apply, IsLocalizedModule.lift_comp_iso, localizedModuleIsLocalizedModule, instIsLocalizedModuleQuotientSubmoduleLocalizedModuleLocalizationLocalizedToLocalizedQuotient, LocalizedModule.lift_comp, instIsTorsionFreeLocalizationAlgebraMapSubmonoidPrimeCompl_1, Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq, Module.FinitePresentation.linearEquivMapExtendScalars_apply, IsLocalizedModule.iso_symm_apply_aux, ClassGroup.equivPic_symm_apply, LocalizedModule.lift_mk, Module.FinitePresentation.exists_lift_equiv_of_isLocalizedModule, instIsTorsionFreeLocalizationAlgebraMapSubmonoidPrimeCompl, IsLocalizedModule.map_bijective_iff_localizedModuleMap_bijective, LocalizedModule.mul_by_divBy, LocalizedModule.map_exact, LocalizedModule.map_id, AlgebraicGeometry.StructureSheaf.Localizations.comapFun_mk, LocalizedModule.lift_mk_one, IsLocalizedModule.mk_eq_mk', IsLocalizedModule.map_injective_iff_localizedModuleMap_injective, exists_bijective_map_powers, IsLocalizedModule.iso_localizedModule_eq_refl, LocalizedModule.map_mk, IsLocalizedModule.fromLocalizedModule.surj, Localization.flat, MvRatFunc.rank_eq_max_lift, ClassGroup.equivPic_apply, IsLocalizedModule.map_iso_commute, instIsLocalizedModuleLinearMapIdLocalizationLocalizedModuleMapOfFinitePresentation, IsLocalizedModule.map_LocalizedModules, IsLocalizedModule.lift_iso, LocalizedModule.mkLinearMap_apply, Module.FinitePresentation.exists_basis_localizedModule_powers, IsLocalizedModule.iso_mk_one, Module.FinitePresentation.linearEquivMapExtendScalars_symm_apply
|
instRing 📖 | CompOp | 24 mathmath: ModuleCat.localizedModule_functor_map_exact, instIsSeparableFractionRingLocalizationAlgebraMapSubmonoidPrimeCompl, FractionRing.isSeparable_of_isLocalization, ModuleCat.instAdditiveLocalizationLocalizedModule_functor, Algebra.algebraMap_intNorm_fractionRing, Localization.mk_intCast, ModuleCat.localizedModule_isLocalizedModule, isIntegral_localization', ModuleCat.instPreservesFiniteColimitsLocalizationLocalizedModule_functor, ModuleCat.localizedModule_functor_map, ModuleCat.instIsScalarTowerLocalizationCarrierLocalizedModule, HomogeneousLocalization.val_intCast, HomogeneousLocalization.val_natCast, instIsLocalizedModuleQuotientSubmoduleLocalizedModuleLocalizationLocalizedToLocalizedQuotient, WittVector.exists_frobenius_solution_fractionRing, WittVector.StandardOneDimIsocrystal.frobenius_apply, instIsSeparableFractionRingAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl, IsFractionRing.charP, ModuleCat.localizedModuleMap_hom_apply, ModuleCat.localizedModule_functor_obj, WittVector.exists_frobenius_solution_fractionRing_aux, ModuleCat.instPreservesFiniteLimitsLocalizationLocalizedModule_functor, instIsIntegralAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl, IsFractionRing.charZero
|
instSemiring 📖 | CompOp | 203 mathmath: PrimeSpectrum.mapPiLocalization_id, Module.Finite.instLocalizationLocalizedModule, MaximalSpectrum.mapPiLocalization_bijective, Localization.algebraMap_injective_of_span_eq_top, Localization.epi', instIsScalarTowerLocalizationAlgebraMapSubmonoidPrimeCompl, LocalizedModule.restrictScalars_map_eq, Localization.AtPrime.mapPiEvalRingHom_bijective, WittVector.IsocrystalHom.frob_equivariant, instIsScalarTowerLocalizationAlgebraMapSubmonoidPrimeComplFractionRing, universalHom_apply, MaximalSpectrum.toPiLocalization_apply_apply, Localization.algEquiv_apply, Module.FinitePresentation.exists_notMem_bijective, Localization.algEquiv_mk', Localization.localRingHom_mk', AlgebraicGeometry.Scheme.basic_open_isOpenImmersion, Polynomial.UniversalCoprimeFactorizationRing.exists_liesOver_residueFieldMap_bijective, AlgebraicGeometry.localRingHom_comp_stalkIso_apply, HomogeneousLocalization.range_awayMapAux_subset, instIsScalarTowerAtPrimeFractionRing_1, Module.basicOpen_subset_freeLocus_iff, Localization.localRingHom_to_map, Algebra.Generators.compLocalizationAwayAlgHom_toAlgHom_toComp, instIsScalarTowerAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl, Localization.localRingHom_injective_of_primesOver_eq_singleton, Localization.mk_algebraMap, Polynomial.UniversalCoprimeFactorizationRing.homEquiv_comp_snd, instIsSeparableFractionRingLocalizationAlgebraMapSubmonoidPrimeCompl, Localization.AtPrime.isLocalRing, IsLocalization.instIsNoetherianRingLocalization, instIsScalarTowerAtPrimeLocalizationAlgebraMapSubmonoidPrimeComplFractionRing, instFinitePresentationAway, AlgebraicGeometry.Scheme.isOpenImmersion_SpecMap_localizationAway, AlgebraicGeometry.Scheme.instIsOpenImmersionMapOfHomAwayAlgebraMap, instIsLocalHomAtPrimeRingHomAlgebraMap, LocalizedModule.map_surjective, MaximalSpectrum.mapPiLocalization_naturality, Localization.AtPrime.eq_maximalIdeal_iff_comap_eq, PrimeSpectrum.toPiLocalization_surjective_of_discreteTopology, Algebra.QuasiFiniteAt.exists_fg_and_exists_notMem_and_awayMap_bijective, IsLocalizedModule.map_surjective_iff_localizedModuleMap_surjective, Localization.algHom_ext_iff, LocalizedModule.equivTensorProduct_symm_apply_tmul_one, LocalizedModule.equivTensorProduct_apply_mk, AlgebraicGeometry.StructureSheaf.comap_apply, LocalizedModule.map_injective, Algebra.Generators.compLocalizationAwayAlgHom_X_inl, LocalizedModule.equivTensorProduct_symm_apply_tmul, RatFunc.mk_def, RatFunc.mk_eq_div', PrimeSpectrum.mapPiLocalization_bijective, Algebra.algebraMap_intNorm_fractionRing, Localization.epi, PrimeSpectrum.toPiLocalization_not_surjective_of_infinite, Algebra.IsSmoothAt.exists_isStandardEtale_mvPolynomial, HomogeneousLocalization.val_awayMap, Ring.instIsScalarTowerFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure_1, Localization.awayMap_surjective_iff, IsLocalization.instIsScalarTowerLocalizationAtPrime, AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff', PrimeSpectrum.mapPiLocalization_comp, Polynomial.UniversalCoprimeFactorizationRing.homEquiv_comp_fst, Localization.algEquiv_mk, AlgebraicGeometry.Spec_map_localization_isIso, AlgebraicIndependent.lift_reprField, WittVector.IsocrystalEquiv.frob_equivariant, AlgHom.IsArithFrobAt.localize_algebraMap, numeratorRingHom_apply, Algebra.Generators.sq_ker_comp_le_ker_compLocalizationAwayAlgHom, Localization.localRingHom_id, instIsScalarTowerAtPrimeFractionRing, LocalizedModule.coe_map_eq, Localization.mapPiEvalRingHom_bijective, Localization.AtPrime.mapPiEvalRingHom_comp_algebraMap, Module.FinitePresentation.exists_free_localizedModule_powers, MaximalSpectrum.mapPiLocalization_id, PrimeSpectrum.mapPiLocalization_naturality, Module.rankAtStalk_eq_finrank_tensorProduct, RatFunc.ofFractionRing_comp_algebraMap, ModuleCat.instIsScalarTowerLocalizationCarrierLocalizedModule, map_equiv_traceDual, HomogeneousLocalization.instIsScalarTowerSubtypeMemOfNatLocalization, Localization.AtPrime.comap_maximalIdeal, Algebra.isUnramifiedAt_iff_map_eq, Ideal.relNorm_algebraMap', Localization.finite_of_primesOver_eq_singleton, Localization.localAlgHom_apply, PrimeSpectrum.toPiLocalization_bijective, instFinitePresentationLocalizationLocalizedModule, Ring.instIsSeparableFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure, instIsPrincipalIdealRingLocalizationAlgebraMapSubmonoidPrimeComplOfIsDedekindDomainOfFiniteOfNeZeroIdeal, Localization.algEquiv_symm_mk', RatFunc.liftRingHom_ofFractionRing_algebraMap, IsLocalization.isDomain_localization, Ideal.relNorm_algebraMap, PrimeSpectrum.discreteTopology_iff_toPiLocalization_surjective, WittVector.inv_pair₂, instIsLocalizedModuleQuotientSubmoduleLocalizedModuleLocalizationLocalizedToLocalizedQuotient, Localization.algEquiv_symm_mk, RingHom.surjective_localRingHom_of_surjective, IsGaloisGroup.toFractionRing, Localization.mk_one_eq_algebraMap, Localization.exists_awayMap_bijective_of_residueField_surjective, WittVector.inv_pair₁, PrimeSpectrum.piLocalizationToMaximal_comp_toPiLocalization, Localization.mk_natCast, Localization.monoidOf_eq_algebraMap, IsLocalization.instCompatibleSMulLocalizationOfIsScalarTower_1, PrimeSpectrum.piLocalizationToMaximal_surjective, instFlatAtPrime, Module.FinitePresentation.linearEquivMapExtendScalars_apply, Localization.instIsTorsionFreeAtPrimeAlgebraMapSubmonoidPrimeComplOfIsDomain, instFiniteTypeAway, IsArtinianRing.instLocalization, Ideal.IsDedekindDomain.ramificationIdx_eq_one_iff, ClassGroup.equivPic_symm_apply, Module.FinitePresentation.exists_lift_equiv_of_isLocalizedModule, instFiniteAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl, Ring.instIsScalarTowerFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure, IsLocalizedModule.map_bijective_iff_localizedModuleMap_bijective, localization_unit_isIso, WittVector.StandardOneDimIsocrystal.frobenius_apply, instFiniteFractionRingLocalizationAlgebraMapSubmonoidNonZeroDivisors, MaximalSpectrum.mapPiLocalization_comp, HomogeneousLocalization.val_awayMap_eq_aux, Ring.instFiniteDimensionalFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure, TopCat.Presheaf.SubmonoidPresheaf.toLocalizationPresheaf_app, IsLocalization.instIsScalarTowerAtPrimeFractionRing, Localization.AtPrime.instIsScalarTower_1, Algebra.weaklyQuasiFiniteAt_iff, Localization.AtPrime.instIsScalarTower, LocalizedModule.map_id, HomogeneousLocalization.awayMapAux_mk, IsLocalization.instFiniteTypeLocalizationOfFGSubtypeMemSubmonoid, instIsSeparableFractionRingAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl, Localization.coe_algEquiv, AlgebraicIndependent.aevalEquivField_apply_coe, AlgebraicGeometry.isIso_SpecMap_stakMap_localization, HomogeneousLocalization.Away.eventually_smul_mem, Algebra.IsAlgebraic.rank_fractionRing, instFiniteLocalizationAlgebraMapSubmonoidPrimeCompl, IsLocalizedModule.map_injective_iff_localizedModuleMap_injective, MaximalSpectrum.toPiLocalization_injective, PrimeSpectrum.range_comap_algebraMap_localization_compl_eq_range_comap_quotientMk, AlgebraicGeometry.Scheme.affineOpenCoverOfSpanRangeEqTop_f, HomogeneousLocalization.den_smul_val, IsLocalization.instCompatibleSMulLocalizationOfIsScalarTower, RingHom.SurjectiveOnStalks.localRingHom_surjective, WittVector.exists_frobenius_solution_fractionRing_aux, Algebra.Generators.compLocalizationAwayAlgHom_relation_eq_zero, Localization.localRingHom_bijective_of_saturated_inf_eq_top, MaximalSpectrum.toPiLocalization_not_surjective_of_infinite, Polynomial.UniversalCoprimeFactorizationRing.factor₁_mul_factor₂, RatFunc.mk_one', Localization.awayMap_injective_iff, IsLocalization.isLocalization_atPrime_localization_atPrime, exists_bijective_map_powers, AlgebraicIndependent.aevalEquivField_algebraMap_apply_coe, Algebra.IsAlgebraic.rank_fractionRing_mvPolynomial, Localization.localRingHom_comp, LocalizedModule.map_mk, instIsTorsionFreeLocalizationAlgebraMapSubmonoidPrimeCompl_2, Localization.isLocalHom_localRingHom, instIsScalarTowerLocalizationAlgebraMapSubmonoid, PrimeSpectrum.piLocalizationToMaximal_bijective, PrimeSpectrum.toPiLocalization_injective, RingHom.locally_iff_finite, IsLocalization.instIsDomainLocalizationAlgebraMapSubmonoidPrimeComplOfFaithfulSMul, Localization.localRingHom_bijective_of_not_conductor_le, Algebra.algebraMap_intTrace_fractionRing, Localization.localRingHom_surjective_of_primesOver_eq_singleton, localization_unit_isIso', IsLocalization.ideal_eq_iInf_comap_map_away, Module.mem_freeLocus, ClassGroup.equivPic_apply, Ideal.absNorm_algebraMap, AlgebraicGeometry.StructureSheaf.comapₗ_eq_localRingHom, IsLocalizedModule.instIsTorsionFreeLocalizationLocalizedModuleOfIsDomain, Localization.awayLift_mk, instIsLocalizedModuleLinearMapIdLocalizationLocalizedModuleMapOfFinitePresentation, PrimeSpectrum.maximalSpectrumToPiLocalization_surjective_of_discreteTopology, RingHom.surjectiveOnStalks_iff_forall_maximal, instIsScalarTowerLocalizationAlgebraMapSubmonoidPrimeCompl_1, AlgebraicGeometry.localRingHom_comp_stalkIso, Localization.AtPrime.map_eq_maximalIdeal, instFiniteDimensionalFractionRingOfFinite, Polynomial.UniversalCoprimeFactorizationRing.isCoprime_factor₁_factor₂, RatFunc.toFractionRingAlgEquiv_apply, universalHom_commutes, Algebra.IsAlgebraic.rank_fractionRing_polynomial, FractionRing.mk_eq_div, HomogeneousLocalization.algebraMap_apply, Module.FinitePresentation.exists_basis_localizedModule_powers, IsLocalization.isDomain_of_local_atPrime, Localization.AtPrime.mapPiEvalRingHom_algebraMap_apply, PrimeSpectrum.discreteTopology_iff_toPiLocalization_bijective, RingHom.surjective_localRingHom_iff, RatFunc.ofFractionRing_algebraMap, Module.FinitePresentation.linearEquivMapExtendScalars_symm_apply, Localization.coe_algEquiv_symm, Localization.algEquiv_symm_apply, Algebra.ZariskisMainProperty.exists_fg_and_exists_notMem_and_awayMap_bijective
|
numeratorRingHom 📖 | CompOp | 1 mathmath: numeratorRingHom_apply
|
universalHom 📖 | CompOp | 3 mathmath: universalHom_apply, universalHom_unique, universalHom_commutes
|