Algebraize tactic #
This file defines the algebraize
tactic. The basic functionality of this tactic is to
automatically add Algebra
instances given RingHom
s. For example, algebraize [f, g]
where
f : A →+* B
and g : B →+* C
are RingHom
s, will add the instances Algebra A B
and
Algebra B C
corresponding to these RingHom
s.
Further functionality #
When given a composition of RingHom
s, e.g. algebraize [g.comp f]
, the tactic will also try to
add the instance IsScalarTower A B C
if possible.
After having added suitable Algebra
and IsScalarTower
instances, the tactic will search through
the local context for RingHom
properties that can be converted to properties of the corresponding
Algebra
. For example, given f : A →+* B
and hf : f.FiniteType
, then algebraize [f]
will add
the instance Algebra A B
and the corresponding property Algebra.FiniteType A B
. The tactic knows
which RingHom
properties have a corresponding Algebra
property through the algebraize
attribute.
Algebraize attribute #
The algebraize
attribute is used to tag RingHom
properties that can be converted to Algebra
properties. It assumes that the tagged declaration has a name of the form RingHom.Property
and
that the corresponding Algebra
property has the name Algebra.Property
.
If not, the Name
of the corresponding algebra property can be provided as optional argument. The
specified declaration should be one of the following:
- An inductive type (i.e. the
Algebra
property itself), in this case it is assumed that theRingHom
and theAlgebra
property are definitionally the same, and the tactic will construct theAlgebra
property by giving theRingHom
property as a term. - A constructor for the
Algebra
property. In this case it is assumed that theRingHom
property is the last argument of the constructor, and that no other explicit argument is needed. The tactic then constructs theAlgebra
property by applying the constructor to theRingHom
property.
Here are three examples of properties tagged with the algebraize
attribute:
@[algebraize]
def RingHom.FiniteType (f : A →+* B) : Prop :=
@Algebra.FiniteType A B _ _ f.toAlgebra
An example when the Name
is provided (as the Algebra
does not have the expected name):
@[algebraize Module.Finite]
def RingHom.Finite (f : A →+* B) : Prop :=
letI : Algebra A B := f.toAlgebra
Module.Finite A B
An example with a constructor as parameter (as the two properties are not definitonally the same):
@[algebraize Algebra.Flat.out]
class RingHom.Flat {R : Type u} {S : Type v} [CommRing R] [CommRing S] (f : R →+* S) : Prop where
out : f.toAlgebra.Flat := by infer_instance
algebraize_only #
To avoid searching through the local context and adding corresponding Algebra
properties, use
algebraize_only
which only adds Algebra
and IsScalarTower
instances.
Function that extracts the name of the corresponding Algebra
property from a RingHom
property that has been tagged with the algebraize
attribute. This is done by either returning the
parameter of the attribute, or by assuming that the tagged declaration has name RingHom.Property
and then returning Algebra.Property
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A user attribute that is used to tag RingHom
properties that can be converted to Algebra
properties. Using an (optional) parameter, it will also generate a Name
of a declaration which
will help the algebraize
tactic access the corresponding Algebra
property.
There are two cases for what declaration corresponding to this Name
can be.
- An inductive type (i.e. the
Algebra
property itself), in this case it is assumed that theRingHom
and theAlgebra
property are definitionally the same, and the tactic will construct theAlgebra
property by giving theRingHom
property as a term. - A constructor for the
Algebra
property. In this case it is assumed that theRingHom
property is the last argument of the constructor, and that no other explicit argument is needed. The tactic then constructs theAlgebra
property by applying the constructor to theRingHom
property.
Finally, if no argument is provided to the algebraize
attribute, it is assumed that the tagged
declaration has name RingHom.Property
and that the corresponding Algebra
property has name
Algebra.Property
. The attribute then returns Algebra.Property
(so assume case 1 above).
Given an expression f
of type RingHom A B
where A
and B
are commutative semirings,
this function adds the instance Algebra A B
to the context (if it does not already exist).
This function also requries the type of f
, given by the parameter ft
. The reason this is done
(even though ft
can be inferred from f
) is to avoid recomputing ft
in the algebraize
tactic,
as when algebraize
calls addAlgebraInstanceFromRingHom
it has already computed ft
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Given an expression g.comp f
which is the composition of two RingHom
s, this function adds
the instance IsScalarTower A B C
to the context (if it does not already exist).
Equations
- One or more equations did not get rendered due to their size.
Instances For
This function takes an array of expressions t
, all of which are assumed to be RingHom
s,
and searches through the local context to find any additional properties of these RingHoms
, after
which it tries to add the corresponding Algebra
properties to the context. It only looks for
properties that have been tagged with the algebraize
attribute, and uses this tag to find the
corresponding Algebra
property.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Mathlib.Tactic.Algebraize.instInhabitedConfig = { default := { properties := default } }
Function elaborating Algebraize.Config
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A list of terms passed to algebraize
as argument.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Tactic that, given RingHom
s, adds the corresponding Algebra
and (if possible)
IsScalarTower
instances, as well as Algebra
corresponding to RingHom
properties available
as hypotheses.
Example: given f : A →+* B
and g : B →+* C
, and hf : f.FiniteType
, algebraize [f, g]
will
add the instances Algebra A B
, Algebra B C
, and Algebra.FiniteType A B
.
See the algebraize
tag for instructions on what properties can be added.
The tactic also comes with a configuration option properties
. If set to true
(default), the
tactic searches through the local context for RingHom
properties that can be converted to
Algebra
properties. The macro algebraize_only
calls
algebraize (config := {properties := false})
,
so in other words it only adds Algebra
and IsScalarTower
instances.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Version of algebraize
, which only adds Algebra
instances and IsScalarTower
instances,
but does not try to add any instances about any properties tagged with
@[algebraize]
, like for example Finite
or IsIntegral
.
Equations
- One or more equations did not get rendered due to their size.