IMO 2012 A5 (Good maps and ring homomorphisms) #
We prove some results relating good maps and ring homomorphisms. Namely, good maps behave well with respect to composing with ring homomorphisms.
theorem
IMOSL.IMO2012A5.Generalization.good_comp_hom
{R : Type u_2}
{S : Type u_3}
[NonAssocSemiring R]
[NonAssocSemiring S]
{f : R → S}
{R₀ : Type u_1}
(h : good f)
[NonAssocSemiring R₀]
(φ : R₀ →+* R)
:
theorem
IMOSL.IMO2012A5.Generalization.good_hom_comp
{R : Type u_2}
{S : Type u_3}
[NonAssocSemiring R]
[NonAssocSemiring S]
{f : R → S}
{S₀ : Type u_1}
(h : good f)
[NonAssocSemiring S₀]
(φ : S →+* S₀)
:
theorem
IMOSL.IMO2012A5.Generalization.NontrivialGood.comp_hom
{R : Type u_2}
{S : Type u_3}
[NonAssocSemiring R]
[NonAssocSemiring S]
{f : R → S}
{R₀ : Type u_1}
(hf : NontrivialGood f)
[NonAssocSemiring R₀]
(φ : R₀ →+* R)
:
NontrivialGood (f ∘ ⇑φ)
theorem
IMOSL.IMO2012A5.Generalization.NontrivialGood.hom_comp
{R : Type u_2}
{S : Type u_3}
[NonAssocSemiring R]
[NonAssocSemiring S]
{f : R → S}
{S₀ : Type u_1}
(hf : NontrivialGood f)
[NonAssocSemiring S₀]
(φ : S →+* S₀)
:
NontrivialGood (⇑φ ∘ f)