Morphisms of star rings #
This file defines a new type of morphism between (non-unital) rings A
and B
where both
A
and B
are equipped with a star
operation. This morphism, namely NonUnitalStarRingHom
, is
a direct extension of its non-star
red counterpart with a field map_star
which guarantees it
preserves the star operation.
As with NonUnitalRingHom
, the multiplications are not assumed to be associative or unital.
Main definitions #
Implementation #
This file is heavily inspired by Mathlib.Algebra.Star.StarAlgHom
.
Tags #
non-unital, ring, morphism, star
Non-unital star ring homomorphisms #
A non-unital ⋆-ring homomorphism is a non-unital ring homomorphism between non-unital
non-associative semirings A
and B
equipped with a star
operation, and this homomorphism is
also star
-preserving.
- toFun : A → B
- map_zero' : self.toFun 0 = 0
By definition, a non-unital ⋆-ring homomorphism preserves the
star
operation.
Instances For
By definition, a non-unital ⋆-ring homomorphism preserves the star
operation.
α →⋆ₙ+* β
denotes the type of non-unital ring homomorphisms from α
to β
.
Equations
- «term_→⋆ₙ+*_» = Lean.ParserDescr.trailingNode `term_→⋆ₙ+*_ 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →⋆ₙ+* ") (Lean.ParserDescr.cat `term 25))
Instances For
NonUnitalStarRingHomClass F A B
states that F
is a type of non-unital ⋆-ring homomorphisms.
You should also extend this typeclass when you extend NonUnitalStarRingHom
.
Instances
Turn an element of a type F
satisfying NonUnitalStarRingHomClass F A B
into an actual
NonUnitalStarRingHom
. This is declared as the default coercion from F
to A →⋆ₙ+ B
.
Equations
- ↑f = let __src := ↑f; { toNonUnitalRingHom := __src, map_star' := ⋯ }
Instances For
Equations
- NonUnitalStarRingHomClass.instCoeHeadNonUnitalStarRingHom = { coe := NonUnitalStarRingHomClass.toNonUnitalStarRingHom }
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
See Note [custom simps projection]
Equations
Instances For
Copy of a NonUnitalStarRingHom
with a new toFun
equal to the old one. Useful
to fix definitional equalities.
Equations
- f.copy f' h = { toFun := f', map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_star' := ⋯ }
Instances For
The identity as a non-unital ⋆-ring homomorphism.
Equations
- NonUnitalStarRingHom.id A = let __src := 1; { toNonUnitalRingHom := __src, map_star' := ⋯ }
Instances For
The composition of non-unital ⋆-ring homomorphisms, as a non-unital ⋆-ring homomorphism.
Equations
- f.comp g = let __src := f.comp g.toNonUnitalRingHom; { toNonUnitalRingHom := __src, map_star' := ⋯ }
Instances For
Equations
- NonUnitalStarRingHom.instZero = { zero := let __src := 0; { toNonUnitalRingHom := __src, map_star' := ⋯ } }
Equations
- NonUnitalStarRingHom.instInhabited = { default := 0 }
Equations
- NonUnitalStarRingHom.instMonoidWithZero = MonoidWithZero.mk ⋯ ⋯
Star ring equivalences #
A ⋆-ring equivalence is an equivalence preserving addition, multiplication, and the star operation, which allows for considering both unital and non-unital equivalences with a single structure.
- toFun : A → B
- invFun : B → A
- left_inv : Function.LeftInverse self.invFun self.toFun
- right_inv : Function.RightInverse self.invFun self.toFun
By definition, a ⋆-ring equivalence preserves the
star
operation.
Instances For
A ⋆-ring equivalence is an equivalence preserving addition, multiplication, and the star operation, which allows for considering both unital and non-unital equivalences with a single structure.
Equations
- «term_≃⋆+*_» = Lean.ParserDescr.trailingNode `term_≃⋆+*_ 25 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≃⋆+* ") (Lean.ParserDescr.cat `term 0))
Instances For
StarRingEquivClass F A B
asserts F
is a type of bundled ⋆-ring equivalences between A
and
B
.
You should also extend this typeclass when you extend StarRingEquiv
.
By definition, a ⋆-ring equivalence preserves the
star
operation.
Instances
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Turn an element of a type F
satisfying StarRingEquivClass F A B
into an actual
StarRingEquiv
. This is declared as the default coercion from F
to A ≃⋆+* B
.
Equations
- ↑f = let __src := ↑f; { toRingEquiv := __src, map_star' := ⋯ }
Instances For
Any type satisfying StarRingEquivClass
can be cast into StarRingEquiv
via
StarRingEquivClass.toStarRingEquiv
.
Equations
- StarRingEquivClass.instCoeHead = { coe := StarRingEquivClass.toStarRingEquiv }
The identity map as a star ring isomorphism.
Equations
- StarRingEquiv.refl = let __src := RingEquiv.refl A; { toRingEquiv := __src, map_star' := ⋯ }
Instances For
Auxilliary definition to avoid looping in dsimp
with StarRingEquiv.symm_mk
.
Equations
- StarRingEquiv.symm_mk.aux f f' h₁ h₂ h₃ h₄ h₅ = { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄, map_star' := h₅ }.symm
Instances For
Transitivity of StarRingEquiv
.
Equations
- e₁.trans e₂ = let __src := e₁.trans e₂.toRingEquiv; { toRingEquiv := __src, map_star' := ⋯ }
Instances For
If a (unital or non-unital) star ring morphism has an inverse, it is an isomorphism of star rings.
Equations
- StarRingEquiv.ofStarRingHom f g h₁ h₂ = { toFun := ⇑f, invFun := ⇑g, left_inv := h₁, right_inv := h₂, map_mul' := ⋯, map_add' := ⋯, map_star' := ⋯ }
Instances For
Promote a bijective star ring homomorphism to a star ring equivalence.
Equations
- StarRingEquiv.ofBijective f hf = let __src := RingEquiv.ofBijective f hf; { toFun := ⇑f, invFun := __src.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, map_star' := ⋯ }