theorem
L28 ↗residue_mapOfRingHom
TwoChartCech.Cover.LaurentChart.residue_mapOfRingHom
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.Cover_LaurentChart_residue_mapOfRingHom
universe u vLean source · statement
theorem _root_.TwoChartCech.Cover.LaurentChart.residue_mapOfRingHom {R : Type u} {S : Type u}
[CommRing R] [CommRing S]
{𝒰 : TwoChartCech.Cover.{u, v} R} {𝒲 : TwoChartCech.Cover.{u, v} S}
(τ : R →+* S) (φ : 𝒰.A01 →+* 𝒲.A01)
(h : φ.comp (algebraMap R 𝒰.A01) = (algebraMap S 𝒲.A01).comp τ)
(Λ : 𝒰.LaurentChart) (Λ' : 𝒲.LaurentChart) (hΛ : ∀ y : 𝒰.A01, Λ'.expand (φ y) = (Λ.expand
y).map τ)
(η : Ω[𝒰.A01⁄R]) :
Λ'.residue (KaehlerDifferential.mapOfRingHom τ φ h η) = τ (Λ.residue η)