Category of Commutative Algebras

Stream: mathlib4

[Raghuram]

I have been playing with some code for commutative algebras and ended up with (so far) something roughly to the effect of (this is pseudo-code; I've only kept definitions and statements, omitting proofs):

-- Algebraic structure typeclass

/-- A commutative algebra is an algebra (see `Algebra`) in which multiplication is
commutative. -/
class CommAlgebra (R : Type u) [CommSemiring R] (A : Type v) [Semiring A]
    extends Algebra R A where
  /-- Multiplicative is commutative in a commutative algebra. -/
  mul_comm (a b : A) : a * b = b * a

variable (R : Type u) [CommSemiring R]

variable {R A} in
/-- Any commutative algebra is a commutative semiring.

This is not marked as an instance; it must be manually used. -/
def toCommSemiring (self : CommAlgebra R A) : CommSemiring A := { self with }

variable {R} in
/-- Creating a commutative algebra from a morphism to a commutative semiring.

The function `RingHom.toAlgebra` creates an algebra, but in fact the algebra is
always a commutative algebra if `A` is a commutative semiring. -/
def RingHom.toCommAlgebra {A : Type v} [CommSemiring A] : CommAlgebra R A where
  __ := f.toAlgebra
  mul_comm := CommSemiring.mul_comm

/-- A commutative R-algebra structure on a commutative A is equivalent to a ring hom `R →+* A`. -/
def CommAlgebra.equiv_RingHom (A : Type v) [CommSemiring A] :
    CommAlgebra R A ≃ (R →+* A) where
  toFun := (·.toRingHom)
  invFun := RingHom.toCommAlgebra

-- Category of commutative algebras

/-- The category of commutative R-algebras. -/
structure CommAlgebraCat where
  carrier : Type v
  isSemiring : Semiring carrier := by infer_instance
  isCommAlgebra : CommAlgebra R carrier := by infer_instance

instance : Category (CommAlgebraCat R) where
  Hom A B := A →ₐ[R] B
  id A := AlgHom.id R A
  comp f g := g.comp f

instance : ConcreteCategory (CommAlgebraCat R) where
  forget := { obj := CommAlgebraCat.carrier, map := (·.toFun) }

instance : HasForget₂ (CommAlgebraCat R) CommSemiRingCat where
  forget₂ := { obj := (CommSemiRingCat.of ·), map := AlgHom.toRingHom }

/-- The category of commutative R-algebras is isomorphic to the under-category
of R in the category of commutative semirings. -/
def IsoToUnderCommSemiRing :
    Cat.of (CommAlgebraCat R) ≅ Cat.of (Under (CommSemiRingCat.of R)) where
  hom := .toUnder (forget₂ (CommAlgebraCat R) CommSemiRingCat) (.of R)
    (fun A ↦ algebraMap R A) -- the map from R associated with each object
    AlgHom.comp_algebraMap    -- morphisms induce commutative triangles
  inv :=
    { obj := fun A ↦ CommAlgebraCat.of' A.hom.toCommAlgebra
      map := fun {A B} ⟨_, f, h⟩ ↦
        ⟨f, RingHom.congr_fun (h : B.hom = f.comp A.hom).symm⟩ }

-- Upgrades when `R` is in fact a `CommRing` rather than a `CommSemiring`
variable (R : Type u) [CommRing R]

instance : HasForget₂ (CommAlgebraCat R) CommRingCat where
  forget₂ := { obj := (CommRingCat.of ·), map := AlgHom.toRingHom }

/-- The category of commutative R-algebras is isomorphic to the under-category
of R in the category of commutative rings when R is a commutative ring. -/
def IsoToUnderCommRing :
    Cat.of (CommAlgebraCat R) ≅ Cat.of (Under (CommRingCat.of R)) where
  hom := .toUnder (forget₂ (CommAlgebraCat R) CommSemiRingCat) (.of R)
    (fun A ↦ algebraMap R A) -- the map from R associated with each object
    AlgHom.comp_algebraMap    -- morphisms induce commutative triangles
  inv :=
    { obj := fun A ↦ CommAlgebraCat.of' A.hom.toCommAlgebra
      map := fun {A B} ⟨_, f, h⟩ ↦
        ⟨f, RingHom.congr_fun (h : B.hom = f.comp A.hom).symm⟩ }
-- Proofs WIP for this last one

Since I already have and am adding to the code anyway, is there any interest in putting this / a modified version of this / something similar to this in Mathlib? (I know that CommRingCat already exists and one could just work with Under (CommRingCat.of R), so I'm not sure if this is wanted.)

[Eric Wieser]

I think CommAlgebraCat would be reasonable; you are not the first person to want this category:

@Amelia Livingston said:

I do ultimately need this for CommAlg R (not in mathlib but I have it in a file), yeah. I didn't use Mon_ to do this for Algebra R but I'll try using CommMon_ for commutative algebras and see if it's easier

[Eric Wieser]

(note that CommAlgebra is not reasonable, it won't work with typeclass search)

[Eric Wieser]

I believe @Amelia Livingston's code is public, though I don't remember where and it's possibly for Lean 3

[Raghuram]

Eric Wieser said:

I think CommAlgebraCat would be reasonable; you are not the first person to want this category:

I'm sure of that :laughing:; I wasn't sure if this way of doing it was desirable.
I very much don't know how to make design decisions when formalising things in Lean (in the sense of what will lead to less headaches to work with down the line).

[Adam Topaz]

The category CommAlgCat ( :cat: ) is certainly something that we want!

[Andrew Yang]

I think IsoToUnderCommRing should be stated in terms docs#CategoryTheory.Equivalence instead?

[Adam Topaz]

Yes, unless it's a definitional equality

[Adam Topaz]

(which it won't be in this case)

[Raghuram]

I tried to prove it was an isomorphism rather than an equivalence because it seemed like it was, well, an isomorphism rather than just an equivalence.
But yeah, I don't know the best practices here.

[Raghuram]

Let me try an Equivalence and see if it's easier.

[Adam Topaz]

If the right simp lemmas are set up properly, then providing the equivalence should just be a matter of extracting the two functors you already defined and using the built-in automation to get the proofs "for free".

[Adam Topaz]

well, I guess you have to provide the data of the natural isomorphism between the identify functors and the compositions, but that should be straightforward.

[Adam Topaz]

and in any case, an equivalence is likely to have much better definitional properties

[Raghuram]

I'm a bit clueless on how to come up with the components of the natural isomorphisms, since the identity and composition are in fact (i.e., mathematically rather than in Lean) equal and the natural transformation the identity map (but I don't know how to formalise that except by showing that they are equal and using eqToHom, which I'm guessing defeats the point, of having good definitional behaviour).

[Adam Topaz]

docs#CategoryTheory.NatIso.ofComponents

[Raghuram]

Thanks! That helps make the equivalence once I get the components.

[Adam Topaz]

If the isomorphisms needed for this natural isomorphism are indeed just "identities" then you can use docs#CategoryTheory.Iso.refl to fill in those components

[Adam Topaz]

And again, the automation should get the naturality proofs automatically. If not, then some API might be missing

[Raghuram]

Adam Topaz said:

If the isomorphisms needed for this natural isomorphism are indeed just "identities" then you can use docs#CategoryTheory.Iso.refl to fill in those components

They're morally identities, but the source and target are not definitionally equal (I think; otherwise the isomorphism I was trying to construct before should have been much easier).

[Adam Topaz]

I see, okay, but if the types are the same and the underlying map is indeed the identity, then it may work!

[Adam Topaz]

Worth a shot in any case!

[Raghuram]

Adam Topaz said:

Worth a shot in any case!

Didn't work unfortunately

[Raghuram]

Let me try to actually extract something readable to send here

[Kevin Buzzard]

They're morally identities

Next you'll be telling us they're canonically isomorphic :-)

Lean is quite fussy about this sort of thing :-/

[Raghuram]

Basic.lean
Above file defines CommAlgebra itself.

import Basic -- change accordingly
import Mathlib.Algebra.Category.AlgebraCat.Basic

open CategoryTheory
universe v u

variable (R : Type u) [CommSemiring R]

/-- The category of commutative R-algebras. -/
structure CommAlgebraCat where
  carrier : Type v
  isSemiring : Semiring carrier := by infer_instance
  isCommAlgebra : CommAlgebra R carrier := by infer_instance

attribute [instance] CommAlgebraCat.isSemiring CommAlgebraCat.isCommAlgebra

namespace CommAlgebraCat

instance : CoeSort (CommAlgebraCat R) (Type v) where
  coe := CommAlgebraCat.carrier

attribute [coe] CommAlgebraCat.carrier

instance category : Category (CommAlgebraCat R) where
  Hom A B := A →ₐ[R] B
  id A := AlgHom.id R A
  comp f g := g.comp f

instance concreteCategory : ConcreteCategory (CommAlgebraCat R) where
  forget := { obj := CommAlgebraCat.carrier, map := (·.toFun) }
  forget_faithful := ⟨AlgHom.coe_fn_inj.mp⟩

section Of
variable (A : Type v) [Semiring A]

/-- The object in the category of commutative R-algebras associated to
a type with the structure of a commutative R-algebra. -/
def of [CommAlgebra R A] : CommAlgebraCat R where
  carrier := A

variable {R} in
/-- The object in the category of commutative R-algebras associated to
a `CommAlgebra R` instance. -/
def of' {A : Type v} [Semiring A] (inst : CommAlgebra R A) : CommAlgebraCat R where
  isCommAlgebra := inst

end Of

section AlgebraicInstances
variable (self : CommAlgebraCat R)

instance isCommSemiring : CommSemiring self.carrier :=
  self.isCommAlgebra.toCommSemiring

instance isAlgebra : Algebra R self.carrier :=
  self.isCommAlgebra.toAlgebra

end AlgebraicInstances

instance hasForgetToCommSemiRing : HasForget₂ (CommAlgebraCat R) CommSemiRingCat where
  forget₂ := { obj := (CommSemiRingCat.of ·), map := AlgHom.toRingHom }

-- Locally redeclare R as a `CommRing`.
section CommRing variable (R : Type u) [CommRing R]

instance isCommRing (self : CommAlgebraCat R) : CommRing self.carrier where
  __ := Algebra.semiringToRing R
  __ := self.isCommSemiring

instance hasForgetToCommRing : HasForget₂ (CommAlgebraCat R) CommRingCat where
  forget₂ := { obj := (CommRingCat.of ·), map := AlgHom.toRingHom }

def EquivToUnderCommRing :
    Equivalence (CommAlgebraCat R) (Under (CommRingCat.of R)) where
  functor := .toUnder (forget₂ (CommAlgebraCat R) CommRingCat) (.of R)
    (fun A ↦ algebraMap R A) -- the map from R associated with each algebra
    AlgHom.comp_algebraMap    -- algebra morphisms induce commutative triangles
  inverse :=
    { obj := fun A ↦ CommAlgebraCat.of' A.hom.toCommAlgebra
      map := fun {A B} ⟨_, f, h⟩ ↦
        ⟨f, RingHom.congr_fun (h : B.hom = f.comp A.hom).symm⟩ }
  unitIso :=
    NatIso.ofComponents
      (fun A ↦ (sorry : A ≅ CommAlgebraCat.of' (algebraMap R A).toCommAlgebra))
  counitIso :=
    NatIso.ofComponents
      (fun ⟨_, A, f⟩ ↦ (sorry : (let A' : CommAlgebraCat := (CommAlgebraCat.of' f.toCommAlgebra)
                                  ⟨_, A', algebraMap R A'⟩
                                 ≅ ⟨_, A, f⟩))

end CommRing
end CommAlgebraCat

[Adam Topaz]

unknown package 'Basic'

[Raghuram]

Yes, that's a local import, which I attached at the beginning.
Would it be better to concatenate the two as a message?

[Adam Topaz]

well, first one should take care of the issues Eric pointed out above.

[Adam Topaz]

In this case we could just write

variable (R : Type u) [CommSemiring R]
/-- The category of commutative R-algebras. -/
structure CommAlgebraCat where
  carrier : Type v
  isCommSemiring : CommSemiring carrier := by infer_instance
  isAlgebra : Algebra R carrier := by infer_instance

[Raghuram]

I see

[Kevin Buzzard]

It's much better to have a term of type CommSemiring R than to have a term of type Semiring R and a proof of a * b = b * a kicking around, which you'll constantly have to be upgrading to a CommSemiring in order to use any lemmas about commutative semirings.

[Kevin Buzzard]

You could do this for example:

class CommAlgebra (R : Type u) (A : Type v) [CommSemiring R] [CommSemiring A] extends Algebra R A where

but then this makes it clear that CommAlgebra is not adding anything: we "have it already". Every definition comes with a cost -- you have to make the API for that definition. So it's best to make no definition if you can avoid making a definition.

[Raghuram]

This should be working code except for the last definition, which has sorry's (and so obviously can't fill in the proofs about them):

import Mathlib.Algebra.Category.AlgebraCat.Basic

open CategoryTheory
universe v u

variable (R : Type u) [CommSemiring R]

/-- The category of commutative R-algebras. -/
structure CommAlgebraCat where
  carrier : Type v
  isCommSemiring : CommSemiring carrier := by infer_instance
  isAlgebra : Algebra R carrier := by infer_instance

attribute [instance] CommAlgebraCat.isCommSemiring CommAlgebraCat.isAlgebra

namespace CommAlgebraCat

instance : CoeSort (CommAlgebraCat R) (Type v) where
  coe := CommAlgebraCat.carrier

attribute [coe] CommAlgebraCat.carrier

instance category : Category (CommAlgebraCat R) where
  Hom A B := A →ₐ[R] B
  id A := AlgHom.id R A
  comp f g := g.comp f

instance concreteCategory : ConcreteCategory (CommAlgebraCat R) where
  forget := { obj := CommAlgebraCat.carrier, map := (·.toFun) }
  forget_faithful := ⟨AlgHom.coe_fn_inj.mp⟩

section Of
variable (A : Type v) [CommSemiring A]

/-- The object in the category of commutative R-algebras associated to
a type with the structure of a commutative R-algebra. -/
def of [Algebra R A] : CommAlgebraCat R where
  carrier := A

variable {R} in
/-- The object in the category of commutative R-algebras associated to
a `CommAlgebra R` instance. -/
def of' {A : Type v} [CommSemiring A] (inst : Algebra R A) : CommAlgebraCat R where
  isAlgebra := inst

end Of

instance hasForgetToCommSemiRing : HasForget₂ (CommAlgebraCat R) CommSemiRingCat where
  forget₂ := { obj := (CommSemiRingCat.of ·), map := AlgHom.toRingHom }

-- Locally redeclare R as a `CommRing`.
section CommRing variable (R : Type u) [CommRing R]

instance isCommRing (self : CommAlgebraCat R) : CommRing self.carrier where
  __ := Algebra.semiringToRing R
  __ := self.isCommSemiring

instance hasForgetToCommRing : HasForget₂ (CommAlgebraCat R) CommRingCat where
  forget₂ := { obj := (CommRingCat.of ·), map := AlgHom.toRingHom }

def EquivToUnderCommRing :
    Equivalence (CommAlgebraCat R) (Under (CommRingCat.of R)) where
  functor := .toUnder (forget₂ (CommAlgebraCat R) CommRingCat) (.of R)
    (fun A ↦ algebraMap R A) -- the map from R associated with each algebra
    AlgHom.comp_algebraMap    -- algebra morphisms induce commutative triangles
  inverse :=
    { obj := fun A ↦ CommAlgebraCat.of' A.hom.toAlgebra
      map := fun {A B} ⟨_, f, h⟩ ↦
        ⟨f, RingHom.congr_fun (h : B.hom = f.comp A.hom).symm⟩ }
  unitIso :=
    NatIso.ofComponents
      (fun A ↦ (sorry : A ≅ CommAlgebraCat.of' (algebraMap R A).toAlgebra))
  counitIso :=
    NatIso.ofComponents
      (fun ⟨_, A, f⟩ ↦ sorry)

end CommRing
end CommAlgebraCat

[Raghuram]

Sorry about the problematic code earlier.

[Kevin Buzzard]

Lean is hard! Knowing the maths is not good enough; there are all sorts of subtleties, which you only discover by writing code and trying stuff out and asking experts. Don't be sorry! Thanks for asking!

[Raghuram]

That's very true :sweat_smile:
I meant the broken MWE though

[Raghuram]

Well, not exactly an MWE.

[Kevin Buzzard]

There are two non-defeq smuls:

def EquivToUnderCommRing :
    Equivalence (CommAlgebraCat R) (Under (CommRingCat.of R)) where
  functor := .toUnder (forget₂ (CommAlgebraCat R) CommRingCat) (.of R)
    (fun A ↦ algebraMap R A) -- the map from R associated with each algebra
    AlgHom.comp_algebraMap    -- algebra morphisms induce commutative triangles
  inverse :=
    { obj := fun A ↦ CommAlgebraCat.of' A.hom.toAlgebra
      map := fun {A B} ⟨_, f, h⟩ ↦
        ⟨f, RingHom.congr_fun (h : B.hom = f.comp A.hom).symm⟩ }
  unitIso :=
    NatIso.ofComponents
      (fun A ↦ by
        cases' A with A i1 i2
        dsimp [of', mk]
        convert CategoryTheory.Iso.refl _
        cases' i2 with i3 i4 h5 h6
        ext r x
        dsimp
        congr
        -- this is the problem I guess?
        sorry)
      sorry
  counitIso :=
    NatIso.ofComponents
      (fun ⟨_, A, f⟩ ↦ sorry)
      sorry
  functor_unitIso_comp := sorry

[Kevin Buzzard]

You need to use h6:

      (fun A ↦ by
        cases' A with A i1 i2
        dsimp [of', mk]
        convert CategoryTheory.Iso.refl _
        rename_i foo bar
        cases' i2 with i3 i4 h5 h6
        ext r x
        dsimp
        rw [h6]
        rfl)

[Kevin Buzzard]

In the definition of Algebra we have the field smul_def' : ∀ r x, r • x = toRingHom r * x and of course the proof of this isn't rfl, but somehow buried in the diagram chase you end up with two actions of R on A and this is the reason they're equal. This is why you're in hell.

[Raghuram]

Right - if I'm understanding correctly, when we go from CommAlgebraCat R to Under (CommRing.of R), we get the morphism toRingHom : R ->+* A, and the reconstruction of the algebra structure uses toRingHom r * x for the smul (definitionally), unlike the original algebra where the smul is the same, but only propositionally.

[Kevin Buzzard]

I need to do other things now so can't check details but this sounds like exactly the sort of thing which might be happening.

[Adam Topaz]

I think one should make a constructor that makes an iso from an AlgEquiv, then use something like docs#AlgEquiv.ofRingEquiv

[Adam Topaz]

Presumably on the level of rings RingEquiv.id would work?

[Adam Topaz]

Alternatively make a constructor that constructs an iso from an isomorphism on the level of rings together with a proof of compatibility with the scalar mult

[Antoine Chambert-Loir]

Kevin Buzzard said:

You could do this for example:

class CommAlgebra (R : Type u) (A : Type v) [CommSemiring R] [CommSemiring A] extends Algebra R A where

but then this makes it clear that CommAlgebra is not adding anything: we "have it already". Every definition comes with a cost -- you have to make the API for that definition. So it's best to make no definition if you can avoid making a definition.

On the other hand, would there be useful to have a systematic way of introducing standard algebraic objects via an abbreviation. Say you write [CommAlgebra R A], and the compiler translates it into [CommSemiring A] [Module R A]? And if some refactor suggest a better translation, then most of the files could remain the same.

[Raghuram]

As an update, here's what I've gotten so far:

import Mathlib.Algebra.Category.AlgebraCat.Basic

section Util

/- Proved in https://github.com/leanprover-community/mathlib4/pull/9511. -/
theorem Ring.toSemiring_injective {R : Type u} :
    Function.Injective (@Ring.toSemiring R) :=
  sorry

theorem CommRing.toCommSemiring_injective {R : Type u} :
    Function.Injective (@CommRing.toCommSemiring R) :=
  by rintro ⟨⟩ ⟨⟩ h; congr; exact Ring.toSemiring_injective (by injection h)

-- Commutative analogue of Algebra.semiringToRing
@[reducible] def Algebra.commSemiringToCommRing (R : Type u) [CommRing R]
    (A : Type v) [CommSemiring A] [Algebra R A] : CommRing A where
  __ := Algebra.semiringToRing R
  mul_comm := ‹CommSemiring A›.mul_comm

end Util

open CategoryTheory
universe v u

/-- The category of commutative R-algebras. -/
structure CommAlgebraCat (R : Type u) [CommSemiring R] where
  carrier : Type v
  isCommSemiring : CommSemiring carrier := by infer_instance
  isAlgebra : Algebra R carrier := by infer_instance

attribute [instance] CommAlgebraCat.isCommSemiring CommAlgebraCat.isAlgebra

namespace CommAlgebraCat

section RSemiring
variable (R : Type u) [CommSemiring R]

instance : CoeSort (CommAlgebraCat R) (Type v) where
  coe := CommAlgebraCat.carrier

attribute [coe] CommAlgebraCat.carrier

instance category : Category (CommAlgebraCat R) where
  Hom A B := A →ₐ[R] B
  id A := AlgHom.id R A
  comp f g := g.comp f

instance concreteCategory : ConcreteCategory (CommAlgebraCat R) where
  forget := { obj := CommAlgebraCat.carrier, map := (·.toFun) }
  forget_faithful := ⟨AlgHom.coe_fn_inj.mp⟩

section Of
variable (A : Type v) [CommSemiring A]

/-- The object in the category of commutative R-algebras associated to
a type with the structure of a commutative R-algebra. -/
def of [Algebra R A] : CommAlgebraCat R where
  carrier := A

variable {R A} in
/-- The object in the category of commutative R-algebras associated to
a `CommAlgebra R` instance. -/
def of' (inst : Algebra R A) : CommAlgebraCat R where
  isAlgebra := inst

end Of

-- Redeclare R as a `CommRing`.
end RSemiring section RRing variable (R : Type u) [CommRing R]

instance isCommRing (self : CommAlgebraCat R) : CommRing self.carrier :=
  Algebra.commSemiringToCommRing R self

instance hasForgetToCommRing : HasForget₂ (CommAlgebraCat R) CommRingCat where
  forget₂ := { obj := (CommRingCat.of ·), map := AlgHom.toRingHom }

@[simp] lemma forget₂_commRing_obj (A : CommAlgebraCat R) :
    (forget₂ _ CommRingCat).obj A = CommRingCat.of A :=
  rfl

@[simp] lemma forget₂_commRing_map {A B : CommAlgebraCat R} (f : A ⟶ B) :
    (forget₂ _ CommRingCat).map f = f.toRingHom :=
  rfl

def equivToUnderCommRing :
    Equivalence (CommAlgebraCat R) (Under (CommRingCat.of R)) where
  functor := .toUnder (forget₂ (CommAlgebraCat R) CommRingCat) (.of R)
    (algebraMap R ·)          -- map from R associated with each algebra
    AlgHom.comp_algebraMap    -- algebra morphisms induce commutative triangles
  inverse :=
    { obj := (CommAlgebraCat.of' ·.hom.toAlgebra)
      map := fun f ↦ ⟨f.right, RingHom.congr_fun f.w.symm⟩ }
  unitIso := NatIso.ofComponents
    (fun A ↦ eqToIso <| congrArg CommAlgebraCat.of' <|
                           -- We reconstructed the `smul`, but `smul_def` guarantees we get what we started with.
                           by ext; apply A.isAlgebra.smul_def)
  counitIso := NatIso.ofComponents
    (fun A ↦ eqToIso <| by
      -- Unwrap both sides to the form `⟨_, <comm ring>, <morphism from R>⟩`
      dsimp [Functor.toUnder]; conv => rhs; rewrite [StructuredArrow.eq_mk A]
      -- We reconstructed the `Neg` and `Sub`, but these are uniquely determined by the `Semiring` structure.
      congr; exact CommRing.toCommSemiring_injective rfl)

end RRing

I've constructed the natural isomorphism components using the above help, but the auto-param aesop_cat proofs are not succeeding.
(I'm not sure if this is because the isomorphisms are constructed essentially by rewriting CategoryTheory.Iso.refl idenity maps using object equalities and that's "evil" (indeed, the object equalities can be used equally well for constructing an isomorphism of categories as I was doing earlier, and I get very similar naturality goals to what I have left now, so perhaps I'm not properly "using" the fact that I'm constructing an Equivalence to make the job easier?).
I've used eqToIso because apparently it leads to less dependent type theory hell than literally rewriting, but maybe that wasn't enough?)

[Raghuram]

Adam Topaz said:

I think one should make a constructor that makes an iso from an AlgEquiv, then use something like docs#AlgEquiv.ofRingEquiv

Were you suggesting this just as a possible way to construct the natural isomorphism components or also because it would be easier to prove things (specifically naturality, right now) about or otherwise superior to the other approach, consisting of rewriting by object equality and using CategoryTheory.Iso.refl?
In the latter case, I can try to use this approach instead, but I don't know how to do it like this without again rewriting by an object equality (in which case it seems like I might as well just use the identity (iso)morphism any category provides).

[Raghuram]

Just to clarify the construction, and specifically what is definitionally and propositionally equal (to the best of my understanding):

• There are two categories, that of commutative R-algebras and that of commutative rings with a ring homomorphism from R, with functors between them forming an equivalence.
• For any commutative R-algebra, if we apply both functors, we get a commutative R-algebra which has:
  • the same type/carrier, definitionally
  • the same CommSemiRing structure, again should be definitionally true
  • the same R-algebra structure, but now only propositionally (partly, some fields are definitionally equal)

• Similarly, for any commutative ring with morphism from R, if we apply both functors, we get another one which has:

  • the same type/carrier, definitionally

  • the same CommRing structure, but now only propositionally (partly, the CommSemiring part of it is definitionally the same)
    (If we try to construct the analogous equivalence for R a CommSemiRing rather than CommRing, we actually do get definitional equality here.)

  • the same ring homomorphism.
    This should be definitionally true as functions. Since RingHom only depends on NonAssocSemiring, they should in fact have the same type, so they might be definitionally equal or something close to it as RingHoms as well (using proof irrelevance).

Given all of this, the natural isomorphism components mathematically "ought" to be identity morphisms (which is why I tried to construct an isomorphism of categories rather than an equivalence originally), which is why right now they are constructed by rewriting object equalities / using eqToIso. But if there's a different way of defining them in Lean that makes it easier to construct the equivalence/isomorphism, that would be great too.

[Raghuram]

Antoine Chambert-Loir said:

Say you write [CommAlgebra R A], and the compiler translates it into [CommSemiring A] [Module R A]? And if some refactor suggest a better translation, then most of the files could remain the same.

(Note: a commutative R-algebra isn't equivalent to a commutative (semi)ring which is an R-module because the multiplication might not be R-linear, but is rather equivalent to a commutative (semi)ring with a ring homomorphism from R. I'm assuming that you meant something more like for [CommAlgebra R A] to abbreviate [CommSemiring A] [<what we currently call Algebra R A>].)

I think that if an abbreviation like that was sufficient, then (dropping the commutativeness to talk about something already in Mathlib) Algebra R A could have been defined as a structure extending Semiring A to begin with, rather than one taking a Semiring A as a parameter.
I don't know for sure why it isn't defined that way, but I would guess it's to make it possible to talk about something being an algebra over mutiple (semi)rings with (definitionally) the same (semi)ring structure.

So (assuming such a use-case that prevents Algebra R A from extending Semiring A) in at least some use-cases you'll have to stop using the syntactic sugar that expands one declaration to two and write [(Comm)Semiring A] [Algebra R A] manually.

On the other hand, as an abbreviation for the most common use-case, I think this would be quite convenient, and there are many more similarly useful abbreviations. (For example, most files dealing with modules probably just have a module over a specific ring, and might benefit from a [Module' R M] which expands to [AddCommGroup M] [Module R M] or even a [ModulePair R M] which expands to [Ring R] [AddCommGroup M] [Module R M].)

That would have a much wider scope than what this thread is about though.

[Raghuram]

Raghuram said:

I've constructed the natural isomorphism components using the above help, but the auto-param aesop_cat proofs are not succeeding.

Rereading the chat, I'm guessing that I need to prove some more simp lemmas to make aesop_cat succeed at the naturality proofs (and hopefully the half-adjunction one as well).
But I'm not sure what kind of simp lemmas to prove.

[Kim Morrison]

You can show us some goals and we can guess. :-) Usually you need to write := by aesop_cat, look at the resulting failure, and guess what needs to be simplified! There's no shame in writing the proof by hand first, then adjusting it until aesop can reproduce it, and then finally deleting it.

[Andrew Yang]

I don't think you should use eqToIso since it invloves casts and is not good to work with.

[Andrew Yang]

There should be something like

variable {R} in
@[simps! hom_apply inv_apply]
def CommAlgebraCat.isoOf {A B : CommAlgebraCat R} (e : A ≃ₐ[R] B) : A ≅ B where
  hom := e.toAlgHom
  inv := e.symm.toAlgHom
  hom_inv_id := e.symm_comp
  inv_hom_id := e.comp_symm

def AlgEquiv.refl' {R A} [CommSemiring R] [Semiring A]
    {inst₁ : Algebra R A} {inst₂ : Algebra R A} (e : inst₁ = inst₂) :
    @AlgEquiv R A A _ _ _ inst₁ inst₂ :=
  @AlgEquiv.mk R A A _ _ _ inst₁ inst₂
    (Equiv.refl A) (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ ↦ e ▸ rfl)

then aesop works for you in unitIso:

unitIso := NatIso.ofComponents (fun X ↦ CommAlgebraCat.isoOf (AlgEquiv.refl' (Algebra.algebra_ext _ _ (fun _ ↦ rfl))))

[Raghuram]

Scott Morrison said:

There's no shame in writing the proof by hand

No shame, but work I was hoping to avoid ;)

Scott Morrison said:

You can show us some goals and we can guess. :-)

The sorrys in the above code snippet; here's one of them explicitly (after rintro _ _ (f : _ →ₐ[R] _); dsimp):

R : Type u
inst : CommRing R
X Y : CommAlgebraCat R
f : ↑X →ₐ[R] ↑Y
⊢ f ≫ eqToHom _ = eqToHom _ ≫ { toRingHom := ↑f, commutes' := _ }

The eqToHoms are components of the eqToIso isomorphisms I constructed, and the structure on the right is the image of f under the functor which I want to show is isomorphic to the identity.

I'll get started on trying to decipher this and prove it by hand in a while...

[Andrew Yang]

(deleted)

[Raghuram]

Andrew Yang said:

There should be something like

variable {R} in
@[simps! hom_apply inv_apply]
def CommAlgebraCat.isoOf {A B : CommAlgebraCat R} (e : A ≃ₐ[R] B) : A ≅ B where
  hom := e.toAlgHom
  inv := e.symm.toAlgHom
  hom_inv_id := e.symm_comp
  inv_hom_id := e.comp_symm

def AlgEquiv.refl' {R A} [CommSemiring R] [Semiring A]
    {inst₁ : Algebra R A} {inst₂ : Algebra R A} (e : inst₁ = inst₂) :
    @AlgEquiv R A A _ _ _ inst₁ inst₂ :=
  @AlgEquiv.mk R A A _ _ _ inst₁ inst₂
    (Equiv.refl A) (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ ↦ e ▸ rfl)

then aesop works for you in unitIso:

unitIso := NatIso.ofComponents (fun X ↦ CommAlgebraCat.isoOf (AlgEquiv.refl' (Algebra.algebra_ext _ _ (fun _ ↦ rfl))))

So is the idea that if we rewrite by the equality "deeper" inside, rather than rewriting Iso.refl or something, things become easier?

[Andrew Yang]

The key is to only rewrite equalities in Prop type goals if possible.

[Christian Merten]

Is there a PR for this? If not, are you still working on this @Raghuram? Bumping this thread, because I need CommAlgebraCat.

[Andrew Yang]

Maybe use Under (CommRingCat.of R) in the mean time? Unless the base ring is a semiring.

[Christian Merten]

Good idea, I'll inherit limit properties from CommRingCat right? So taking limits should be okay, probably comparing to the corresponding limit in ModuleCat R is painful? I am reluctant to write API for this, if it is to be replaced by CommAlgebraCat anyway.

[Andrew Yang]

The existing API for general over categories should be enough I think.

[Christian Merten]

I'll give it a shot (if we stick with the explicit definition of docs#adicCompletion, I might not need it anyway).

[Eric Wieser]

Maybe @Adam Topaz has opinions on whether we should define a new CommAlgebraCat, or use what Andrew describes.

[Raghuram]

Christian Merten said:

Is there a PR for this? If not, are you still working on this Raghuram? Bumping this thread, because I need CommAlgebraCat.

Can't say what anyone else has done, but pretty much everything I have done is in this thread.