Structures · Algebra
IsLocalHom
A map f between monoids is local if any a in the domain is a unit
whenever f a is a unit. See IsLocalRing.local_hom_TFAE for other equivalent
definitions in the local ring case - from where this concept originates, but it is useful in
other contexts, so we allow this generalisation in mathlib.
- Defined in
- Mathlib.Algebra.Group.Units.Hom
- Shape
- One type argument · adds map_nonunit
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances6
- CommRingCat.carrier
- MvPowerSeries
- PowerSeries
- Localization.AtPrime
- HomogeneousLocalization.AtPrime
- Subtype
How is a type an instance?
Loading the hierarchy index…
Assumed by81
- isUnit_map_iff
- IsLocalRing.ResidueField.map
- AlgebraicGeometry.Scheme.descResidueField
- IsLocalHom.map_nonunit
- IsUnit.of_map
- RingHom.domain_isLocalRing
- Algebra.FormallyUnramified.map_maximalIdeal
- IsLocalRing.comap_closedPoint
- Irreducible.of_map
- isUnit_of_map_unit
- IsLocalRing.maximalIdeal_comap
- AlgebraicGeometry.Scheme.residue_descResidueField
- Module.FaithfullyFlat.of_flat_of_isLocalHom
- IsLocalRing.ResidueField.map_comp
- IsLocalRing.ResidueField.lift
- Algebra.FormallyUnramified.iff_map_maximalIdeal_eq
- AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_Spec_fromSpecStalk
- IsLocalRing.ResidueField.map_residue
- IsLocalRing.ResidueField.map.congr_simp
- IsLocalHom.isField
- IsLocalRing.length_restrictScalars
- CovBy.length_baseChange
- IsLocalRing.map_maximalIdeal_lt_top
- IsLocalRing.length_baseChange
- IsRelPrime.of_map
- IsLocalRing.of_surjective
- RingHom.isLocalRing_pullback
- IsLocalRing.map_maximalIdeal_le
- map_nonunit
- bijective_rangeRestrict_comp_of_valuationRing
- IsLocalRing.ResidueField.mapAlgHom'
- IsLocalRing.ResidueField.map_comp_residue
- IsLocalRing.ResidueField.mapAlgEquiv'
- AlgebraicGeometry.Spec_closedPoint
- AlgebraicGeometry.Scheme.descResidueField.congr_simp
- IsLocalRing.ResidueField.mapAlgHom
- Algebra.FormallySmooth.of_formallySmooth_residueField_tensor
- AlgebraicGeometry.Scheme.descResidueField_fromSpecResidueField
- Algebra.FormallyUnramified.of_map_maximalIdeal
- Algebra.FormallyUnramified.isField_quotient_map_maximalIdeal
- map_mem_nonunits_iff
- CovBy.length_restrictScalars
- IsLocalRing.ResidueField.instAlgebra
- PowerSeries.map.isLocalHom
- Algebra.instFiniteResidueFieldOfFormallyUnramified
- AddMonoidAlgebra.isLocalHom_algebraMap
- IsLocalRing.ResidueField.mapAlgEquiv'_residue
- IsLocalRing.ResidueField.instIsScalarTower
- AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_Spec_fromSpecStalk_assoc
- AlgebraicGeometry.Scheme.residue_descResidueField_assoc
Ancestors0
No ancestors.