Adding instances to Algebra/Order/Kleene.lean

Stream: new members

[Nick Decroos]

I am trying to define instances for AddOpposite, MulOpposite, ULift, Subsemiring, Subring and Subalgebra here. (These instances were specified in a TODO in that file.)

I have this code now (I'm omitting the instance statements that raised no problems).

-- Add these imports to file
import Mathlib.Algebra.Ring.Subring.Basic
import Mathlib.Algebra.Algebra.Subalgebra.Basic

namespace Subring

instance instIdemSemiring [IdemSemiring α] : IdemSemiring (Subring α) := sorry

instance [IdemCommSemiring α] : IdemCommSemiring (Subring α) := sorry

instance [KleeneAlgebra α] : KleeneAlgebra (Subring α) := sorry

end Subring

namespace Subalgebra

instance instIdemSemiring [IdemSemiring α] : IdemSemiring (Subalgebra α) := sorry

instance [IdemCommSemiring α] : IdemCommSemiring (Subalgebra α) := sorry

instance [KleeneAlgebra α] : KleeneAlgebra (Subalgebra α) := sorry

end Subalgebra

For Subring, I get the error

failed to synthesize
  Ring α
use `set_option diagnostics true` to get diagnostic information

For Subalgebra, I get the error message that a build cycle is detected.

`c:\Users\desti\.elan\toolchains\leanprover--lean4---v4.10.0-rc1\bin\lake.exe setup-file C:/Users/desti/OneDrive/Documenten/mathlib4/Mathlib/Algebra/Order/Kleene.lean Init Mathlib.Algebra.Order.Monoid.Canonical.Defs Mathlib.Algebra.Ring.Pi Mathlib.Algebra.Ring.InjSurj Mathlib.Tactic.Monotonicity.Attr Mathlib.Algebra.Ring.Prod Mathlib.Algebra.Order.Monoid.Canonical.Defs Mathlib.Algebra.Ring.Subsemiring.Basic Mathlib.Algebra.Ring.Subring.Basic Mathlib.Algebra.Algebra.Subalgebra.Basic --no-build` failed:

stderr:
✖ [1014/1066] Running Mathlib.Algebra.Order.Kleene
error: build cycle detected:
  +Mathlib.Algebra.Algebra.Subalgebra.Basic:olean
  +Mathlib.Algebra.Order.Kleene:deps
  +Mathlib.Algebra.Order.Kleene:leanArts
  +Mathlib.Algebra.Order.Kleene:olean
  +Mathlib.Algebra.Algebra.Operations:deps
  +Mathlib.Algebra.Algebra.Operations:leanArts
  +Mathlib.Algebra.Algebra.Operations:olean
  +Mathlib.Algebra.Algebra.Subalgebra.Basic:deps
  +Mathlib.Algebra.Algebra.Subalgebra.Basic:leanArts
  +Mathlib.Algebra.Algebra.Subalgebra.Basic:olean
✖ [1056/1066] Running Mathlib.Data.Set.Semiring
error: .\.\.\.\Mathlib\Data\Set\Semiring.lean: bad import 'Mathlib.Algebra.Order.Kleene'
✖ [1058/1066] Running Mathlib.Algebra.Algebra.Operations
error: .\.\.\.\Mathlib\Algebra\Algebra\Operations.lean: bad import 'Mathlib.Algebra.Order.Kleene'
error: .\.\.\.\Mathlib\Algebra\Algebra\Operations.lean: bad import 'Mathlib.Data.Set.Semiring'
✖ [1059/1066] Running Mathlib.Algebra.Algebra.Subalgebra.Basic
error: .\.\.\.\Mathlib\Algebra\Algebra\Subalgebra\Basic.lean: bad import 'Mathlib.Algebra.Algebra.Operations'
✖ [1060/1066] Running imports (C:/Users/desti/OneDrive/Documenten/mathlib4/Mathlib/Algebra/Order/Kleene.lean)
error: C:/Users/desti/OneDrive/Documenten/mathlib4/Mathlib/Algebra/Order/Kleene.lean: bad import 'Mathlib.Algebra.Algebra.Subalgebra.Basic'
Some builds logged failures:
- Mathlib.Algebra.Order.Kleene
- Mathlib.Data.Set.Semiring
- Mathlib.Algebra.Algebra.Operations
- Mathlib.Algebra.Algebra.Subalgebra.Basic
- imports (C:/Users/desti/OneDrive/Documenten/mathlib4/Mathlib/Algebra/Order/Kleene.lean)
error: build failed

[Eric Wieser]

Did you mean

instance [IdemCommSemiring α] (S : Subring α) : IdemCommSemiring S := sorry

instead of

instance [IdemCommSemiring α] : IdemCommSemiring (Subring α) := sorry

?

[Nick Decroos]

Eric Wieser

Thanks for the feedback. Yes, I actually meant the first definition. So I guess I should change it for all definitions?

[Nick Decroos]

I now have this code at the moment:

namespace AddOpposite

instance instIdemSemiring [IdemSemiring α] : IdemSemiring (AddOpposite α) := sorry

instance [IdemCommSemiring α] : IdemCommSemiring (AddOpposite α) := sorry

instance [KleeneAlgebra α] : KleeneAlgebra (AddOpposite α) := sorry

end AddOpposite

namespace MulOpposite

instance instIdemSemiring [IdemSemiring α] : IdemSemiring (MulOpposite α) := sorry

instance [IdemCommSemiring α] : IdemCommSemiring (MulOpposite α) := sorry

instance [KleeneAlgebra α] : KleeneAlgebra (MulOpposite α) := sorry

end MulOpposite

namespace ULift

instance instIdemSemiring [IdemSemiring α] : IdemSemiring (ULift α) := sorry

instance [IdemCommSemiring α] : IdemCommSemiring (ULift α) := sorry

instance [KleeneAlgebra α] : KleeneAlgebra (ULift α) := sorry

end ULift

namespace Subsemiring

instance instIdemSemiring [IdemSemiring α] : IdemSemiring (Subsemiring α) := sorry

instance [IdemCommSemiring α] (S : Subsemiring α) : IdemCommSemiring S := sorry

instance [KleeneAlgebra α] (S : Subsemiring α) : KleeneAlgebra S := sorry

end Subsemiring



namespace Subring

instance instIdemSemiring [IdemSemiring α] [Ring α] : IdemSemiring (Subring α) := sorry

instance [IdemCommSemiring α] [S : Ring α] (S : Subring α) : IdemCommSemiring S := sorry

instance [KleeneAlgebra α] [S : Ring α] (S : Subring α) : KleeneAlgebra S := sorry

end Subring

/-
namespace Subalgebra

instance instIdemSemiring [IdemSemiring α] : IdemSemiring (Subalgebra α) := sorry

instance [IdemCommSemiring α] (S : Subalgebra α) : IdemCommSemiring S := sorry

instance [KleeneAlgebra α] (S : Subalgebra α) : KleeneAlgebra S := sorry

end Subalgebra
-/

[Eric Wieser]

The approach here is going to be to define Function.Injective.idemCommSemiring etc

[Nick Decroos]

Eric Wieser said:

The approach here is going to be to define Function.Injective.idemCommSemiring etc

I'm sorry, I don't know how to implement this approach, and why it should work. Can you explain this?