unitsModPrincipalUnitsEquivResidueFieldUnits

English

There is a multiplicative equivalence between the quotient of the unit group of A by the principal unit comap and the units of the residue field.

Русский

Существует мультипликативное эквивалентности между фактор-группой единиц A по отношению к главной единичной группе и единицами остаточного поля.

LaTeX

$$A.unitGroup ⧸ A.principalUnitGroup.comap A.unitGroup.subtype ≃* (IsLocalRing.ResidueField A)ˣ$$

Lean4

/-- The quotient of the unit group of `A` by the principal unit group of `A` agrees with
the units of the residue field of `A`. -/
def unitsModPrincipalUnitsEquivResidueFieldUnits :
    A.unitGroup ⧸ A.principalUnitGroup.comap A.unitGroup.subtype ≃* (IsLocalRing.ResidueField A)ˣ :=
  (QuotientGroup.quotientMulEquivOfEq A.ker_unitGroupToResidueFieldUnits.symm).trans
    (QuotientGroup.quotientKerEquivOfSurjective _ A.surjective_unitGroupToResidueFieldUnits)

Похожие утверждения