# Zulip Chat Archive

## Stream: new members

### Topic: Help constructing a natural transformation

#### Vasily Ilin (May 20 2022 at 00:07):

I have state

```
K: Type u_1
_inst_1: comm_ring K
⊢ coyoneda.obj (opposite.op (Algebra.of K K[X])) ⟶ forget (Algebra K)
```

in my proof. What should my next line be? I tried

```
hom :=
{ app := sorry,
naturality' := sorry,
},
```

but getting `invalid 'begin-end' expression, ',' expected`

.

Here is the full code:

```
-- https://leanprover-community.github.io/mathlib_docs/category_theory/functor/hom.html
-- THE PLAN IS TO DEFINE AN AFFINE GROUP SCHEME AS A REPRESENTABLE FUNCTOR FROM K-ALGEBRAS TO GROUPS, AND PROVE THAT G_a := Hom(K[X], _) IS AN AFFINE GROUP SCHEME
import category_theory.types
import algebra.category.Algebra.basic
import algebra.category.Group.basic
import data.polynomial.basic
import data.polynomial.algebra_map
import category_theory.over
import tactic
open_locale polynomial
open polynomial
open category_theory
variables (K : Type*) [comm_ring K]
-- variables (K_alg : Type*) [category K_alg] [category_theory.under K] -- category of commutative K-algebras. But how to use it...
class affine_scheme :=
(scheme : Algebra K ⥤ Type*)
(corepresentable : scheme.corepresentable)
class affine_group_scheme :=
(scheme : Algebra K ⥤ Group)
(corepresentable : (scheme ⋙ forget Group).corepresentable)
-- DEFINING G_a
instance G_a : affine_scheme K :=
{
scheme := forget (Algebra K),
corepresentable := begin
refine {has_corepresentation := _},
refine ⟨opposite.op (Algebra.of K K[X]), _⟩, -- ∃ (f : coyoneda.obj (opposite.op (Algebra.of K K[X])) ⟶ forget (Algebra K)), is_iso f
refine exists.intro _ _,
hom :=
{ app := sorry,
naturality' := sorry,
},
-- need to contruct a natural tranformation Hom(K[X], _) ⟶ forget (Algebra K)
-- see for an example of defining a natural transformation https://leanprover-community.github.io/mathlib_docs/category_theory/yoneda.html#category_theory.yoneda_lemma
end,
}
```

#### Adam Topaz (May 20 2022 at 00:15):

I would avoid constructing the corepresentable term in tactic mode.

#### Adam Topaz (May 20 2022 at 00:19):

Also, I think you're misunderstanding what typeclasses are for. Certainly defining `G_a : affine_scheme K`

makes no sense if you want $\mathbb{G_a}$.

#### Adam Topaz (May 20 2022 at 00:25):

But if you ignore those issues, here is something to get you started

```
instance G_a : affine_scheme K :=
{
scheme := forget (Algebra K),
corepresentable := begin
refine {has_corepresentation := _},
refine ⟨opposite.op (Algebra.of K K[X]), _⟩, -- ∃ (f : coyoneda.obj (opposite.op (Algebra.of K K[X])) ⟶ forget (Algebra K)), is_iso f
refine exists.intro _ _,
refine ⟨_,_⟩,
{ intros A, dsimp, intros f,
exact f X },
{ tidy },
{ apply_with nat_iso.is_iso_of_is_iso_app { instances := ff },
intros A, rw is_iso_iff_bijective,
sorry
}
end,
}
```

#### Violeta Hernández (May 20 2022 at 00:28):

The solution here is to make `G_a`

a `def`

instead of an `instance`

#### Violeta Hernández (May 20 2022 at 00:30):

An `instance`

is some theorem or construction that you want to always make available on some type. For instance, there is an instance `field ℝ`

that builds a field structure on `ℝ`

, which you have available every time some theorem calls for a field.

#### Violeta Hernández (May 20 2022 at 00:30):

Here, you just want to build some specific object, nothing canonical. So you should have a `def`

instead.

#### Reid Barton (May 20 2022 at 02:26):

And `affine_scheme`

and `affine_group_scheme`

should be `structure`

s

#### Junyan Xu (May 20 2022 at 03:14):

Note that we have docs#algebraic_geometry.is_affine

Last updated: Dec 20 2023 at 11:08 UTC